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:25AM * 1 point [-]

Proof of Proposition 6. This proof uses Fact 5, the converse Barcan formula.

Strictly speaking, variables in Peano arithmetic are supposed to refer to natural numbers, and axioms like $\forall x . x + 1 > 0$ reflect this. But in this post, we have been treating variables like rational numbers! In fact, there are ways of talking about rational numbers using Peano arithmetic, and so far in this post we haven't bothered to write them out. But for this proof it will be important to distinguish between naturals and rationals. First we'll prove literal readings of (a) - (e) — that is, we'll assume variables refer to natural numbers. Then we'll indicate how to extend the proofs to rational versions of the Lemma.

(a)

$\begin{align*} & \vdash \forall x_1, \dots, x_k (P(x_1, \dots, x_k) \to Q(x_1, \dots, x_k)) & \\& \vdash \operatorname{Prv}(\forall x_1, \dots, x_k (P(x_1, \dots, x_k) \to Q(x_1, \dots, x_k))) & \\& \vdash \forall x_1, \dots, x_k \operatorname{Prv}(P(\dot{x}_1, \dots, \dot{x}_k) \to Q(\dot{x}_1, \dots, \dot{x}_k)) & \mbox{(converse Barcan formula)} \\& \vdash \forall x_1, \dots, x_k \operatorname{Prv}(P(\dot{x}_1, \dots, \dot{x}_k)) \to \operatorname{Prv}(Q(\dot{x}_1, \dots, \dot{x}_k)) & \end{align*}$

(b)

$\begin{align*} & \vdash \forall x. x = x & \\& \vdash \operatorname{Prv}(\forall x. x = x) & \\& \vdash \forall x \operatorname{Prv}(\dot{x} = \dot{x}) & \mbox{(converse Barcan formula)} \\& \vdash \forall x \operatorname{Prv}(\operatorname{Sub}(\ulcorner x = x \urcorner, x)) & \\& \vdash \forall x \operatorname{Prv}(\operatorname{Sub}(\ulcorner x = y \urcorner, x, x)) & \\& \vdash \forall x, y ( x = y \to \operatorname{Prv}(\operatorname{Sub}(\ulcorner x = y \urcorner, x, y))) & \\& \vdash \forall x, y (x = y \to \operatorname{Prv}(\dot{x} = \dot{y})) & \end{align*}$

$\begin{align*} & \vdash \forall z \operatorname{Prv}(\operatorname{Sub}(\ulcorner z = z \urcorner, z)) \\& \vdash \forall x,y \operatorname{Prv}(\operatorname{Sub}(\ulcorner z = z \urcorner, x + y)) \\& \vdash \forall x,y \operatorname{Prv}(\operatorname{Concat}(\operatorname{Sub}(\ulcorner z \urcorner, x + y), \ulcorner = \urcorner, \operatorname{Sub}(\ulcorner z \urcorner, x + y)) \end{align*}$

$\operatorname{Concat}$ is a recursive function such that $\operatorname{Concat}(\ulcorner \alpha \urcorner, \ulcorner \beta \urcorner, \ulcorner \gamma \urcorner) = \ulcorner \alpha \beta \gamma \urcorner$ . Now by messing around with Gödel numbers and numerals, one can prove

$\vdash \forall x,y \operatorname{Sub}(\ulcorner z \urcorner, x + y) = \operatorname{Sub}(\ulcorner x + y \urcorner, x, y)$

$\begin{align*} & \vdash \forall x,y \operatorname{Prv}(\operatorname{Concat}(\operatorname{Sub}(\ulcorner z \urcorner, x + y), \ulcorner = \urcorner, \operatorname{Sub}(\ulcorner x + y \urcorner, x, y))) \\& \vdash \forall x,y \operatorname{Prv}(\dot{x + y} = \dot{x} + \dot{y}) \end{align*}$

(d) We proceed by induction on $y$ . The base case:

$\begin{align*} & \vdash \forall x. 0 = x \times 0 & \\& \vdash \operatorname{Prv}( \forall x. 0 = x \times 0) & \\& \vdash \forall x \operatorname{Prv}( 0 = \dot{x} \times 0) & \mbox{(converse Barcan formula)} \\& \vdash \forall x \operatorname{Prv}( \dot{\overbrace{x \times 0}} = \dot{x} \times 0) & \end{align*}$

Now for the induction step, which implicitly uses part (a) in almost every step:

$\begin{align*} \vdash \forall x,y \operatorname{Prv}(\dot{\overbrace{xy}} = \dot{x} \times \dot{y}) \to \operatorname{Prv}(\dot{\overbrace{x(y+1)}} & = \dot{\overbrace{xy + x}} & \\& = \dot{\overbrace{xy}} + \dot{x} & \mbox{by (c)} \\& = \dot{x} \times \dot{y} + \dot{x} & \\& = \dot{x} \times (\dot{y} + 1) & \\& = \dot{x} \times \dot{\overbrace{y + 1}} ) & \mbox{ by (c)} \end{align*}$

(e)

$\begin{align*} \vdash \forall x,y ( x > y & \to \exists z. x = y + z + 1 & \\& \to \exists z \operatorname{Prv}( \dot{x} = \dot{\overbrace{y + z + 1}}) & \mbox{by (b)} \\& \to \exists z \operatorname{Prv}( \dot{x} = \dot{y} + \dot{z} + 1) & \mbox{by (c)} \\& \to \exists z \operatorname{Prv}( \dot{x} > \dot{y}) & \\& \to \operatorname{Prv}( \dot{x} > \dot{y}) \end{align*}$

Now we consider rational numbers. Every rational number $x$ can be written as

$x = \frac{x - x'}{x'' + 1}$

where $x, x$ are natural numbers. So one way to represent a rational-valued variable in Peano arithmetic is with a triple $(x, x', x'')$ of natural-valued variables. Two rational numbers are equal to each other when

$\frac{x - x'}{x'' + 1} = \frac{y - y'}{y'' + 1}$

Rearranging, we get $xy$

This condition is expressible in Peano arithmetic, and is how we can express equality of two rationals.

We can prove a rational version of (b) using the natural version of (b) and repeated application of the natural versions of (c) and (d):

$\begin{align*} \vdash \forall x,x',x'',y,y',y'' ( & x \times y'' + x + y' \times x'' + y' = y \times x'' + y +x' \times y'' + x' \\ & \to \operatorname{Prv}(\dot{\overbrace{x \times y'' + x + y' \times x'' + y'}} = \dot{\overbrace{y \times x'' + y +x' \times y'' + x'}}) & \\ & \to \operatorname{Prv}(\dot{x} \times \dot{y}'' + \dot{x} + \dot{y}' \times \dot{x}'' + \dot{y}' = \dot{y} \times \dot{x}'' + \dot{y} +\dot{x}' \times \dot{y}'' + \dot{x}') & \end{align*}$

With similar strategies one can prove rational versions of (a), (c), (d), and (e). Then we can prove the rational version of (f) directly:

(f)

$\begin{align*} \vdash \forall x,y( x \neq y &\to x > y \vee y > x & \\&\to \operatorname{Prv}(\dot{x} > \dot{y}) \vee \operatorname{Prv}(\dot{y} > \dot{x}) & \mbox{by (e)} \\&\to \operatorname{Prv}(\dot{x} \neq \dot{y}) \vee \operatorname{Prv}(\dot{y} \neq \dot{x}) & \\&\to \operatorname{Prv}(\dot{x} \neq \dot{y}) \end{align*}$

$\square$

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

Article Navigation

Comments (33)

Nearest Meetups

Virtual Study Room

Recent Comments

Recent Posts

Recent Rationality Quotes

Recent Wiki Edits

Top Contributors, 30 Days

Recent Karma Awards

Comments (33)

Top Contributors, 30 Days

You'll need to login or register to do that

(Don't worry, it only takes a few seconds)

Create

Login