5
$\begingroup$

Why if provable(P) then provable(provable(P))?

I was reading Godel's incompleteness theorem explained in words of one syllable and came across this assertion (near the end of the first paragraph):

In fact, if a claim can be proved, then it can be proved that the claim can be proved.

Can you give a proof (or a counterexample if it's false)?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ I'm puzzled: why is our proof of P not already a proof, of the best sort, that P is provable? $\endgroup$
    – John Bentin
    Commented Dec 20, 2010 at 12:05
  • 1
    $\begingroup$ @John Bentin: the answer by Zhen Lin explains this. It's an issue of metatheory vs object theory in formal logic. $\endgroup$
    – Carl Mummert
    Commented Dec 20, 2010 at 12:12
  • $\begingroup$ @Carl Mummert: Thanks for explaining this. I skipped Zhen Lin's answer earlier because I was put off by the "square" notation. Now I see that he bypasses this anyway. $\endgroup$
    – John Bentin
    Commented Dec 20, 2010 at 14:17
  • 1
    $\begingroup$ If the (good!) answers below don't give you enough information to satisfy you, then the keyword "Hilbert-Bernays provability" may help you locate relevant literature. The Hilbert-Bernays provability conditions list the requirements to prove Goedel's second incompleteness theorem, and one of them is that your theory be able to prove Prov(x) => Prov(Prov(x)). $\endgroup$
    – Timothy Chow
    Commented Dec 20, 2010 at 16:34
  • $\begingroup$ Actually, now that you point that out, I've realised that there are actually two questions here. The quote talks about the first Hilbert—Bernays condition, that for every true sentence P, we have Prov(#P)... but the title of the question is the second Hilbert—Bernays condition, which is rather more interesting, because it says for any sentence P whatsoever (even false ones!), Prov(#P) => Prov(#Prov(#P)). $\endgroup$
    – Zhen Lin
    Commented Dec 20, 2010 at 16:51

4 Answers 4

Reset to default
11
$\begingroup$

We work with Peano arithmetic PA. Following Goedel, in PA we can define a primitive recursive relation $\mathrm{Prf}(m,n)$ such that Peano arithmetic proves $\mathrm{Prf}(m,n)$ if, and only if, $n$ is the Goedel code of a proof of the statement whose Goedel code is $m$. This much you have to take on trust, or look it up in a book.

Now suppose a statement $\phi$ is provable. Then it has a proof $p$. From $\phi$ and $p$ we can compute their Goedel codes $m$ and $n$, respectively. Because $p$ is a proof of $\phi$, it follows that $\mathrm{Prf}(n,m)$ is provable in PA.

More generally, we can ask your question in the language of Provability logic, namely is it the case that $\square \phi \Rightarrow \square \square \phi$ (the modal operator $\square$ means "it is provable that"). The answer is positive, as this is known as the K4 axiom of modal logic, and it is part of Provability logic.

Improve this answer
$\endgroup$
7
  • $\begingroup$ You are saying if Q then provable(Q). This is stronger than what I'm asking and you didn't prove it before using it. Axiom? I'm looking for a proof.... $\endgroup$
    – Zirui Wang
    Commented Dec 20, 2010 at 11:32
  • $\begingroup$ @Zirui Wang: This answer is what I would write for the question as I read it. I think you need to clarify the question if you're looking for something else. You can ignore the final paragraph: the second paragraph explains how you would use a proof of a formula $\phi$; in PA to construct a proof the "$\phi$ is provable" in PA. Because the original proof is finite, you put it into a Goedel number and then prove things about the Goedel number by inspection. $\endgroup$
    – Carl Mummert
    Commented Dec 20, 2010 at 12:20
  • 4
    $\begingroup$ @Zirui: With all respect, no, I am not saying "if $Q$ then $\mathrm{provable}(Q)$". Please read my answer carefully. My initial assumption is "Suppose $\phi$ is provable." and not "suppose $\phi$ is true", as you claim. I have answered exactly what you asked. If you meant to ask something else, then try again. $\endgroup$
    – Andrej Bauer
    Commented Dec 20, 2010 at 17:39
  • 1
    $\begingroup$ I think it would be best if you read a suitable book about Goedel's encoding of provability inside PA. Yes, I am sure that PA proves $\mathrm{Prf}(m,n)$ if $n$ codes a proof of a statement coded by $m$. To answer your second question: "$\phi$ is provable" means "there exists a proof $p$ of $\phi$" (outside PA). So if I assume that $\phi$ is provable then I am allowed to conclude that there is a proof $p$ (outside PA) of $\phi$. From such a $p$ I can construct a number $n$ which is the Goedel code of $p$. This $n$ represents $p$ inside the formal system PA. $\endgroup$
    – Andrej Bauer
    Commented Dec 23, 2010 at 14:24
  • 2
    $\begingroup$ @Zirui: You seem to have doubts about very standard material in logic. Perhaps the doubts will go away after you have read r6.ca/Goedel/goedel1.html, where Russell O'Connor formally verified that the Goedelization really works as it should. I direct your attention to section 6.2. where it is proved that the $\mathrm{Prf}$ relation has the desired properties (our $\mathrm{Prf}$ is called checkPrf in Russell's work). $\endgroup$
    – Andrej Bauer
    Commented Dec 23, 2010 at 14:32
9
$\begingroup$

(This is really just a comment, but apparently I don't have enough reputation to leave comments yet.)

I think there's some room for more care in the notation. $\Box \phi \implies \Box \Box \phi$ looks suspiciously like a formal sentence within a particular theory, and while undoubtedly true I feel it sweeps some things under the rug.

In the quote, the word "proved" formally has two meanings:

In fact, if a claim can be proved1, then it can be proved1 that the claim can be proved2.

The instances of "can be proved1" refer to proving a formal sentence in a fixed theory, whereas "can be proved2" is itself a formal sentence within that theory. In the notation Andrej uses in his post, "can be proved2" is the predicate $\mathrm{Prf}$. The quote can be formalised like this, for Peano arithmetic at least: "If $\mathrm{PA} \vdash \phi$ then $\mathrm{PA} \vdash \exists n . \mathrm{Prf}(m, n)$, where $m$ is the Gödel code of the sentence $\phi$ and $n$ is the code of any valid proof of $\phi$ (from the axioms of PA).

(For what it's worth, when I first started looking at logic I was confused about the difference between $\vdash$ and $\implies$. This is of a similar nature, I think.)

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ A key point is that "proofs" in the usual sense live in the metatheory. $\endgroup$
    – Carl Mummert
    Commented Dec 20, 2010 at 12:16
  • $\begingroup$ @Carl Mummert: Is there a difference between meta-theory and theory? Godel has coded all the metatheory concepts in the theory itself. $\endgroup$
    – Zirui Wang
    Commented Dec 23, 2010 at 11:18
  • $\begingroup$ @Zirui: How do you know that the coding works and lifts the relevant metatheory results into the theory itself? So, for instance, there's a concept of a proof inside PA — it's just a number satisfying certain constraints — and a concept of a proof in the metatheory — it's a sequence of sentences in the language of PA satisfying certain constraints. The challenge is to show that every number PA claims is a valid proof in fact encodes a valid proof in the "real world", and vice-versa — and this is precisely what Gödel did. [continued] $\endgroup$
    – Zhen Lin
    Commented Dec 23, 2010 at 13:45
  • $\begingroup$ [continuation] In computer science terms, what he showed was that set of numbers which encodes valid proofs in PA is recursive; equivalently, there is a Turing machine which will decide in finite time whether or not any number I give it encodes a valid proof. $\endgroup$
    – Zhen Lin
    Commented Dec 23, 2010 at 13:51
3
$\begingroup$

In order to talk about provability, we need to say what provability is. There are basically two options:

  1. Define an explicit provability predicate: encode some proof calculus in the natural numbers, then define "is a valid proof of $\phi$" as a predicate on natural number codes for proofs, then define "$\phi$ is provable" as "there exists a proof $\phi$". This was a major component of G\"odel's famous incompleteness proof.

  2. Select a set of axioms for the provability predicate, such that formulae involving "is provable" (but not "is a valid proof") follow from the axioms just in case they are true for a "sensible" proof system. If we take "sensible" to mean predicate calculus under the axioms of Peano Arithmetic, then the axioms of modal logic K4 plus the axiom $\Box(\Box A\Rightarrow A)\Rightarrow \Box A$ have this property; this seminal result is due to Solovay.

From perspective #2, the requirement "if $\phi$ is provable, it is provable that $\phi$ is provable" is taken to be part of the basic definition of provability. This is essentially an axiom excluding the possibility that we might be dealing with more than one notion of provability or entailment.

(or a counterexample if it's false)?

One often-overlooked case is when dealing with two different provability predicates. For example, take:

  • $\Box\phi$ to mean "$\neg\phi$ is inconsistent with ZFC" -- a fancy way of saying that if $M\vDash ZFC$, then $M\vDash \phi$

  • $\Box_\omega\phi$ to mean "$\neg\phi$ is $\omega$-inconsistent with ZFC" -- a fancy way of saying that if $M\vDash ZFC$ and $M$'s $\omega$ ordinal is well-founded, then $M\vDash \phi$.

In this scenario we do not have $\Box_\omega A \Rightarrow \Box_\omega \Box A$.

Such methods can be used to investigate how much first-order notions of provability ($\Box$) can tell us about infinitary ($\Box_\omega$) notions of provability and vice versa.

Improve this answer
$\endgroup$
2
  • $\begingroup$ For another example, see C. Smorynski, Self-Reference and Modal Logic, chapter 4, where he uses $\Box\varphi$ and $\bigtriangledown\varphi$, with the former meaning "provable in PA" and the latter meaning "provable in some theory T$\supseteq$PA". Of course this is only interesting when T is not finitely axiomatizable over PA. I speculate that this might be useful in the study of sentences provable in PA$_1$ (PA plus the set of all $\Pi_1$ consequences of PA). $\endgroup$
    – Adam
    Commented Jan 1, 2011 at 22:14
  • $\begingroup$ For yet another example, see Guaspari+Solovay (dx.doi.org/10.1016/0003-4843(79)90017-2) who use $\Box\phi$ for "$\phi$ is provable in PA" and $\Box^R\phi$ for "$\phi$ is Rosser-provable in PA". A formula $\phi$ is Rosser-provable if there is some proof of $\phi$ with natural number code $p$, and no natural number less than $p$ is the code for a proof of $\neg\phi$. $\endgroup$
    – Adam
    Commented Jan 11, 2011 at 0:19
2
$\begingroup$

Here's the way that I would think about the proof of the result which Wang asks about. First show that Robinson's Q proves every Sigma^0_1 sentence which is true on the standard model. (One way to establish this is to realize that the standard models embeds into every model of Robinson's Q). Second show that this first fact can be established in a subsystem of PA like ISigma^0_1, so that within ISigma^0_1 a schema is provable which asserts, for each Sigma^0_1 sentence, that if it is true then it is provable from Robinson's Q. (You need to go up to an intermediary system like ISigma^0_1 because you will need a little bit of induction to prove the first fact). Third note that formalized versions of provability statements have complexity Sigma^0_1.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .