Title

Proof of Löb's theorem

<p>The intuition behind the proof of Lób’s theorem invokes the formalization of the following argument:</p>

<p>Let <script id="MathJax-Element-27" type="math/tex">S</script> stand for the sentence “If <script id="MathJax-Element-28" type="math/tex">S</script> is provable, then I am Santa Claus”.</p>

<p>As it is standard, when trying to prove a If…then theorem we can start by supposing the antecedent and checking that the consequent follows. But if <script id="MathJax-Element-29" type="math/tex">S</script> is provable, then we can chain its proof to an application of modus ponens of <script id="MathJax-Element-30" type="math/tex">S</script> to itself in order to get a proof of the consequent “I am Santa Claus”. If we suppose that finding a proof of a sentence implies that the sentence is true, then “I am Santa Claus” is true.</p>

<p>Thus we have supposed that <script id="MathJax-Element-31" type="math/tex">S</script> is provably true then it follows that “I am Santa Claus”, which is a proof of what <script id="MathJax-Element-32" type="math/tex">S</script> states! Therefore, <script id="MathJax-Element-33" type="math/tex">S</script> is provably true, and we can apply the same reasoning again (this time without supposing a counterfactual) to get that it is true that “I am Santa Claus”.</p>

<p>Holy Gödel! Have we broken logic? If this argument was to work, then we could proof all the nonsensical thing we wanted. So where does it fail?</p>

<p>One suspicion point is our implicit assumption that <script id="MathJax-Element-34" type="math/tex">S</script> can be constructed in the first place as a first order sentence. But we know that there exists a [ provability predicate] encoding the meaning we need, and then we can apply the [ diagonal lemma] to the formula <script id="MathJax-Element-35" type="math/tex">Prv(x)\implies</script> “I am Santa Claus” to get our desired <script id="MathJax-Element-36" type="math/tex">S</script>.</p>

<p>We will ignore that expressing “I am Santa Claus” in the language of first order logic is rather difficult, since we could have been dealing all the time with <script id="MathJax-Element-37" type="math/tex">0=1</script> instead of then sentence “I am Santa Claus”.</p>

<p>It turns out that the culprit of this paradox is the apparently innocent supposition that when “I am Santa Claus” is provable, then it is true.</p>

<p>How can this be false?, you may ask. Well, the standard provability predicate <script id="MathJax-Element-38" type="math/tex">Prv</script> is something of the form <script id="MathJax-Element-39" type="math/tex">\exists y Proof(x,y)</script>, where <script id="MathJax-Element-40" type="math/tex">Proof(x,y)</script> is true iff <script id="MathJax-Element-41" type="math/tex">y</script> encodes a valid proof of <script id="MathJax-Element-42" type="math/tex">x</script>. But <script id="MathJax-Element-43" type="math/tex">y</script> might be a [ nonstandard number] encoding a [ nonstandard proof] of infinitely many steps. If the only proofs of <script id="MathJax-Element-44" type="math/tex">x</script> are nonstandard then certainly you will never be able to prove <script id="MathJax-Element-45" type="math/tex">x</script> from the axioms of the system using standard methods.</p>

<p>We can restate this result we just reasoned as Löb’s theorem: If <script id="MathJax-Element-46" type="math/tex">Prv(A)\implies A</script> is provable, then <script id="MathJax-Element-47" type="math/tex">A</script> is provable.</p>

<hr>

<p>Now we go for the formal proof.</p>

<p>Let <script id="MathJax-Element-48" type="math/tex">T</script> be an [ axiomatizable] extension of [ minimal arithmetic], and <script id="MathJax-Element-49" type="math/tex">P</script> a one-place predicate satisfying the [ Bernais-Hilbert derivability conditions], which are:</p>

<ol>
<li>If <script id="MathJax-Element-50" type="math/tex">T\vdash A</script>, then <script id="MathJax-Element-51" type="math/tex">T\vdash P(A)</script>.</li>
<li><script id="MathJax-Element-52" type="math/tex">T\vdash P(A\implies B) \implies (P(A)\implies P(B))</script></li>
<li><script id="MathJax-Element-53" type="math/tex">T\vdash P(A)\implies P(P(A))</script>.</li>
</ol>

<p>For example, <script id="MathJax-Element-54" type="math/tex">PA</script> and the standard provability predicate [ satisfy those conditions].</p>

<p>Let us suppose that <script id="MathJax-Element-55" type="math/tex">A</script> is such that <script id="MathJax-Element-56" type="math/tex">T\vdash P(A)\implies A</script>.</p>

<p>As <script id="MathJax-Element-57" type="math/tex">T</script> extends minimal arithmetic, the diagonal lemma is applicable, and thus there exists <script id="MathJax-Element-58" type="math/tex">S</script> such that <script id="MathJax-Element-59" type="math/tex">T\vdash P(S)\implies A</script>.</p>

<p>By condition 1, <script id="MathJax-Element-60" type="math/tex">T\vdash P(P(S)\implies A)</script>.</p>

<p>By condition 2, <script id="MathJax-Element-61" type="math/tex">T\vdash P(P(S))\implies P(A)</script>.</p>

<p>By condition 3, <script id="MathJax-Element-62" type="math/tex">T\vdash P(S)\implies P(P(S))</script> and thus <script id="MathJax-Element-63" type="math/tex">T\vdash P(S)\implies P(A)</script>.</p>

<p>By our initial assumption, this means that <script id="MathJax-Element-64" type="math/tex">T\vdash P(S)\implies P(A)</script>.</p>

<p>But by the construction of <script id="MathJax-Element-65" type="math/tex">S</script>, then <script id="MathJax-Element-66" type="math/tex">T\vdash S</script>!</p>

<p>By condition 1 again, then <script id="MathJax-Element-67" type="math/tex">T\vdash P(S)</script>, and since we alreadt had shown that <script id="MathJax-Element-68" type="math/tex">T\vdash P(S)\implies A</script>, we have that <script id="MathJax-Element-69" type="math/tex">T\vdash A</script>, which completes the proof.</p>

<p>We remark that <script id="MathJax-Element-70" type="math/tex">P</script> can be any predicate satisfying the conditions, such as the verum predicate <script id="MathJax-Element-71" type="math/tex">x=x</script>.</p>

<blockquote>
  <p>Written with <a href="https://stackedit.io/">StackEdit</a>.</p>
</blockquote>