deductions are ${\mathrm{\Delta }}_1$

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

First, $\mathrm{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:

$\mathrm{Term}(x)\leftrightarrow$

$x=⟨5⟩\vee$

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

$\mathrm{AtForm}(x)\leftrightarrow$

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

$\mathrm{Form}(x)\leftrightarrow$$\mathrm{AtForm}(x)\vee$

The definition of $\mathrm{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 ${\mathrm{\Delta }}_1$. This will be done by formalizing the concept of truth tables, which will require some development. First we show that $\mathrm{AtForms}(a)$, which is a sequence containing the (unique) atomic formulas of $a$ is ${\mathrm{\Delta }}_1$. Define it by:

$\mathrm{AtForms}(a,t)\leftrightarrow$$(\mathrm{\neg }\mathrm{Form}(a)\wedge t=0)\vee$

$\mathrm{Form}(a)\wedge ($

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$:

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:

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

$\mathrm{True}(v,a)\leftrightarrow$$TAf(v,a)\wedge$

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

We say that a number $a$ is a deduction of $\varphi$ if it encodes a proof of $\varphi$ 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 such that ${(a)}_j=⟨4,{(a)}_k,{(a)}_i⟩$ (that is, ${(a)}_i$ is a conclusion under modus ponens from ${(a)}_j$ and ${(a)}_k$).

and the last element of $a$ is $\mathrm{⌜}\varphi \mathrm{⌝}$.

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