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<x[x=\langle 0,i\rangle]\vee$
		$\displaystyle x=\langle 5\rangle\vee$
		$\displaystyle\exists y<x[x=\langle 6,y\rangle\wedge\operatorname{Term}(y)]\vee$
		$\displaystyle\exists y,z<x[x=\langle 8,y,z\rangle\wedge\operatorname{Term}(y)% \wedge\operatorname{Term}(z)]\vee$
		$\displaystyle\exists y,z<x[x=\langle 9,y,z\rangle\wedge\operatorname{Term}(y)% \wedge\operatorname{Term}(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<x[x=\langle 1,y,z\rangle\wedge\operatorname{Term}(y)% \wedge\operatorname{Term}(z)]\vee$
		$\displaystyle\exists y,z<x[x=\langle 7,y,z\rangle\wedge\operatorname{Term}(y)% \wedge\operatorname{Term}(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<x[x=\langle 2,i,y\rangle\wedge\operatorname{Form}(y)]\vee$
		$\displaystyle\exists y<x[x=\langle 3,y\rangle\wedge\operatorname{Form}(y)]\vee$
		$\displaystyle\exists y,z<x[x=\langle 4,y,z\rangle\wedge\operatorname{Form}(y)% \wedge\operatorname{Form}(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<a[a=\langle 1,x,y\rangle t=a]\vee$
		$\displaystyle\exists x,y<a[a=\langle 7,x,y\rangle\wedge t=a]\vee$
		$\displaystyle\exists i,x<a[a=\langle 2,i,x\rangle\wedge t=\operatorname{% AtForms}(x)]\vee$
		$\displaystyle\exists x<a[a=\langle 3,x\rangle\wedge t=\operatorname{AtForms}(x% )]\vee$
		$\displaystyle\exists x,y<a[a=\langle 4,x,y\rangle\wedge t=\operatorname{% AtForms}(x)*_{u}\operatorname{AtForms}(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<x[x=\langle 3,y\rangle\wedge\operatorname{True}(v,y)]\vee$
		$\displaystyle\exists y,z<x[x=\langle 4,y,z\rangle\wedge\operatorname{True}(v,y% )\rightarrow\operatorname{True}(v,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 $A x$ . 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<i$ 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 $A x$ is $\Delta_{1}$ (almost every system of axioms, including $P A$ , 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<i[(a)_{j}=\langle 4,(a)_{k},(a)_{i}% \rangle]\vee\operatorname{Taut}((a)_{i})\right]

Title	deductions are $\Delta_{1}$
Canonical name	DeductionsAreDelta1
Date of creation	2013-03-22 12:58:36
Last modified on	2013-03-22 12:58:36
Owner	mathcam (2727)
Last modified by	mathcam (2727)
Numerical id	9
Author	mathcam (2727)
Entry type	Theorem
Classification	msc 03B10
Synonym	deductions are delta 1
Defines	truth assignment

deductions are Δ1

deductions are $\Delta_{1}$