Nisan comments on Formulas of arithmetic that behave like decision agents

[Nisan]

Proof of Proposition 4. This is kinda similar to the new proof of Proposition 3. It uses Lemma 6.

)%20\vdash%20A_0%20=%20C%20\to)

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

%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20C)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20D))%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C)))%0A\end{array}%20&%0A\end{align*})

%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\\%20\vee%20&%20\operatorname{Prv}(A_1%20=%20C)%0A\\%20\vee%20&%20\operatorname{Prv}(A_1%20=%20D)%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%0A\end{array}%20&%0A\\&\to%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%20&%20\mbox{by%20Lemma%201.1,3}%0A\\&\to%20\operatorname{Prv}((A_1%20=%20C%20\to%20A_0%20=%20D)%20\wedge%20(A_1%20=%20D%20\to%20A_0%20=%20C))%20&%0A\\&\to%20\operatorname{Prv}((A_1%20=%20C%20\to%20U_1%20=%202)%20\wedge%20(A_1%20=%20D%20\to%20U_1%20=%20-1))%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%20&%0A\end{align*})

Similarly,

)%20\vdash%20A_1%20=%20C%20\to%20A_0%20=%20C)

So

)%20\vdash%20A_0%20=%20A_1)

So

%0A\\%20\vee%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&%20\mbox{by%20definition%20of%20}%20A%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%20&%0A\\%20&%20\vdash%20\phi_0(0,1)%20&%0A\end{align*})

Suppose also that

) for some $aneq0$ and some $b$. Then

%20\wedge%20\phi_0(\dot{a},%20\dot{b})%0A\\&%20\vdash%20(A_0%20=%20C%20\to%20U_0%20=%200)%20\wedge%20(A_0%20=%20C%20\to%20U_0%20=%20\dot{a})%0A\\&%20\vdash%20A_0%20=%20C%20\to%200%20=%20U_0%20=%20\dot{a}%0A\\&%20\vdash%20A_0%20=%20C%20\to%20\bot%0A\\&%20\vdash%20A_0%20\neq%20C%0A\end{align*})

Assuming consistency of

), this is impossible by Lemma 1.3. So if

), then $a$ must be $0$. Similarly, one can prove that $b$ must be $1$. Thus, assuming consistency of

),

)%20\wedge%20a%20%3E%20b))

So, by the definition of $A$, we have $A\_0=D$. Similarly, $A\_1=D$.

$square$