2
$\begingroup$

Context (from https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic#From_the_incompleteness_theorems):

The incompleteness theorems show that a particular sentence G, the Gödel sentence of Peano arithmetic, is not provable nor disprovable in Peano arithmetic. By the completeness theorem, this means that G is false in some model of Peano arithmetic. However, G is true in the standard model of arithmetic, and therefore any model in which G is false must be a non-standard model.

I roughly understand the above, but some finesses about first vs. second order logic escape me. "G is true in the standard model" is related to the use of the second order logic, but how exactly? I am looking for high level explanations/considerations/examples rather than technicalities.

Question 1: The "Peano arithmetic" is a first order theory which, if augmented with the second order axiom of induction, yields exactly the "standard model of arithmetic". Is it correct? What are the major differences between both theories (typical statement whose proof requires the second order induction)?

Question 2: Why is G true in the standard model of arithmetic, whereas it may or may not be true in the Peano arithmetic? Does the Gödel encoding requires the standard model of arithmetic? What part of the argument (proof of Gödel's incompleteness theorem) fails in the Peano arithmetic?

$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

I think you may be confused about the difference between models and theories. A theory is simply a set of sentences, while a model is a set with interpretations for all relevant symbols. E.g. in this context:

  • Our language is the language of arithmetic $\mathcal{L} = \{ 0, 1, +, \times, < \}$
  • PA is a theory in this language (definition can be found on Wiki)
  • The standard model $\mathbb{N}$ is a structure in this language, where we interpret all the symbols with their usual meanings.

A key difference is that models have to have an opinion on every formula, since we have a way of assigning truth values to any formula. However, theories do not - it is possible that both $\psi$ and $\lnot\psi$ could be consistent with some theory. Such a theory is called incomplete.

Now, to answer your questions:

  • PA is indeed a first order theory. It is not categorical, meaning that it has non-isomorphic models (the so-called nonstandard models of arithmetic). If you add the second-order induction axiom, you get a categorical theory, since the only model is $\mathbb{N}$. However, PA$^+$ and $\mathbb{N}$ are not the same - the former is a theory, while the latter is the unique model of that theory.

  • G is true in $\mathbb{N}$ just cause it happens to be - remember every formula has to be either true or false in a given model. However, both G and its negation are consistent with PA, i.e. there are models of PA+G (such as $\mathbb{N}$), and also models of PA+(not G) - a nonstandard model. Therefore, just from PA we can't decide if G is true or false - it's consistent either way.

  • I think the Gödel encoding can be done in PA (hence in nonstandard models), so it wouldn't require the standard model $\mathbb{N}$.

  • The actual proof of Gödel's theorem happens in some "metatheory" which is outside of arithmetic. So, it's wrong to ask about the proof of GIT failing in PA, since the proof is not carried out in PA. The formula G is a formula in the language of arithmetic which is not provable from PA. However, note that G is not the proof of GIT, but just an object constructed as part of this proof.

$\endgroup$
6
  • $\begingroup$ For the theory PA+, G cannot be proved or disproved because it encodes "G is not provable in PA+" (and a fortiori "G is not provable in PA"). Since N is the only model of PA+, either G or (not G) is a semantic consequence of PA+. The proof of GIT shows that G is true in N, based on the idea that if G where false, then there would be a proof of G. The proof (in the meta-theory) that G is true in N is thus indirect. But in a model of PA, G may well be false, and in this case, it somehow does not follow that G is provable. A subtle difference still escapes me. $\endgroup$
    – Loic
    Sep 12, 2021 at 20:20
  • $\begingroup$ By PA$^+$, I meant PA plus the second-order induction axiom that you stated. I think G is provable in PA$^+$ but not in PA. I'm not quite sure what you're confused about - G is not provable in PA since there are models of PA in which G is true, and also models of PA in which G is false. $\endgroup$
    – Jordan Mitchell Barrett
    Sep 12, 2021 at 22:46
  • $\begingroup$ I though that G is a semantic consequence of PA+ (that is, G is true in N, the essentially unique model of PA+), but that G is not provable from the axioms of PA+. That is an very important point, is G provable in PA+, or only a semantic consequence? What I do not understand: How can be established that G cannot be false in the essentially unique model N of PA+ (based on the idea that G encodes "G has no proof"), and how does the same argument fail for a model of PA. Somehow, that fact that PA+ is categorical and that PA is not plays a role, but it escapes me. $\endgroup$
    – Loic
    Sep 13, 2021 at 18:17
  • 1
    $\begingroup$ Okay, you're right that G is a semantic consequence of PA$^+$. Provability can only be determined with respect to a given proof system, and in the case of second-order logic, there are multiple inequivalent systems that could be a sensible choice. In fact, there are even multiple ways to give semantics to SOL. So you'd have to state what proof system you're talking about. $\endgroup$
    – Jordan Mitchell Barrett
    Sep 14, 2021 at 15:04
  • 1
    $\begingroup$ I don't know the details of the GIT proof, so I don't think I can help any further. Maybe you could open a new question focusing on the specifics of the proof: "How can be established that G cannot be false in the essentially unique model N of PA+ (based on the idea that G encodes "G has no proof"), and how does the same argument fail for a model of PA" $\endgroup$
    – Jordan Mitchell Barrett
    Sep 14, 2021 at 15:05
1
$\begingroup$

I read a bit more about Gödel's proof, and I think that I can reasonably well answer my own questions now.

Question 1: PA+ (PA with the second order axiom of induction) has an essentially unique model, namely N, the standard model of arithmetic. Any model of PA contains N (up to isomorphism), and may contain additional exotic elements. The difference between N and a non-standard model is precisely the presence (in a non-standard model) resp. the absence (in the standard model N) of exotic elements. A typical claim which does not hold in a non-standard model is: Any number is a descendant (by iterative application of the successor function) of zero.

Question 2: The image of a Gödel encoded number/formula/proof is, by construction, a natural number, such that an exotic number cannot be the encoding of anything. It is impossible for a natural number to disprove G, because in this case, the natural number in question would encode a proof of G, which then would yield a plain contradiction. But it is well possible for an exotic number to disprove G, since this exotic number is not the Gödel encoding of anything (in particular, it does not yield a proof of G).

Remark: Both (PA and G) and (PA and not G) are consistent first order theories, which thus have models. That is, some (non-standard) model of PA exists where G is false.

$\endgroup$
4
  • 1
    $\begingroup$ Re: your last paragraph, in fact $G$ is provable in second-order Peano arithmetic (your "$\mathsf{PA^+}$"), although "provable" is a bit of an odd term to use where second-order logic is concerned. $\endgroup$
    – Noah Schweber
    Sep 17, 2021 at 14:23
  • $\begingroup$ @NoahSchweber Yes, there is some problem in my argumentation about the provability in PA+. If I understand correctly, G depends on a given theory (in which natural numbers can be described), and G cannot be proved in the theory in question (which may or may not be PA+). Is it correct, in your opinion? Must the underlying theory be a first-order theory? I think that G is a semantic consequence of PA+ (true in N), but is it really provable from the axioms of PA+? Under which exact hypotheses? $\endgroup$
    – Loic
    Sep 17, 2021 at 16:26
  • 1
    $\begingroup$ "Must the underlying theory be a first-order theory?" Short version, yes. There is a more abstract version of GIT which applies to general logics, but it's significantly more complicated. Since $\mathsf{PA}^+$ is not a first-order theory, it's unclear what "provable from the axioms of $\mathsf{PA^+}$" should mean if not "semantically entailed by $\mathsf{PA^+}$." One option is to use the Henkin proof system (which is sound but not complete for the standard second-order semantics); in this sense $G$ is not $\mathsf{PA^+}$-provable but this takes some thought. $\endgroup$
    – Noah Schweber
    Sep 17, 2021 at 16:37
  • $\begingroup$ @NoahSchweber Thank you so much. I will adapt my answer accordingly. $\endgroup$
    – Loic
    Sep 17, 2021 at 18:24

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.