Many examples are now known of sentences undecidable in Peano's Arithmetic (PA) assuming that PA is consistent. Are some or all of these sentences also undecidable in Second Order Arithmetic (SOA) if SOA is consistent? I am interested in this question because SOA is an axiomatizable theory even though it contains some of the axioms of second order logic-whose set of universally valid sentences is not recursively enumerable. If s is a sentence undecidable in SOA which asserts that all positive integers have a certain property, what could we say about the smallest positive integer n that is asserted by the negation of s to fail to have this property? There are models of PA which contain n as an "infinite" positive integer. But are there any models of SOA which contain "infinite" positive integers? It seems that I do not fully understand the model theory of SOA.
-
1$\begingroup$ You need to be more specific about which type of second order semantics you want to use. In full SOA, $\omega$ is the only model, but then you don't have a complete proof calculus as in first order logic. $\endgroup$– Christian RemlingCommented Jul 23, 2015 at 17:59
-
$\begingroup$ You can formalize the sentence "SOA is consistent" in PA. That sentence is of course undecidable in SOA. $\endgroup$– user76367Commented Jul 24, 2015 at 2:28
3 Answers
Since you're asking about provability in SOA, you're presumably referring to a standard deduction system, such as the one in Steve Simpson's book, which is sound not only for the standard (or "full") semantics but also for Henkin semantics.
The most natural example of a sentence undecidable in SOA is "SOA is consistent". It's unprovable because of Gödel's second incompleteness theorem, and it's not refutable because it's true.
Gödel's second incompleteness theorem and his completeness theorem together imply that some nonstandard models of SOA contain nonstandard integers n satisfying the formula that expresses "n is the Gödel number of a proof of a contradiction on SOA.
-
3$\begingroup$ Note that Gödel's paper on the incompleteness theorems is, as indicated in its title, about Principia Mathematica and related systems. Principia Mathematica is considerably stronger than SOA. $\endgroup$ Commented Jul 23, 2015 at 18:44
-
1$\begingroup$ "...and it's not refutable because it's true." really? How does one get this? $\endgroup$– David Roberts ♦Commented Jul 24, 2015 at 5:26
-
2$\begingroup$ @DavidRoberts The facts that Con(SOA) is true, that all axioms of SOA are true, that logical inference preserves truth, and that therefore Con(SOA) cannot be refuted in SOA are all provable in the usual foundational system for mathematics, ZFC. (They're also provable in far weaker systems,but I don't think that's needed to answer "How does one get this?") $\endgroup$ Commented Jul 24, 2015 at 14:50
-
$\begingroup$ OK, thanks. I was worried you had access to some higher truth somehow, rather than working in ZFC. $\endgroup$– David Roberts ♦Commented Jul 25, 2015 at 1:51
Actually I misread your post above: per Christian Remling's comment, it's not clear what you mean by SOA. That term usually refers to a first-order theory whose objects are natural numbers and sets of natural numbers (but not sets of sets, etc). It is recursively enumerable and subject to the incompleteness theorems, so it has nonstandard models with nonstandard or "infinite" positive integers. That's the theory in Steve Simpson's book that Andreas also refers to. The Wikipedia article is very good:
https://en.wikipedia.org/wiki/Second-order_arithmetic
If you mean the historical Peano axioms that use second-order logic for the induction axiom, then assuming full second-order semantics, that theory is categorical (it has exactly one model, the standard naturals). But second-order logic doesn't have the completeness or compactness theorems, and it is sometimes called "set theory in sheep's clothing". To prove theorems in the usual sense of the word, you have to fix a first-order, r.e. axiomitazation of the fragment of set theory that you use to discuss sets of natural numbers. But then you're back in the land of incomplete theories with nonstandard models.
Finally there is so-called "true arithmetic" (TA), the complete, non-r.e., first-order theory of $\bf N$. This has just one countable model, the standard integers. But by upward Löwenheim–Skolem, it has models of every infinite cardinality. First-order logic just can't tell the whole story of $\bf N$.
-
$\begingroup$ This is mostly true, but the last paragraph is wrong: TA has lots of nonstandard countable models. $\endgroup$ Commented Jul 24, 2015 at 16:35
-
$\begingroup$ Many thanks for your answers which have given me alot to think about. I thought that Hilbert and Bernays presented the first formalized and axiomatizable version of what I call SOA. You do not mention whether any of the interesting examples of sentences such as the Paris-Harrington theorem or Goodstein's theorem-which have been shown to be undecidable in PA-are also undecidable in SOA. Finally, does every axiomatizable theory-even if based upon higher order logic-have non-standard models which contain "infinite" positive integers? $\endgroup$ Commented Jul 24, 2015 at 18:09
-
$\begingroup$ The question at the end of my previous comment is not quite what I meant to ask. I meant to ask whether every consistent and axiomatizable extension of PA-even if based upon higher order logic-has non-standard models which contain "infinite" positive integers. I am not too sure about exactly what Godel's incompleteness theorem and model theory have to say regarding consistent and axiomatizable extensions of PA that are not based upon first order logic. $\endgroup$ Commented Jul 25, 2015 at 17:32
-
$\begingroup$ I am really trying to avoid theories in which second order axioms are "represented $\endgroup$ Commented Jul 26, 2015 at 18:31
Garabed, regarding your recent comments, this is pretty basic stuff and maybe you want to try MathSE for further discussion. But,
1) yes, there are known interesting sentences in the language of PA that are undecidable in SOA or even ZFC. Obvious ones like Con(ZFC) of course, but also various more "mathematical" ones that Harvey Friedman has been collecting for years: https://u.osu.edu/friedman.8/files/2014/01/Putnam062115pdf-15ku867.pdf
2) all countable nonstandard models of PA contain "infinite" elements, see here.
3) The 19th century Peano axioms (that use second-order logic) have no nonstandard models (all models are isomorphic to one another). The trouble is that this doesn't get you any closer to knowing arithmetic truth, because you don't have an axiomatic way to nail down "true" universe of relations that the second-order quantifiers actually range over. If by "axiomatizable extensions of PA that are not based upon first-order logic" you mean you're going to study the second-order sentences using a first-order axiomitazation of set theory, then yes, you get the usual incompleteness and nonstandard models.
Noah Schweber, whoops, of course you're right. Since TA is complete, all its models satisfy the same set of first-order sentences (elementary equivalence), but they aren't necessarily isomorphic.
-
$\begingroup$ I am really trying to avoid theories in which second order axioms are "represented" by first order axiom schemes. These are actually first order theories. $\endgroup$ Commented Jul 26, 2015 at 18:39