Edit After Andreas Blass answer below and comments below the original post I have changed it to accommodate posters' remarks. I hope it is clear and makes more sense now.

Let $\mathrm{PA}$ be the first-order Peano Arithmetic with full induction schema. Let $\mathrm{Con(PA)}$ be the standard $\Pi_1$ consistency statement for $\mathrm{PA}$. By the 2nd Incompleteness Theorem we know that $\mathrm{PA}\nvdash \mathrm{Con(PA)}$, if only $\mathrm{PA}$ is consistent. Therefore (assuming consistency of $\mathrm{PA}$) the theory $\mathrm{PA^+}=\mathrm{PA}+\neg\mathrm{Con(PA)}$ is consistent and has a model. This theory is $\omega$-inconsistent, since we know that no natural number codes a proof of, say, '$0=1$', therefore for every number $n$ we have that $\mathrm{PA}\vdash\neg\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},\overline{n})$, where $\mathrm{Proof}(x,y)$ represents in $\mathrm{PA}$ recursive relation: $y$ codes a proof of a formula whose number is $x$; yet $\mathrm{PA^+}\vdash\exists y\,\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},y)$. Thus in a model $\mathfrak{M}$ of $\mathrm{PA^+}$ there is a non-standard number which codes a proof of '$0=1$'.

I have the following questions:

  • How can I interpret $y$ is coding a proof of `$0=1$' in this situation?

My questions is motivated by the following. $\mathrm{Proof}(x,y)$ represents derivability relation for Peano Arithmetic; in case $\mathrm{PA}$ is consistent there cannot be a PA-proof of `$0=1$'. So can I choose an arbitrary non-standard number $q$ to serve as interpreting the variable $y$ in $\mathrm{Proof}(\overline{\ulcorner0=1\urcorner},y)$ and satisfying the formula in question? Or is this interpretation determined in some other way?

  • 1
    $\begingroup$ Careful! All that the the 2nd incompleteness theorem tells you is that $Con(PA)$ is unprovable, not that it is independent, and this provided you already accept the consistency of PA. If you apply that theorem to your theory $PA^+$ instead, you can only conclude that $Con(PA^+)$ is unprovable in $PA^+$, because in fact $\neg Con(PA^+)$ is actually provable there. $\endgroup$ – godelian Sep 25 '14 at 12:06
  • $\begingroup$ @godelian Yes, you are right - from 2nd GIT we only get that $PA$ does not prove $Con(PA)$ and I assumed consistency tacitly (I edited the question accordingly). But that does not influence the gist of the question, does it? $\endgroup$ – Mad Hatter Sep 25 '14 at 12:53
  • 1
    $\begingroup$ I don’t understand “these won’t lead us beyond standard natural numbers”. Standard numbers code standard proofs and formulas, nonstandard numbers code nonstandard formulas and proofs (that is, of nonstandard length). What should lead from where to where? $\endgroup$ – Emil Jeřábek Sep 25 '14 at 13:19
  • $\begingroup$ @emil $Proof(x,y)$ represents <<PA-derivability>> relation: standard number $n$ codes a PA-proof of a formula coded by standard number $k$. This relation holds for proofs of $PA$. When we consider $PA^+$ and its model, then there must be an element $q$ of the model for which $Proof(\overline{\ulcorner 0=1\urcorner},\overline{q})$. But there cannot be such a proof if $PA$ is consistent. Does it mean that we can take any non-standard number to serve as $q$? There's something basic I cannot grasp here... $\endgroup$ – Mad Hatter Sep 25 '14 at 13:53

The witness coding a proof of 0=1 in a nonstandard model is likely to be very specific; depending on your encoding, most nonstandard numbers may not code proofs at all. And even if all numbers encode proofs, many nonstandard numbers will encode proofs of true formulas, or of other false formulas.

The encoding of proofs that you've chosen reduces proofs to some combinatorial structure, and that structure is still around in the nonstandard model. For instance, say you've decided that $q$ encodes a proof if $q$ has the form $$2^{q_1}3^{q_2}5^{q_3}\cdots p_n^{q_n}$$ where each $q_i$ encodes a formula and $q_{i}$ is derived from $\{q_j\}_{j<i}$ by some finite list of operations. If this is the encoding, a nonstandard $q$ only encodes a proof if it is of this form, but with $n$ a nonstandard number.

In this case $q$ actually describes a list of steps where each step follows from the ones above it; the problem is that this list isn't well-founded, so it doesn't correspond to a genuine proof. But you can still ask questions like "what is the 7th step" (and also, what is the $a$-th step for $a$ a nonstandard integer $\leq n$), and the 8th step really does follow from steps $1,\ldots,7$.

  • 2
    $\begingroup$ Of course, some of the steps may also be nonstandard instances of axiom schemes, such as nonstandard instances of the induction scheme or nonstandard tautologies. $\endgroup$ – Carl Mummert Sep 25 '14 at 23:23
  • $\begingroup$ In case $n$ is a non-standard number, does $q_n$ code a non-standard formula? $\endgroup$ – Mad Hatter Sep 27 '14 at 8:04
  • $\begingroup$ @MadHatter: Not necessarily. $\endgroup$ – Henry Towsner Sep 27 '14 at 19:28
  • $\begingroup$ I think that the nonstandard proof of 0=1 could have standard finite n, with some nonstandard q_i. $\endgroup$ – Joel David Hamkins Sep 28 '14 at 0:50
  • 2
    $\begingroup$ @PyRulez PA proves each the consistency of each standard-finite fragments. But in a nonstandard model, it is not generally true that the model thinks every nonstandard finite subset of its version of PA is consistent, and this fails in the models of $\neg$Con(PA). $\endgroup$ – Joel David Hamkins Feb 18 '18 at 6:56

Your two questions should probably be answered together, because "coding a proof" makes sense in any model of PA, whereas "coding" and "proof" alone require us to go outside the model, decoding a number as a (possibly nonstandardly long) string of symbols. But "$x$ codes a PA-proof" is expressed, thanks to Gödel, as a formula $\phi(x)$ in the language of PA. To say that an element $q$ in a non-standard model $\mathfrak M$ of PA codes a PA-proof is just so say that $\phi(x)$ is true in $\mathfrak M$ when $x$ is interpreted as denoting $q$.

  • $\begingroup$ Could you please write something more about the difference between "coding a proof" and ""coding" and "proof""? $\endgroup$ – Mad Hatter Sep 25 '14 at 13:57
  • 2
    $\begingroup$ @MadHatter "Coding a proof" is a property of just numbers (in the standard model). "Coding" refers to a relationship between numbers and strings of characters. "Proof" refers to a property of just strings of characters. PA is about numbers, not about strings of characters, so it can express "coding a proof" but not "coding" and "proof" individually. (After one sets up the coding machinery, one can use it to translate statements about character strings into PA, but that doesn't help when coding itself is in question.) $\endgroup$ – Andreas Blass Sep 25 '14 at 14:00
  • $\begingroup$ I get your point now. Yes, I indeed should ask about the meaning of "coding a proof". $\endgroup$ – Mad Hatter Sep 25 '14 at 14:08
  • $\begingroup$ The choice of $q$ may be done arbitrarily, in the sense of just choosing any non-standard number as an interpretation of variable $y$ in $\mathrm{Proof}(\overline\ulcorner 0=1\urcorner,y)$? $\endgroup$ – Mad Hatter Sep 25 '14 at 14:50
  • 1
    $\begingroup$ If you work with a specific $\mathfrak M$, then the operations and relations that come with $\mathfrak M$ determine which elements $q$ will code PA-proofs. If, on the other hand, you don't fix a specific $\mathfrak M$, then it's not clear what would be meant by "non-standard elements". $\endgroup$ – Andreas Blass Sep 25 '14 at 15:49

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.