We often replace axioms that quantify over sets with first-order axiom schemata in order to obtain a first-order system of axioms. For example, the axiom of induction gives rise in a natural way to the first-order axiom schema of induction.

What is the actual definition of this 'natural way', and more to the point, which (second-order) sentences give rise to schemata in this way?

Example. In the Peano Postulates, we have the axiom of full induction.

For all sets $A$, we have that if $0 \in A$ and $n \in A \Rightarrow S(n) \in A$ for all $n$, then $n \in A$ for all $n$.

Now with respect to any given language of interest, this gives rise to a first-order axiom schema of induction, namely

[For all predicates $\phi(*)$ definable in the language of interest], we have that if $\phi(0)$ and $\phi(n) \Rightarrow \phi(S(n))$ for all $n$, then $\phi(n)$ for all $n$.


I'd much prefer to present the second-order Induction Axiom like this:

$$\forall X([X0 \land \forall n(Xn \to Xn')] \to \forall nXn)$$

with a genuine second-order quantifier ('for all sets' sounds too much like a sorted first-order quantification over sets). The corresponding first order schema is

$$([\varphi(0) \land \forall n(\varphi(n) \to \varphi(n'))] \to \forall n\varphi(n))$$ And the correspondence is plain. Given a second-order universal quantification $\forall X\Psi$ (where the initial quantification and its associated monadic variables are the only second order expressions in the sentence) the counterpart first-order schema is formed by deleting the initial quantifier and replacing every $X\tau$ for term $\tau$ by the schematic $\varphi(\tau)$.

If a second-order theory is such that any second-order axioms can regimented with single prenex second-order universal quantifiers (and associated monadic variables), then the theory will have a schematic first-order counterpart formed in this way by replacing the second order axioms with all the instances of the counterpart first-order schema. (In principle, there could be more complex cases, where we have a second-order theory whose second-order quantifiers run over many-place relations, not one-place properties and/or there are multiple quantifiers: then schematization would be more complex, but as far as I know [away from the library!] things go as you would expect.)

You mention that second-order arithmetic has a first-order counterpart where the second-order induction axiom is replaced by every instance of the schematic counterpart of the axiom. Another example is second-order set theory where a second-order replacement axiom has as its first-order counterpart the instances of the familiar first-order replacement schema, etc. For more, see e.g. Shapiro's Foundations without Foundationalism: A Case for Second-order Logic.

  • $\begingroup$ Peter thanks for your answer. I'm a little confused about this fragment: "If a second-order theory is such that any second-order axioms can regimented with single prenex second-order quantifiers, then the theory will have a schematic first-order counterpart..." I find this surprising; surely we require that the prenex quantifier be $\forall,$ as opposed to $\exists$? Also, why does it have to be single? Why can't sentences of the form $\forall X\forall Y : \Psi(X,Y)$ be used? $\endgroup$ – goblin Aug 1 '13 at 8:46
  • $\begingroup$ Oops, I indeed meant universal quantifiers: sorry for the slip. As to "single" I was just thinking of the common sorts of case -- as you say there's nothing in principle to stop more complex cases. I've clarified just a bit. Thanks for the correction. $\endgroup$ – Peter Smith Aug 1 '13 at 12:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.