Axiom schemas, such as the PA induction schema, differ from second-order axioms in that they only hold for "definable" predicates, rather for "all" predicates. As a result, you can have non-standard models of first-order PA for which induction holds for all definable predicates, but does not hold true in general.

This leads to questions about which predicates "exist." In general, for every possible infinite combination of natural numbers (or more generally, objects in the domain), is there considered to "exist" a unary predicate that is "true" for only those numbers, even if the predicate is undefinable? And likewise with n-ary predicates?

This would seem to be a semantic thing. Is there an "axiom of first-order logic" that determines which of these predicates we consider to "exist?" (Or would this perhaps be more pertinent to second-order logic, being related to things like Henkin semantics?)

  • 1
    $\begingroup$ (Unary) Predicates define subsets of the domain (or, more generally, subobjects but I won't go there...) What's happening is not every subset is necessarily characterized by a predicate. I recommend terminologically separating predicates from the subsets (relations, in the general $n$-ary case) that are their semantics. You get: "the interpretation of the induction schema means induction holds for the interpretation of any predicate but not for all subsets." $\endgroup$ – Derek Elkins left SE Mar 10 '19 at 7:12
  • $\begingroup$ One small but important point is that the second-order induction axiom is a specific instance of the induction scheme for second-order arithmetic. It is the induction instance for the formula $n \in A$. This axiom is only strong in circumstances where other choices require many sets to exist. $\endgroup$ – Carl Mummert Mar 10 '19 at 13:52
  • $\begingroup$ @CarlMummert - well, I was thinking more of things like $A(n)$ than $n \in A$, but I guess they're the same thing. But then what other formulas would be in the "scheme"? Any formula which you could write using predicates and logical primitives (and/or/not) basically just defines another predicate, so wouldn't the single axiom get everything? $\endgroup$ – Mike Battaglia Mar 10 '19 at 14:34
  • $\begingroup$ The axiom scheme for induction in second-order arithmetic has (the universal closure of) every formula of the form $\phi(0) \land (\forall n) [ \phi(n) \to \phi(n+1)] \to (\forall n)\phi(n)$ where $\phi(x)$ is a formula in the language of second-order arithmetic. $\endgroup$ – Carl Mummert Mar 10 '19 at 15:13

The answers are different syntactically and semantically. We can stick to second-order arithmetic here, but second-order logic in general acts the same.

Semantically, if we work with "full models" then, in each model, we require the second-order part to include all subsets of the first order part. If the model also satisfies the induction axiom $$ \forall A( 0 \in A \land (\forall n)[n \in A \to n+1 \in A]) $$ then the model will satisfy induction for every subset of the first-order part (which, in conjunction with a few other first-order axioms, will force the first-order part to be the standard natural numbers $\omega$).

If we work with "Henkin models" then we allow the second-order part to be a proper subset of the first-order part. The set-existence axioms in the theory then determine which sets of first-order objects must be in the model. But even with the strongest set existence schemes we will not ensure that all subsets of the first-order part are included.

The difference is not so significant when we work syntactically and look at formal proofs instead of models. When we consider full second-order logic syntactically, we often view the set existence axioms as "part of the logic", because our choice of models forces the set existence axioms to hold. But, even though our models now must contain all subsets, in a formal proof we can still only construct some of them - the ones that come from the set existence axioms. So, when we work syntactically, we are essentially in the same position if we look at full models or at Henkin models.


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.