Nisan comments on Formulas of arithmetic that behave like decision agents

Nisan 6 Apr 2012 3:13 UTC
5 points
0
Proof of Proposition 3 (without using Löb’s theorem). This proof uses Lemma 6.

For brevity, let $A_i$ stand for
), let $U_i$ stand for
), and let
) stand for
%20\wedge%20(A_i%20=%20D%20\to%20U_i%20=%20b)).

First, notice that

$\\begin\{align\*\} \\vdash \\forall a,b \( a>b &\\to \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \(a = 1 \\wedge b = 0\$
%0A\\%20\vee%20&%20(a%20\neq%20-1%20\wedge%20a%20\neq%201)%0A\\%20\vee%20&%20(b%20\neq%200%20\wedge%20b%20\neq%202)%0A\end{array}%0A\\&\to%20\begin{array}[t]{r@{\,}ll}%0A&%20\operatorname{Prv}(%20\dot{a}%20=%201%20\wedge%20\dot{b}%20=%200)%20&%20\mbox{by%20Lemma%206(b),(f)}%0A\\%20\vee%20&%20\operatorname{Prv}(\dot{a}%20\neq%20-1%20\wedge%20\dot{a}%20\neq%201)%20&%0A\\%20\vee%20&%20\operatorname{Prv}(%20\dot{b}%20\neq%200%20\wedge%20\dot{b}%20\neq%202))%20&%0A\end{array}%0A\end{align*})

So

$\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$
)%20\vdash%20A_0%20=%20C%20\to)

$\\begin\{align\*\} &\\to \\exists a,b \(\\operatorname\{Prv\}\(\\phi\_0\(\\dot\{a\},\\dot\{b\}\$
)%20\wedge%20a%20%3E%20b)%20&%0A\\&\to%20\exists%20a,b%20(\begin{array}[t]{r@{\,}l}%0A&\operatorname{Prv}(%20\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}=1%20\wedge%20\dot{b}%20=%200)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20\neq%20-1%20\wedge%20\dot{a}%20\neq%201)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{b}%20\neq%200%20\wedge%20\dot{b}%20\neq%202))%0A\end{array}%20&%0A\\&\to%20\exists%20a,b%20(%20\begin{array}[t]{r@{\,}l}%0A&%20\operatorname{Prv}((A_0%20=%20C%20\to%20U_0%20=%201)%20\wedge%20(A_0%20=%20D%20\to%20U_0%20=%200))%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20C%20\to%20U_0%20\neq%20-1%20\wedge%20U_0%20\neq%201)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20D%20\to%20U_0%20\neq%200%20\wedge%20U_0%20\neq%202))%0A\end{array}%20&%20\mbox{by%20definition%20of%20}%20\phi_0%0A\end{align*})

$\\begin\{align\*\} \\qquad\\qquad &\\to \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\operatorname\{Prv\}\(\(A\_0 = C \\to A\_1 = C\$
%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20D))%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20C\to%20\bot)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20D\to%20\bot)%0A\end{array}%20&%0A\\&\to%20\begin{array}[t]{r@{\,}l}%0A&%20\operatorname{Prv}(A_0%20=%20A_1)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20C)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\end{array}%20&%0A\\&\to%20\operatorname{Prv}(A_0%20=%20A_1)%20&%20\mbox{by%20Lemma%201.1,3}%0A\\&\to%20\operatorname{Prv}(\phi_0(1,0))%20&%0A\\&\to%20\exists%20a,b%20\operatorname{Prv}(\phi_1(\dot{a},\dot{b}))%20\wedge%20a%3Eb%20&%0A\\&\to%20A_1%20=%20C%0A\end{align*})

Similarly,

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$
)%20\vdash%20A_1%20=%20C%20\to%20A_0%20=%20C)

So

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$
)%20\vdash%20A_0%20=%20A_1)

So

$\\begin\{align\*\} PA & \\vdash \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\neg \\operatorname\{Con\}\(\\operatorname\{PA\}\$
%0A\\%20\vee%20&%20(%20\operatorname{Con}(\operatorname{PA})%20\wedge%20\neg%20\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA})))%20%0A\\%20\vee%20&%20(\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA}))%20\wedge%20A_0%20=%20A_1)%0A\end{array}%20&%0A\\%20&%20\vdash%20\begin{array}[t]{r@{\,}l}%0A&%20A_0%20=%20D%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20C%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20A_1%0A\end{array}%20&%20\mbox{by%20Lemma%201.2,4}%0A\\%20&%20\vdash%20A_0%20=%20A_1%0A\\%20&%20\vdash%20\phi_0(1,0)%0A\end{align*})

So there exist natural numbers $a$ and $b$ such that
)%20\wedge%20a%3Eb) is true. Therefore, assuming consistency of
$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$
), by the definition of $A$ , we have $A_0 = C$ . Similarly, $A_1 = C$ .

$s q u a r e$
What links here?