 In what follows, we shall assume familiarity with the above axioms and rules as we derive Frege’s Theorem. As noted, these are essentially the same as the axioms for the first-order predicate calculus, except for the addition of laws for the second-order quantifiers \(\forall F\) and \(\exists F\) that correspond to the laws governing the first-order quantifiers \(\forall x\) and \(\exists x\).