11
$\begingroup$

Forgive the elementary nature of the question. I understand that the second order Peano Axioms are categorical in the sense that all their models are isomorphic. This equivalence class of models is taken to be the definition of natural numbers.

My question is that: Is the theory defined by those second order axioms complete? i.e. is every second-order statement in this theory provable or disprovable from the axioms?

For the first order Peano Arithmetic axioms any statement that is true in all models is provable or disprovable by the completeness of first-order logic, but of course this is in applicable to the second-order axioms.

Improve this question
$\endgroup$
4
  • $\begingroup$ To clarify: I am asking about syntactic completeness in the sense that there exists a proof for every true statment, using a suitable proof system. $\endgroup$
    – Mohamed Alaa El Behairy
    Commented Feb 7, 2010 at 15:32
  • 2
    $\begingroup$ For a clear answer, you would need to explain your 'suitable proof system' or, at least, your requirements for 'suitable'. Indeed, one of the principal difficulties with second-order logic is that every proof system is unsuitable in one way or another. The answer to your question depends on what you're willing to give up for completeness. $\endgroup$
    – François G. Dorais
    Commented Feb 7, 2010 at 15:49
  • $\begingroup$ @François G. Dorais: Can you provide some more detail for your comment, either in another comment or in an answer? Specifically, can you describe the options as to what I can give up and get in exchange? Thanks in advance. Incidentally, I appreciate your contributions to this site very much. $\endgroup$
    – aorq
    Commented Feb 7, 2010 at 23:37
  • 3
    $\begingroup$ @Charles: Any complete proof theory for second-order logic is necessarily (1) infinitary, since compactness fails for second-order logic, and (2) almost indescribable, so as to avoid diagonalization arguments similar to Gödel's Theorem. The requirements are so bad that it is often claimed that there is no such system, though this claim is technically wrong without some implicit assumptions on what constitutes a deductive system. A trivial complete deduction system is the semantic consequence relation itself, but that doesn't help much... $\endgroup$
    – François G. Dorais
    Commented Feb 8, 2010 at 0:08

3 Answers 3

Reset to default
8
$\begingroup$

Note that there are two different types of models of second-order logic: standard models, where second-order quantified variables range over all subsets of the domain; and Henkin models, where second-order quantified variables are allowed to range over a proper subset of the full power-set.

Henkin proved the completeness theorem for second-order logic for Henkin models, so if a sentence is true in all Henkin models, it is derivable. For completeness to hold, it is not enough to consider only standard models, so even though second-order PA is categorical for standard models, it is not complete (as we would expect, this being a corollary Gödel's theorem).

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Henkin models, and multisorted logic, are normally defined using the lambda-calculus, which is to say that the second-order constructions arise from a type-theoretical intuition about what is formally derivable. Second-order arithmetic is defined in multisorted logic. $\endgroup$
    – Charles Stewart
    Commented Feb 10, 2010 at 8:39
  • $\begingroup$ Very helpful answer, thanks Ulrik! I would just add the the historical description of SOL as "categorical" is a bit paradoxical, since a reasonable person would understand this to mean that there are no nonstandard models, but I guess the idea was that the standard notion of "predicate" was taken as part of the definition of SOL. So, I guess SOL isn't really categorical in any sense that I would characterize as "reasonable", sc. one where you take the definition of predicate-hood as part of the content of a model. $\endgroup$
    – Jonathan Sterling
    Commented Jun 3, 2016 at 18:46
4
$\begingroup$

Between them, the previous comments and replies have already covered all of the relevant points, but here in any case is a direct, unsophisticated answer:

Any effective procedure (i.e. anything you could program up) for proving statements of second-order logic must be incomplete (unless it proves false statements). Otherwise, because second-order arithmetic is categorical, we would have an effective procedure for determining the arithmetic truth. But this is impossible by Gödel's first incompleteness theorem.

Improve this answer
$\endgroup$
3
$\begingroup$

If a theory has only one model, then of course it is complete, in the sense that any statement or its negation is a consequence of the theory, because either it holds in the unique model or it doesn't.

As you mention, there is only one model of second-order PA, and this is the model of the natural numbers. Thus, second-order PA is complete for first order assertions.

One can easily extend this to second-order assertions by observing that any isomorphism of the first-order structures will extend to an isomorphism of the second order structures also, if one decrees that the second-order part of the structures should contain all subsets. Thus, there is up to isomorphism only one second-order structure of second-order PA, and so the theory is complete for second-order assertions.

BUT, there are interesting things still to say about incompleteness. And the reason is that the concept of second-order is a set-theoretic concept, and so the question of which statements are true in this unique second-order model of second-order PA will exhibit many set-theoretic independences. That is, ZFC proves that the theory of the natural numbers is a complete theory, but different models of ZFC will have their natural numbers satisfying different statements. This is true already in the first order theory, since some models of ZFC will have the arithmetic statement Con(ZFC) being true in their natural numbers, but others will have the negation of this being true in their natural numbers.

Because of this kind of issue, many logicians prefer to understand the second-order theory in a first-order way, by saying that one specifies a second-order model by giving first it's first order part, and then also specifying the collection of subsets that are to be used as the interpretation of the second-order part. Thus, a second-order model of PA consists of a first order structure (N,+,.,<,0,1) together with a collection S of subsets of N, to be used for interpreting the second-order quantifiers over subsets. In this weaker sense of second-order, one loses the categoricity, and there can be non-standard models again even in the first-order part.

Improve this answer
$\endgroup$
2
  • $\begingroup$ To clarify: the second order PA is semantically complete, but i am asking about syntactic completeness in the sense that every true statement has a proof using a suitable proof system. As to the set-theoretic issues, does this mean that for every model of ZFC we have a different unique model of the PA? if so is there a canonical model of ZFC which defines the true natural numbers? or is it just a question of what subsets each model allow and they agree on all non-second-order statements $\endgroup$
    – Mohamed Alaa El Behairy
    Commented Feb 7, 2010 at 15:48
  • 2
    $\begingroup$ @Mohamed: Con(ZFC) is a first-order statement, so two models of ZFC need not even agree on first-order theory of the natural numbers. $\endgroup$
    – François G. Dorais
    Commented Feb 7, 2010 at 17:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .