deductions are Δ1


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

First, 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:

Term(x) i<x[x=0,i]
x=5
y<x[x=6,yTerm(y)]
y,z<x[x=8,y,zTerm(y)Term(z)]
y,z<x[x=9,y,zTerm(y)Term(z)]

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

AtForm(x) y,z<x[x=1,y,zTerm(y)Term(z)]
y,z<x[x=7,y,zTerm(y)Term(z)]

Next, Form(x), which is true only if x is the Gödel number of a formulaMathworldPlanetmathPlanetmath, is defined recursively by:

Form(x) AtForm(x)
i,y<x[x=2,i,yForm(y)]
y<x[x=3,yForm(y)]
y,z<x[x=4,y,zForm(y)Form(z)]

The definition of 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 tautologiesMathworldPlanetmath is Δ1. This will be done by formalizing the concept of truth tablesMathworldPlanetmath, which will require some development. First we show that AtForms(a), which is a sequence containing the (unique) atomic formulas of a is Δ1. Define it by:

AtForms(a,t) (¬Form(a)t=0)
Form(a)(
x,y<a[a=1,x,yt=a]
x,y<a[a=7,x,yt=a]
i,x<a[a=2,i,xt=AtForms(x)]
x<a[a=3,xt=AtForms(x)]
x,y<a[a=4,x,yt=AtForms(x)*uAtForms(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)i<len(v)x,y<(v)i[(v)i=x,yAtForm(x)(y=1y=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)TA(v)QFForm(a)i<len(AtForms(a))j<len(v)[((v)j)0=(AtForms(a))i]

Then we can define when v makes a true by:

True(v,a) TAf(v,a)
AtForm(a)i<len(v)[((v)i)0=a((v)i)1=1]
y<x[x=3,yTrue(v,y)]
y,z<x[x=4,y,zTrue(v,y)True(v,z)]

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

Taut(a)v<22AtForms(a)[TAf(v,a)True(v,a)]

We say that a number a is a deductionMathworldPlanetmathPlanetmath of ϕ if it encodes a proof of ϕ 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<i such that (a)j=4,(a)k,(a)i (that is, (a)i is a conclusionMathworldPlanetmath under modus ponensMathworldPlanetmath from (a)j and (a)k).

and the last element of a is ϕ.

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

Proves(a,x)i<len(a)[Ax((a)i)j,k<i[(a)j=4,(a)k,(a)i]Taut((a)i)]
Title deductions are Δ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