6
$\begingroup$

Modular Arithmetic (MA) has the same axioms as first order Peano Arithmetic (PA) except ∀x(Sx≠0) is replaced with ∃x(Sx=0). Let MA2 be the second-order variation, with second-order induction.

Answering to a question by Russell Easterly, Emil Jerabek has shown that

Even XOR Odd Infinities?

∃x(x≠0∧x+x=0) ∨ ∃x(x+x=S0)

is unprovable in MA. There is, however, a proof in MA2.

There are mathematical examples which distinguish first-order and second-order PA, but they are more esoteric (Paris-Harrington Theorem) or less mathematical (the consistency of first-order PA). So the result of Jerabek seems IMHO to be of interest, by providing a simple mathematical proposition and system where the second-order system can prove the proposition but not the first-order.

Are there other simple examples of a first-order theory T and an assertion S where T cannot prove S but second-order T, with second-order induction, can prove S? (Obviously, the interest of Emil's result increases if there are none which aren't "reasonably" equivalent.)

Improve this question
$\endgroup$
4
  • 6
    $\begingroup$ There is no such thing as “second-order provability”. Second-order logic is not recursively axiomatizable. $\endgroup$
    – Emil Jeřábek
    Commented Jan 24, 2013 at 13:24
  • $\begingroup$ Propositions are provable in what is called "second-Order Arithmetic" but not in "first-order arithmetic", e.g. the consistency of first-order PA. Since you're surely not disputing that fact, I'm not sure what the point of your comment is. Do you have a better suggestion for the title of the question I am asking? $\endgroup$
    – abo
    Commented Jan 24, 2013 at 19:30
  • 3
    $\begingroup$ The issue is that the "second-order arithmetic" in which Con(PA) is provable is a two-sorted first-order theory, and the provability is still first-order provability in that theory. The real difference between first-order logic and second-order logic is only in semantics, not in derivability. Similarly, to talk about provability in MA2 we must write down a set of axioms for MA2, in which case, for the purposes of studying provability, we will want to view MA2 as a two-sorted first order theory with those axioms (because provability is equivalent to validity in first-order semantics). $\endgroup$
    – Carl Mummert
    Commented Jan 24, 2013 at 23:20
  • $\begingroup$ Yes, "second-order arithmetic" is a two-sorted first order theory. Conversely, a particular two-sorted first-order theory is called "second-order arithmetic". That's a fact; it's standard usage by now. You can then ask questions about provability in this two-sorted first-order theory aka "second-order arithmetic." $\endgroup$
    – abo
    Commented Jan 25, 2013 at 6:22

2 Answers 2

Reset to default
7
$\begingroup$

I assume that you mean the second-order system with both second-order induction and the full second-order comprehension scheme. There are many "second order variations" of Peano Arithmetic, with different strengths, so care is required to specify which one is intended. The second-order induction axiom on its own does not allow you to prove any new sentences of first-order arithmetic, compared to Peano Arithmetic, because every model of Peano Arithmetic extends to a model of $\mathsf{ACA}_0$, and that extended model satisfies the second-order induction axiom.

Regardless, there are not going to be any completely elementary principles of number theory that are provable in full second order arithmetic ($Z_2$) but not in PA, because of the well-known phenomenon that all elementary principles are already provable in PA. It is very difficult to find "natural" true mathematical statements that can be expressed in the language of PA but cannot be proved in PA. The Paris--Harrington principle is, in some sense, as good as it gets, which is the main reason the Paris--Harrington theorem is of interest.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ I am not sure that this really adds any interest to the other result mentioned in the question. We know that the theory of rings is "very incomplete", so it is not particularly surprising to find an incompleteness in it that is resolved by adding more axioms. The interest in Peano Arithmetic is that, while it is still incomplete, it does prove virtually every "natural" true statement about elementary number theory, which is what makes it interesting to find anything even half-natural that PA cannot prove. $\endgroup$
    – Carl Mummert
    Commented Jan 24, 2013 at 13:07
  • $\begingroup$ Yes, exactly, the second-order system needs both second-order induction and full second-order comprehension. I understand that PA will not give a good example of what I am looking for. MA does. I'm just wondering whether there are any other examples. $\endgroup$
    – abo
    Commented Jan 24, 2013 at 19:29
4
$\begingroup$

Replacing the induction with the Replacement Schema, it is a nice theorem that if $V_\kappa$ is a model of ZFC with second-order replacement axiom then $\kappa$ is inaccessible.

This is not true for first-order ZFC. In fact for first-order ZFC if there is such $\kappa$ then there is one which has cofinality $\omega$ (the least such cardinal has cofinality $\omega$, and the "next" cardinal with this property - whenever it exists - has cofinality $\omega$ as well).

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ We have to be somewhat careful about something. The result states that if $V_k$ is a model of ZFC2 in full-second order semantics, from the point of view of the metatheory, then $V_k$ is inaccessible, also from the point of view of the metatheory. However, this proof is not itself carried out in ZFC2, it is carried out in the metatheory, and so it does not directly give a statement that is provable in ZFC2 but not in ZFC. In fact the result in the first sentence is a theorem of ZFC, which happens to be a theorem about sets $V_k$ that satisfy ZFC2. $\endgroup$
    – Carl Mummert
    Commented Jan 24, 2013 at 13:11
  • $\begingroup$ Does it still do so indirectly, and if so how? $\endgroup$
    – Adam Epstein
    Commented Jan 24, 2013 at 13:21
  • 2
    $\begingroup$ @Adam Epstein: no, it just doesn't give an example at all; I could have phrased my comment more clearly. The underlying issue is that there is not really such as thing as "second order provability" because there is no effective deduction system that is sound and complete for full second-order semantics. When we want to talk about "provability in ZFC2" we end up working with Henkin (first-order) semantics for ZFC2, basically treating ZFC2 as a two-sorted first-order theory. $\endgroup$
    – Carl Mummert
    Commented Jan 24, 2013 at 13:43

You must log in to answer this question.

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