Using the example of Gödel numbering, we can show that (the statement that is a proof of , which will be formally defined below) is .
First, should be true if and only if is the Gödel number of a term. Thanks to primitive recursion, we can define it by:
Then , which is true when is the Gödel number of an atomic formula, is defined by:
Next, , which is true only if is the Gödel number of a formula, is defined recursively by:
The definition of , which is true when 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 . This will be done by formalizing the concept of truth tables, which will require some development. First we show that , which is a sequence containing the (unique) atomic formulas of is . Define it by:
We say 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 or :
Then is a truth assignment for if is a truth assignment, is quantifier free, and every atomic formula in is the first member of one of the pairs in . That is:
Then we can define when makes true by:
Then is a tautology if every truth assignment makes it true:
We say that a number is a deduction of if it encodes a proof of from a set of axioms . This means that is a sequence where for each either:
is the Gödel number of an axiom
is a logical tautology
and the last element of is .
If is (almost every system of axioms, including , is ) then , which is true if is a deduction whose last value is , is also . This is fairly simple to see from the above results (let be the relation specifying that is the Gödel number of an axiom):
|Date of creation||2013-03-22 12:58:36|
|Last modified on||2013-03-22 12:58:36|
|Last modified by||mathcam (2727)|
|Synonym||deductions are delta 1|