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=\u27e85\u27e9\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}=\u27e84,{(a)}_{k},{(a)}_{i}\u27e9$ (that is, ${(a)}_{i}$ is a conclusion^{} under modus ponens^{} from ${(a)}_{j}$ and ${(a)}_{k}$).
and the last element of $a$ is $\mathrm{\u231c}\varphi \mathrm{\u231d}$.
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):
$$ 
Title  deductions are ${\mathrm{\Delta}}_{1}$ 

Canonical name  DeductionsAreDelta1 
Date of creation  20130322 12:58:36 
Last modified on  20130322 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 