 It should be noted at this point that instead of using comprehension principles, Frege had a distinguished rule in his system that is equivalent to such principles, namely, his Rule of Substitution. Though Frege’s Rule of Substitution appears to allow the substitution of formulas \(\phi\) for free concept variables \(F\) in theorems of logic, we can understand this rule in terms of the second-order logic we’ve defined as follows: in any theorem of logic with a free variable \(F^{n}\), one may both substitute any \(n\)-place \(\lambda\)-expression \([\lambda x_{1}\ldots x_{n}\, \phi]\) for \(F^{n}\) and then perform \(\lambda\)-conversion. For example, in the second-order system we now have, one can infer \(\forall x(Ox \amp x \gt 5 \equiv Ox \amp x \gt 5)\) from \(\forall y(Fy \equiv Fy)\) by first substituting \([\lambda x \, Ox \amp x \gt 5]\) for \(F\) and then using \(\lambda\)-Conversion on all the resulting subformulas containing the \(\lambda\)-expression that flank the \(\equiv\) sign.  Frege’s Rule of Substitution allows one to do all this in one step. Readers interested in learning a bit more about the connection between the Rule of Substitution and Comprehension Principles described above can consult the following supplementary document: