1
$\begingroup$

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?

$\endgroup$
4
  • 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, 2014 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$ Sep 25, 2014 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$ Sep 25, 2014 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$ Sep 25, 2014 at 13:53

2 Answers 2

8
$\begingroup$

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$.

$\endgroup$
11
  • 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$ Sep 25, 2014 at 23:23
  • 1
    $\begingroup$ @MadHatter: Not necessarily. $\endgroup$ Sep 27, 2014 at 19:28
  • 1
    $\begingroup$ I may misremember the details, but my understanding is that for usual Hilbert-style proof systems (and similar), a proof with a standard number of lines is a sort of a substitution instance of a standard proof (which is essentially the most general unifier of the proof skeleton), and in particular, it cannot be a proof of a contradiction. $\endgroup$ Sep 29, 2014 at 10:38
  • 1
    $\begingroup$ Yes, more or less. See Theorems 2.1, 2.2 in karlin.mff.cuni.cz/~krajicek/scan8.pdf . The result only bounds the depth of the formulas occurring in the proof, but that’s enough to conclude that a model of PA cannot contain a PA-proof of contradiction (or of any unprovable standard formula for that matter) with a standard number of steps, as PA has truth predicates for formulas of bounded depth. $\endgroup$ Sep 29, 2014 at 12:21
  • 3
    $\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$ Feb 18, 2018 at 6:56
6
$\begingroup$

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$.

$\endgroup$
7
  • $\begingroup$ Could you please write something more about the difference between "coding a proof" and ""coding" and "proof""? $\endgroup$ Sep 25, 2014 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$ Sep 25, 2014 at 14:00
  • $\begingroup$ I get your point now. Yes, I indeed should ask about the meaning of "coding a proof". $\endgroup$ Sep 25, 2014 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$ Sep 25, 2014 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$ Sep 25, 2014 at 15:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.