Are there first-order statements that second order PA proves that first order PA does not? Is this known one way or the other? Could you share an example? (edit: to clarify, by 'second order PA' I don't mean any first order theory)
6
-
6$\begingroup$ Wouldn't Con(PA) be an example? $\endgroup$– Miha HabičCommented Jul 25, 2020 at 23:56
-
$\begingroup$ Why would that be an example? Are you suggesting that the consistency of first order PA is provable from second order PA? Or are you saying something like what Noah Schweber said, that a theory that gets referred to as second order PA/second order arithmetic, a first-order, two-sorted theory Z2, that it proves Con(PA) [,Con(ATR0) , and Con(Π1n−CA0) for each n∈N.]? $\endgroup$– pathwayCommented Jul 26, 2020 at 1:46
-
4$\begingroup$ @pathway Yes, anything you could possibly mean by "second-order PA" is capable of proving $Con(\mathsf{PA})$. $\endgroup$– Noah SchweberCommented Jul 26, 2020 at 2:14
-
4$\begingroup$ There's a clash between "second order PA proves" in the first sentence of your question and "I don't mean any first-order theory" in the edit. What notion of "prove" do you have in mind for 2nd-order PA other than first-order logic plus extensionality and comprehension axioms? Do you just mean "Semantic consequence" without any deductive apparatus for proving things? If so, the first paragraph of @Noah Schweber's answer is all you need. But if you have some sort of "proof" in mind, then I wonder what it might be. $\endgroup$– Andreas BlassCommented Jul 26, 2020 at 2:39
-
1$\begingroup$ @pathway In either sense. The proof system which is sound and complete for Henkin semantics gives us the consistency of first-order PA from second-order PA; a fortiori, the full semantics version of second-order PA entails the consistency of PA. $\endgroup$– Noah SchweberCommented Jul 26, 2020 at 4:28
|
Show 1 more comment
3 Answers
$\begingroup$
$\endgroup$
8
It depends what you mean by "second-order $\mathsf{PA}$." If you really mean full second-order $\mathsf{PA}$, then since that theory characterizes $\mathbb{N}$ up to isomorphism it's complete, and consequently all the sentences first-order $\mathsf{PA}$ doesn't prove (of which there are lots, per Godel) are examples.
However, in my experience people often say "second-order $\mathsf{PA}$" when what they really mean is the first-order, two-sorted theory $\mathsf{Z}_2$, which is annoyingly called "second-order arithmetic." This theory consists of the ordered semiring axioms, the axiom of extensionality, and the comprehension and induction schemes over all two-sorted formulas allowing arbitrary parameters. $\mathsf{Z}_2$ is a computably axiomatizable first-order theory, hence per Godel is not complete.
That said, $\mathsf{Z}_2$ is vastly stronger than $\mathsf{PA}$ even for first-order sentences. The most obvious examples are consistency principles: among others, $\mathsf{Z}_2$ proves $\mathsf{Con(PA), Con(ATR_0)}$, and $\mathsf{Con(\Pi^1_n-CA_0)}$ for each $n\in\mathbb{N}.$ That said, keep in mind that $\mathsf{PA}$ is quite strong - there are very few sentences in the language of first-order arithmetic which are independent of $\mathsf{PA}$ and are "natural" (and in particular aren't consistency/soundness/etc. principles). Of course, this last bit is subjective, and Harvey Friedman for example would argue that there are actually lots of these, but in my opinion they're not really that natural.
answered Jul 26, 2020 at 0:14
-
$\begingroup$ That's not right, what you said about 'theories which characterize N are complete.' Second order PA has one model, the standard natural numbers, but it's incomplete. $\endgroup$– pathwayCommented Jul 26, 2020 at 2:12
-
5$\begingroup$ @pathway No, you're incorrect. It's incomplete with respect to the proof system for the Henkin semantics, but in the full semantics it is complete. (Put another way: when dealing with the full semantics we don't talk about a proof system, because there is no good proof system for the full semnatics; when people talk about "the proof system for second-order logic" what they really mean is a particular proof system which is sound and complete for the Henkin semantics, and it's not really relevant in the full semantics.) $\endgroup$ Commented Jul 26, 2020 at 2:13
-
1$\begingroup$ @pathway It implies the consistency of first-order PA, but I'm not actually certain it's equivalent to it. Regardless, I would agree with Andres that it's quite natural - when I said "they're not really that natural" I was referring specifically to the sentences Friedman has introduced, at least those I'm familiar with. $\endgroup$ Commented Jul 26, 2020 at 4:27
-
1$\begingroup$ @bof Yes, but to be honest I would conjecture that there are very few natural examples at all. E.g. the current guess, to my understanding, is that Fermat's last theorem is indeed provable in $\mathsf{PA}$. Leaving aside the "generalized Ramsey theory" side of things, I can't think of any "natural" arithmetic sentence which I actually think is plausibly independent of $\mathsf{PA}$. (Although of course I'd love to be surprised!) $\endgroup$ Commented Jul 26, 2020 at 5:23
-
1$\begingroup$ @MadHatter Already second-order PA is galactic overkill - even first-order PA is overkill; see the discussion here. Note that we have to be a bit careful here - of course (first-order) $\mathsf{PA}$ doesn't prove "$\mathsf{PA}$ is incomplete." What it does prove is "If $\mathsf{PA}$ is consistent, then $\mathsf{PA}$ is complete," and more generally "Every computably axiomatizable consistent theory interpreting Robinson arithmetic is incomplete." (And similarly with G's second IT.) $\endgroup$ Commented Feb 16, 2021 at 18:29
$\begingroup$
$\endgroup$
1
This question more or less reduces to asking for natural arithmetic statements unprovable in PA. A very interesting but lesser-known example that I learned about recently concerns fusible numbers. The term "fusible" may be unfamiliar but it arises as a natural generalization of a well-known puzzle involving measuring lengths of time by burning fuses (finite pieces of string) of different lengths. The puzzle is an old one and was not specifically constructed to produce unprovable statements, so the unprovable statements involving fusible numbers are arguably the most "natural" PA-unprovable statements around.
answered Jul 26, 2020 at 16:37
-
$\begingroup$ Nice one. I didn't see this before! It's curious how the fuse puzzle can lead to trees representing the ordering of $ε_0$. $\endgroup$ Commented Jun 19, 2021 at 18:30
$\begingroup$
$\endgroup$
According to Wikipedia, Goodstein's Theorem is provable from second order arithmetic, and since it implies Con(PA), PA can't prove it, assuming that PA is consistent. "Kirby and Paris showed that [Goodstein's Theorem] is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic)."