4

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$.

goblin GONE
  • 67,744

1 Answers1

6

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.

Peter Smith
  • 54,743
  • 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? – goblin GONE Aug 01 '13 at 08:46
  • 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. – Peter Smith Aug 01 '13 at 12:03