From the mathematical point of view, the discussion of Reflection in what you wrote (by Sy) seems to be oversimplified (and seems to be incorrect). The reflection principles

- anything first order true in is true in some
- anything second order true in is true in some

are both fairly weak. (1) has models where . So does (2). If you only want to consider such models where is strongly inaccessible, then 2) has models where lambda is among the first strongly inaccessible cardinals. So (2) only gives you a handful of strongly inaccessible cardinals in a context like MK or MK + global choice.

- anything first order true in is true in some , with set parameters.
- anything second order true in is true in some , with set parameters.

As is well known, the models of (3) are exactly the models of ZF. If (4) is formulated as a scheme over NBG then we get a system which is equiconsistent with the normal formulation of second order reflection, (6) below. However, it does not appear that (4) over even MK with global choice will prove the existence of a Mahlo cardinal (I haven’t thought about showing this).

- anything first order true in any is true in some , arbitrary.
- anything second order true in any is true in some , arbitrary.

(5) holds in exactly the for which lambda is strongly inaccessible. (6) is the normal way of formulating second order reflection. As a scheme over NBG, it proves the existence of weakly compact cardinals. A subtle cardinal proves the existence of models .

Harvey