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:14:08AM * 2 points [-]

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

$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 (\operatorname{Prv}(\phi_0(\dot{a},\dot{b})) \wedge ( \begin{array}[t]{r@{\,}l} & (a \neq 0 \wedge a \neq 2) \\ \vee & (b \neq -1 \wedge b \neq 1) \\ \vee & (a = 0 \wedge b = -1) \\ \vee & (a = 2 \wedge b = 1) \\ \vee & (a = 2 \wedge b = -1))) \end{array} & \\&\to \exists a,b ( \begin{array}[t]{r@{\,}l} & \operatorname{Prv}( \phi_0(\dot{a},\dot{b}) \wedge \dot{a} \neq 0 \wedge \dot{a} \neq 2) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{b} \neq 1 \wedge \dot{b} \neq 1) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{a} = 0 \wedge \dot{b} = -1) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{a} = 2 \wedge \dot{b} = 1) \\ \vee & \operatorname{Prv}(\phi_0(\dot{a},\dot{b}) \wedge \dot{a} = 2 \wedge \dot{b} = -1)) \end{array} & \mbox{by Lemma 6(b),(f)} \end{align*}$

$\begin{align*} &\to \exists a,b ( \begin{array}[t]{r@{\,}l} & \operatorname{Prv}( A_0 \neq C) \\ \vee & \operatorname{Prv}(A_0 \neq D) \\ \vee & \operatorname{Prv}((A_0 = C \to A_1 = C) \wedge (A_0 = D \to A_1 = C)) \\ \vee & \operatorname{Prv}((A_0 = C \to A_1 = D) \wedge (A_0 = D \to A_1 = D)) \\ \vee & \operatorname{Prv}((A_0 = C \to A_1 = D) \wedge (A_0 = D \to A_1 = C))) \end{array} & \end{align*}$

$\begin{align*} &\to \begin{array}[t]{r@{\,}l} & \operatorname{Prv}(A_0 \neq C) \\ \vee & \operatorname{Prv}(A_0 \neq D) \\ \vee & \operatorname{Prv}(A_1 = C) \\ \vee & \operatorname{Prv}(A_1 = D) \\ \vee & \operatorname{Prv}((A_0 = C \to A_1 = D) \wedge (A_0 = D \to A_1 = C)) \end{array} & \\&\to \operatorname{Prv}((A_0 = C \to A_1 = D) \wedge (A_0 = D \to A_1 = C)) & \mbox{by Lemma 1.1,3} \\&\to \operatorname{Prv}((A_1 = C \to A_0 = D) \wedge (A_1 = D \to A_0 = C)) & \\&\to \operatorname{Prv}((A_1 = C \to U_1 = 2) \wedge (A_1 = D \to U_1 = -1)) & \\&\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} & \mbox{by definition of } A \\ & \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(0,1) & \end{align*}$

Suppose also that $\vdash \phi(\dot{a}, \dot{b})$ for some $a \neq 0$ and some $b$ . Then

$\begin{align*} & \vdash \phi_0(0, 1) \wedge \phi_0(\dot{a}, \dot{b}) \\& \vdash (A_0 = C \to U_0 = 0) \wedge (A_0 = C \to U_0 = \dot{a}) \\& \vdash A_0 = C \to 0 = U_0 = \dot{a} \\& \vdash A_0 = C \to \bot \\& \vdash A_0 \neq C \end{align*}$

Assuming consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ , this is impossible by Lemma 1.3. So if $\vdash \phi_0(\dot{a}, \dot{b})$ , then $a$ must be $0$ . Similarly, one can prove that $b$ must be $1$ . Thus, assuming consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ ,