# deductions are $\Delta_{1}$

Using the example of Gödel numbering, we can show that $\operatorname{Proves}(a,x)$ (the statement that $a$ is a proof of $x$, which will be formally defined below) is $\Delta_{1}$.

First, $\operatorname{Term}(x)$ should be true if and only if $x$ is the Gödel number of a term. Thanks to primitive recursion, we can define it by:

 $\displaystyle\operatorname{Term}(x)\leftrightarrow$ $\displaystyle\exists i $\displaystyle x=\langle 5\rangle\vee$ $\displaystyle\exists y $\displaystyle\exists y,z $\displaystyle\exists y,z

Then $\operatorname{AtForm}(x)$, which is true when $x$ is the Gödel number of an atomic formula, is defined by:

 $\displaystyle\operatorname{AtForm}(x)\leftrightarrow$ $\displaystyle\exists y,z $\displaystyle\exists y,z

Next, $\operatorname{Form}(x)$, which is true only if $x$ is the Gödel number of a formula, is defined recursively by:

 $\displaystyle\operatorname{Form}(x)\leftrightarrow$ $\displaystyle\operatorname{AtForm}(x)\vee$ $\displaystyle\exists i,y $\displaystyle\exists y $\displaystyle\exists y,z

The definition of $\operatorname{QFForm}(x)$, which is true when $x$ is the Gödel number of a quantifier free formula, is defined the same way except without the second clause.

Next we want to show that the set of logical tautologies is $\Delta_{1}$. This will be done by formalizing the concept of truth tables, which will require some development. First we show that $\operatorname{AtForms}(a)$, which is a sequence containing the (unique) atomic formulas of $a$ is $\Delta_{1}$. Define it by:

 $\displaystyle\operatorname{AtForms}(a,t)\leftrightarrow$ $\displaystyle(\neg\operatorname{Form}(a)\wedge t=0)\vee$ $\displaystyle\operatorname{Form}(a)\wedge($ $\displaystyle\exists x,y $\displaystyle\exists x,y $\displaystyle\exists i,x $\displaystyle\exists x $\displaystyle\exists x,y

We say $v$ is a truth assignment if it is a sequence of pairs with the first member of each pair being a atomic formula and the second being either $1$ or $0$:

 $TA(v)\leftrightarrow\forall i<\operatorname{len}(v)\exists x,y<(v)_{i}[(v)_{i}% =\langle x,y\rangle\wedge\operatorname{AtForm}(x)\wedge(y=1\vee y=0)]$

Then $v$ is a truth assignment for $a$ if $v$ is a truth assignment, $a$ is quantifier free, and every atomic formula in $a$ is the first member of one of the pairs in $v$. That is:

 $TAf(v,a)\leftrightarrow TA(v)\wedge\operatorname{QFForm}(a)\wedge\forall i<% \operatorname{len}(\operatorname{AtForms}(a))\exists j<\operatorname{len}(v)[(% (v)_{j})_{0}=(\operatorname{AtForms}(a))_{i}]$

Then we can define when $v$ makes $a$ true by:

 $\displaystyle\operatorname{True}(v,a)\leftrightarrow$ $\displaystyle TAf(v,a)\wedge$ $\displaystyle\operatorname{AtForm}(a)\wedge\exists i<\operatorname{len}(v)[((v% )_{i})_{0}=a\wedge((v)_{i})_{1}=1]\vee$ $\displaystyle\exists y $\displaystyle\exists y,z

Then $a$ is a tautology if every truth assignment makes it true:

 $\operatorname{Taut}(a)\forall v<2^{2^{\operatorname{AtForms}(a)}}[TAf(v,a)% \rightarrow\operatorname{True}(v,a)]$

We say that a number $a$ is a deduction of $\phi$ if it encodes a proof of $\phi$ from a set of axioms $Ax$. This means that $a$ is a sequence where for each $(a)_{i}$ either:

• $(a)_{i}$ is the Gödel number of an axiom

• $(a)_{i}$ is a logical tautology

or

• there are some $j,k such that $(a)_{j}=\langle 4,(a)_{k},(a)_{i}\rangle$ (that is, $(a)_{i}$ is a conclusion under modus ponens from $(a)_{j}$ and $(a)_{k}$).

and the last element of $a$ is $\ulcorner\phi\urcorner$.

If $Ax$ is $\Delta_{1}$ (almost every system of axioms, including $PA$, is $\Delta_{1}$) then $\operatorname{Proves}(a,x)$, which is true if $a$ is a deduction whose last value is $x$, is also $\Delta_{1}$. This is fairly simple to see from the above results (let $\operatorname{Ax}(x)$ be the relation specifying that $x$ is the Gödel number of an axiom):

 $\operatorname{Proves}(a,x)\leftrightarrow\forall i<\operatorname{len}(a)\left[% \operatorname{Ax}((a)_{i})\vee\exists j,k
Title deductions are $\Delta_{1}$ DeductionsAreDelta1 2013-03-22 12:58:36 2013-03-22 12:58:36 mathcam (2727) mathcam (2727) 9 mathcam (2727) Theorem msc 03B10 deductions are delta 1 truth assignment