Nisan comments on Formulas of arithmetic that behave like decision agents - Less Wrong

22 Post author: Nisan 03 February 2012 02:58AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (33)

Tags: decision_theory

Comments (33)

Sort By: Best

You are viewing a single comment's thread.

Comment author: Nisan 06 April 2012 03:13:50AM * 3 points [-]

Proof of Proposition 3 (without using Löb's theorem). This proof uses Lemma 6.

For brevity, let $A_i$ stand for $A(\ulcorner U \urcorner, i)$ , let $U_i$ stand for $\pi_i U()$ , and let $\phi_i(a,b)$ stand for $(A_i = C \to U_i = a) \wedge (A_i = D \to U_i = b)$ .

First, notice that

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

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

$\begin{align*} &\to \exists a,b (\operatorname{Prv}(\phi_0(\dot{a},\dot{b})) \wedge a > b) & \\&\to \exists a,b (\begin{array}[t]{r@{\,}l} &\operatorname{Prv}( \phi_0(\dot{a},\dot{b}) \wedge \dot{a}=1 \wedge \dot{b} = 0) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{a} \neq -1 \wedge \dot{a} \neq 1) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{b} \neq 0 \wedge \dot{b} \neq 2)) \end{array} & \\&\to \exists a,b ( \begin{array}[t]{r@{\,}l} & \operatorname{Prv}((A_0 = C \to U_0 = 1) \wedge (A_0 = D \to U_0 = 0)) \\ \vee & \operatorname{Prv}(A_0 = C \to U_0 \neq -1 \wedge U_0 \neq 1) \\ \vee & \operatorname{Prv}(A_0 = D \to U_0 \neq 0 \wedge U_0 \neq 2)) \end{array} & \mbox{by definition of } \phi_0 \end{align*}$

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

Similarly,

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

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

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

So there exist natural numbers $a$ and $b$ such that $\operatorname{Prv}(\phi_0(\dot{a},\dot{b})) \wedge a>b$ 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$ .