Incompleteness

Arithmetization of Syntax

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Editorial

Note that arithmetization for signed tableaux is not yet available.

Introduction

In order to connect computability and logic, we need a way to talk about the objects of logic (symbols, terms, formulas, derivations), operations on them, and their properties and relations, in a way amenable to computational treatment. We can do this directly, by considering computable functions and relations on symbols, sequences of symbols, and other objects built from them. Since the objects of logical syntax are all finite and built from an enumerable sets of symbols, this is possible for some models of computation. But other models of computation---such as the recursive functions----are restricted to numbers, their relations and functions. Moreover, ultimately we also want to be able to deal with syntax within certain theories, specifically, in theories formulated in the language of arithmetic. In these cases it is necessary to arithmetize syntax, i.e., to represent syntactic objects, operations on them, and their relations, as numbers, arithmetical functions, and arithmetical relations, respectively. The idea, which goes back to Leibniz, is to assign numbers to syntactic objects.

It is relatively straightforward to assign numbers to symbols as their “codes.” Some symbols pose a bit of a challenge, since, e.g., there are infinitely many variables, and even infinitely many function symbols of each arity nnsource. But of course it's possible to assign numbers to symbols systematically in such a way that, say, v2\Obj v_2source and v3\Obj v_3source are assigned different codes. Sequences of symbols (such as terms and formulas) are a bigger challenge. But if we can deal with sequences of numbers purely arithmetically (e.g., by the powers-of-primes coding of sequences), we can extend the coding of individual symbols to coding of sequences of symbols, and then further to sequences or other arrangements of formulas, such as derivations. This extended coding is called “Gödel numbering.” Every term, formula, and derivation is assigned a Gödel number.

By coding sequences of symbols as sequences of their codes, and by choosing a system of coding sequences that can be dealt with using computable functions, we can then also deal with Gödel numbers using computable functions. In practice, all the relevant functions will be primitive recursive. For instance, computing the length of a sequence and computing the iisource-th element of a sequence from the code of the sequence are both primitive recursive. If the number coding the sequence is, e.g., the Gödel number of a formula A!Asource, we immediately see that the length of a formula and the (code of the) iisource-th symbol in a formula can also be computed from the Gödel number of A!Asource. It is a bit harder to prove that, e.g., the property of being the Gödel number of a correctly formed term or of a correct derivation is primitive recursive. It is nevertheless possible, because the sequences of interest (terms, formulas, derivations) are inductively defined.

As an example, consider the operation of substitution. If A!Asource is a formula, xxsource a variable, and ttsource a term, then A[t/x]\Subst{!A}{t}{x}source is the result of replacing every free occurrence of xxsource in A!Asource by ttsource. Now suppose we have assigned Gödel numbers to A!Asource, xxsource, ttsource---say, kksource, llsource, and mmsource, respectively. The same scheme assigns a Gödel number to A[t/x]\Subst{!A}{t}{x}source, say, nnsource. This mapping---of kksource, llsource, and mmsource to nnsource---is the arithmetical analog of the substitution operation. When the substitution operation maps A!Asource, xxsource, ttsource to A[t/x]\Subst{!A}{t}{x}source, the arithmetized substitution function maps the Gödel numbers kksource, llsource, mmsource to the Gödel number nnsource. We will see that this function is primitive recursive.

Arithmetization of syntax is not just of abstract interest, although it was originally a non-trivial insight that languages like the language of arithmetic, which do not come with mechanisms for “talking about” languages can, after all, formalize complex properties of expressions. It is then just a small step to ask what a theory in this language, such as Peano arithmetic, can prove about its own language (including, e.g., whether sentences are provable or true). This leads us to the famous limitative theorems of Gödel (about unprovability) and Tarski (the undefinability of truth). But the trick of arithmetizing syntax is also important in order to prove some important results in computability theory, e.g., about the computational power of theories or the relationship between different models of computability. The arithmetization of syntax serves as a model for arithmetizing other objects and properties. For instance, it is similarly possible to arithmetize configurations and computations (say, of Turing machines). This makes it possible to simulate computations in one model (e.g., Turing machines) in another (e.g., recursive functions).

Coding Symbols

The basic language L\Lang Lsource of first order logic makes use of the symbols

⊥¬∨∧→∀∃=(),\lfalse \quad \lnot \quad \lor \quad \land \quad \lif \quad \lforall \quad \lexists \quad \eq \quad ( \quad ) \quad ,source

together with enumerable sets of variables and constant symbols, and enumerable sets of function symbols and predicate symbols of arbitrary arity. We can assign codes to each of these symbols in such a way that every symbol is assigned a unique number as its code, and no two different symbols are assigned the same number. We know that this is possible since the set of all symbols is enumerable and so there is a bijection between it and the set of natural numbers. But we want to make sure that we can recover the symbol (as well as some information about it, e.g., the arity of a function symbol) from its code in a computable way. There are many possible ways of doing this, of course. Here is one such way, which uses primitive recursive functions. (Recall that ⟨n0,…,nk⟩\tuple{n_0, \dots, n_k}source is the number coding the sequence of numbers n0n_0source, dots, nkn_ksource.)

Definition of symbol codes

If sssource is a symbol of L\Lang Lsource, let the symbol code cs\scode ssource be defined as follows:

  1. If sssource is among the logical symbols, cs\scode ssource is given by the following table:

    ⊥¬∨∧→∀⟨0,0⟩⟨0,1⟩⟨0,2⟩⟨0,3⟩⟨0,4⟩⟨0,5⟩∃=(),⟨0,6⟩⟨0,7⟩⟨0,8⟩⟨0,9⟩⟨0,10⟩\begin{array}{cccccccccc} \lfalse & \lnot & \lor & \land & \lif & \lforall \\ \tuple{0, 0} & \tuple{0, 1} & \tuple{0, 2} & \tuple{0, 3} & \tuple{0, 4} & \tuple{0, 5} \\ \lexists & \eq & ( & ) & ,\\ \tuple{0, 6} & \tuple{0, 7} & \tuple{0, 8} & \tuple{0, 9} & \tuple{0, 10} \end{array}source

  2. If sssource is the iisource-th variable vi\Obj v_isource, then cs=⟨1,i⟩\scode s = \tuple{1, i}source.

  3. If sssource is the iisource-th constant symbol ci\Obj c_isource, then cs=⟨2,i⟩\scode s = \tuple{2, i}source.

  4. If sssource is the iisource-th nnsource-ary function symbol fin\Obj f_i^nsource, then cs=⟨3,n,i⟩\scode s = \tuple{3, n, i}source.

  5. If sssource is the iisource-th nnsource-ary predicate symbol Pin\Obj P_i^nsource, then cs=⟨4,n,i⟩\scode s = \tuple{4, n, i}source.

Primitive recursive recognition of function and predicate symbol codes

The following relations are primitive recursive:

  1. Fn(x,n)\fn{Fn}(x, n)source iff xxsource is the code of fin\Obj f^n_isource for some iisource, i.e., xxsource is the code of an nnsource-ary function symbol.

  2. Pred(x,n)\fn{Pred}(x, n)source iff xxsource is the code of Pin\Obj P^n_isource for some iisource or xxsource is the code of =\eqsource and n=2n = 2source, i.e., xxsource is the code of an nnsource-ary predicate symbol.

Definition of a string Goedel number

If s0,…,sn−1s_0, \dots, s_{n-1}source is a sequence of symbols, its Gödel number is ⟨cs0,…,csn−1⟩\tuple{\scode{s_0}, \dots, \scode{s_{n-1}}}source.

Explain

Note that codes and Gödel numbers are different things. For instance, the variable v5\Obj v_5source has a code cv5=⟨1,5⟩=22·36\scode{\Obj v_5} = \tuple{1, 5} = 2^2\cdot 3^6source. But the variable v5\Obj v_5source considered as a term is also a sequence of symbols (of length 11source). The Gödel number #v5#\Gn{\Obj v_5}source of the term v5\Obj v_5source is ⟨cv5⟩=2cv5+1=222·36+1\tuple{\scode{\Obj v_5}} = 2^{\scode{\Obj v_5} + 1} = 2^{2^2\cdot 3^6 + 1}source.

Worked Goedel number of a prefix equality formula

Recall that if k0k_0source, dots, kn−1k_{n-1}source is a sequence of numbers, then the code of the sequence ⟨k0,…,kn−1⟩\tuple{k_0, \dots, k_{n-1}}source in the power-of-primes coding is

2k0+1·3k1+1·…·pn−1kn−1+1,2^{k_0+1}\cdot3^{k_1+1}\cdot \dots \cdot p_{n-1}^{k_{n-1}+1},source

where pip_isource is the iisource-th prime (starting with p0=2p_0 = 2source). So for instance, the formula v0=0\eq[\Obj v_0][\Obj 0]source, or, more explicitly, =(v0,c0){\eq}(\Obj v_0,\Obj c_0)source, has the Gödel number

⟨c=,c(,cv0,c,,cc0,c)⟩.\tuple{\scode{\eq},\scode{(},\scode{\Obj v_0},\scode{,}, \scode{\Obj c_0},\scode{)}}.source

Here, c=\scode{\eq}source is ⟨0,7⟩=20+1·37+1\tuple{0,7} = 2^{0+1}\cdot 3^{7+1}source, cv0\scode{\Obj v_0}source is ⟨1,0⟩=21+1·30+1\tuple{1,0} = 2^{1+1}\cdot3^{0+1}source, etc. So #=(v0,c0)#\Gn{=(\Obj v_0,\Obj c_0)}source is

2c=+1·3c(+1·5cv0+1·7c,+1·11cc0+1·13c)+1=221·38+1·321·39+1·522·31+1·721·311+1·1123·31+1·1321·310+1=213123·339367·513·7354295·1125·13118099.2^{\scode{=} + 1}\cdot 3^{\scode{(}+1}\cdot 5^{\scode{\Obj v_0}+1} \cdot 7^{\scode{,} + 1} \cdot 11^{\scode{\Obj c_0}+1} \cdot 13^{\scode{)}+1} = \\ 2^{2^1\cdot 3^8 + 1}\cdot 3^{2^1\cdot 3^9+1}\cdot 5^{2^2\cdot 3^1+1} \cdot 7^{2^1\cdot 3^{11} + 1} \cdot 11^{2^3\cdot3^1+1} \cdot 13^{2^1\cdot3^{10}+1} = \\ 2^{13\,123}\cdot 3^{39\,367}\cdot 5^{13}\cdot 7^{354\,295}\cdot11^{25}\cdot13^{118\,099}.source

Coding Terms

Explain

A term is simply a certain kind of sequence of symbols: it is built up inductively from constants and variables according to the formation rules for terms. Since sequences of symbols can be coded as numbers---using a coding scheme for the symbols plus a way to code sequences of numbers---assigning Gödel numbers to terms is not difficult. The challenge is rather to show that the property a number has if it is the Gödel number of a correctly formed term is computable, or in fact primitive recursive.

Variables and constant symbols are the simplest terms, and testing whether xxsource is the Gödel number of such a term is easy: Var(x)\fn{Var}(x)source holds if xxsource is #vi#\Gn{\Obj v_i}source for some iisource. In other words, xxsource is a sequence of length 11source and its single element (x)0(x)_0source is the code of some variable vi\Obj v_isource, i.e., xxsource is ⟨⟨1,i⟩⟩\tuple{\tuple{1, i}}source for some iisource. Similarly, Const(x)\fn{Const}(x)source holds if xxsource is #ci#\Gn{\Obj c_i}source for some iisource. Both of these relations are primitive recursive, since if such an iisource exists, it must be <x< xsource:

Var(x)⇔(∃i<x)x=⟨⟨1,i⟩⟩Const(x)⇔(∃i<x)x=⟨⟨2,i⟩⟩\fn{Var}(x) & \defiff \bexists{i<x}{x = \tuple{\tuple{1, i}}}\\ \fn{Const}(x) & \defiff \bexists{i<x}{x = \tuple{\tuple{2, i}}}source

Primitive recursive recognition of terms and closed terms

The relations Term(x)\fn{Term}(x)source and ClTerm(x)\fn{ClTerm}(x)source which hold iff xxsource is the Gödel number of a term or a closed term, respectively, are primitive recursive.

Proof

A sequence of symbols sssource is a term iff there is a sequence s0s_0source, dots, sk−1=ss_{k-1} = ssource of terms which records how the term sssource was formed from constant symbols and variables according to the formation rules for terms. To express that such a putative formation sequence follows the formation rules it has to be the case that, for each i<ki < ksource, either

  1. sis_isource is a variable vj\Obj v_jsource, or

  2. sis_isource is a constant symbol cj\Obj c_jsource, or

  3. sis_isource is built from nnsource terms t1t_1source, dots, tnt_nsource occurring prior to place iisource using an nnsource-place function symbol fjn\Obj f^n_jsource.

To show that the corresponding relation on Gödel numbers is primitive recursive, we have to express this condition primitive recursively, i.e., using primitive recursive functions, relations, and bounded quantification.

Suppose yysource is the number that codes the sequence s0s_0source, dots, sk−1s_{k-1}source, i.e., y=⟨#s0#,…,#sk−1#⟩y = \tuple{\Gn{s_0}, \dots, \Gn{s_{k-1}}}source. It codes a formation sequence for the term with Gödel number xxsource iff for all i<ki < ksource:

  1. Var((y)i)\fn{Var}((y)_i)source, or

  2. Const((y)i)\fn{Const}((y)_i)source, or

  3. there is an nnsource and a number z=⟨z1,…,zn⟩z = \tuple{z_1, \dots, z_n}source such that each zlz_lsource is equal to some (y)i′(y)_{i'}source for i′<ii' < isource and

    (y)i=#fjn(#⌢flatten(z)⌢#)#,(y)_i = \Gn{\Obj f^n_j(} \concat \fn{flatten}(z) \concat \Gn{)},source

and moreover (y)k−1=x(y)_{k-1} = xsource. (The function flatten(z)\fn{flatten}(z)source turns the sequence ⟨#t1#,…,#tn#⟩\tuple{\Gn{t_1}, \dots, \Gn{t_n}}source into #t1,…,tn#\Gn{t_1, \dots, t_n}source and is primitive recursive.)

The indices jjsource, nnsource, the Gödel numbers zlz_lsource of the terms tlt_lsource, and the code zzsource of the sequence ⟨z1,…,zn⟩\tuple{z_1, \dots, z_n}source, in (3) are all less than yysource. We can replace kksource above with len(y)\len{y}source. Hence we can express “yysource is the code of a formation sequence of the term with Gödel number xxsource” in a way that shows that this relation is primitive recursive.

We now just have to convince ourselves that there is a primitive recursive bound on yysource. But if xxsource is the Gödel number of a term, it must have a formation sequence with at most len(x)\len{x}source terms (since every term in the formation sequence of sssource must start at some place in sssource, and no two subterms can start at the same place). The Gödel number of each subterm of sssource is of course ≤x\le xsource. Hence, there always is a formation sequence with code ≤pk−1k(x+1)\le p_{k-1}^{k(x+1)}source, where k=len(x)k=\len{x}source.

For ClTerm\fn{ClTerm}source, simply leave out the clause for variables.

Exercise on flattening coded lists of terms

Show that the function flatten(z)\fn{flatten}(z)source, which turns the sequence ⟨#t1#,…,#tn#⟩\tuple{\Gn{t_1}, \dots, \Gn{t_n}}source into #t1,…,tn#\Gn{t_1, \dots, t_n}source, is primitive recursive.

Primitive recursive coding of numerals

The function num(n)=#n¯#\fn{num}(n) = \Gn{\num{n}}source is primitive recursive.

Proof

We define num(n)\fn{num}(n)source by primitive recursion:

num(0)=#0#num(n+1)=#′(#⌢num(n)⌢#)#.\fn{num}(0) & = \Gn{\Obj 0}\\ \fn{num}(n+1) & = \Gn{\prime(} \concat \fn{num}(n) \concat \Gn{)}.source

Coding formula

Once we have defined the relation Term(x)\fn{Term}(x)source primitive recursively, we can use it to define the corresponding relation for formulas, Frm(x)\fn{Frm}(x)source primitive recursively.

Primitive recursive recognition of atomic formula codes

The relation Atom(x)\fn{Atom}(x)source which holds iff xxsource is the Gödel number of an atomic formula, is primitive recursive.

Proof

The number xxsource is the Gödel number of an atomic formula iff one of the following holds:

  1. There are nnsource, j<xj < xsource, and z<xz < xsource such that for each i<ni < nsource, Term((z)i)\fn{Term}((z)_i)source and x=x =source

    #Pjn(#⌢flatten(z)⌢#)#.\Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)}.source

  2. There are z1,z2<xz_1, z_2 < xsource such that Term(z1)\fn{Term}(z_1)source, Term(z2)\fn{Term}(z_2)source, and x=x =source

    #=(#⌢z1⌢#,#⌢z2⌢#)#.\Gn{{\eq}(} \concat z_1 \concat \Gn{,} \concat z_2 \concat{\Gn{)}}.source

    tagitemprvFalsex=#⊥#x = \Gn{\lfalse}source. tagitemprvTrue$x = Gnltrue$.

Primitive recursive recognition of formula codes

The relation Frm(x)\fn{Frm}(x)source which holds iff xxsource is the Gödel number of a formula is primitive recursive.

Proof

A sequence of symbols sssource is a formula iff there is a formation sequence s0s_0source, dots, sk−1=ss_{k-1} = ssource of formulas which records how sssource was formed from atomic formulas according to the formation rules. The code for each sis_isource (and indeed of the code of the sequence ⟨s0,…,sk−1⟩\tuple{s_0, \dots, s_{k-1}}source) is less than the code xxsource of sssource.

Exercise giving the detailed formula coding proof

Give a detailed proof of the proposition that the formula code predicate is primitive recursive along the lines of the first proof of the proposition that the term code predicate is primitive recursive.

Primitive recursive recognition of free variable occurrences

The relation FreeOcc(x,z,i)\fn{FreeOcc}(x, z, i)source, which holds iff the iisource-th symbol of the formula with Gödel number xxsource is a free occurrence of the variable with Gödel number zzsource, is primitive recursive.

Proof

Exercise.

Exercise proving the free occurrence relation primitive recursive

Prove the proposition that free occurrence is primitive recursive. You may make use of the fact that any substring of a formula which is a formula is a sub-formula of it.

Primitive recursive recognition of sentence codes

The property Sent(x)\fn{Sent}(x)source which holds iff xxsource is the Gödel number of a sentence is primitive recursive.

Proof

A sentence is a formula without free occurrences of variables. So Sent(x)\fn{Sent}(x)source holds iff

Frm(x)∧(∀i<len(x))(∀z<x)((∃j<z)z=#vj#→¬FreeOcc(x,z,i)).\fn{Frm}(x) \land \bforall{i<\len{x}}{\bforall{z<x}{(\bexists{j<z}{z=\Gn{\Obj v_j}} \lif \lnot\fn{FreeOcc}(x,z,i))}}.source

Substitution

Recall that substitution is the operation of replacing all free occurrences of a variable uusource in a formula A!Asource by a term ttsource, written A[t/u]\Subst{!A}{t}{u}source. This operation, when carried out on Gödel numbers of variables, formulas, and terms, is primitive recursive.

Primitive recursive arithmetized substitution

There is a primitive recursive function Subst(x,y,z)\fn{Subst}(x, y, z)source with the property that

Subst(#A#,#t#,#u#)=#A[t/u]#.\fn{Subst}(\Gn{!A}, \Gn{t}, \Gn{u}) = \Gn{\Subst{!A}{t}{u}}.source

Proof

We can then define a function hSubst\fn{hSubst}source by primitive recursion as follows:

hSubst(x,y,z,0)=ΛhSubst(x,y,z,i+1)={hSubst(x,y,z,i)⌢yif FreeOcc(x,z,i)append(hSubst(x,y,z,i),(x)i)otherwise.\begin{aligned} \fn{hSubst}(x, y, z, 0) & = \emptyseq \\ \fn{hSubst}(x, y, z, i+1) & = \end{aligned}\\ \begin{cases} \fn{hSubst}(x, y, z, i) \concat y & \text{if $\fn{FreeOcc}(x, z, i)$} \\ \fn{append}(\fn{hSubst}(x, y, z, i), (x)_{i}) & \text{otherwise.} \end{cases}source

Subst(x,y,z)\fn{Subst}(x, y, z)source can now be defined as hSubst(x,y,z,len(x))\fn{hSubst}(x, y, z, \len{x})source.

Primitive recursive free for substitution relation

The relation FreeFor(x,y,z)\fn{FreeFor}(x, y, z)source, which holds iff the term with Gödel number yysource is free for the variable with Gödel number zzsource in the formula with Gödel number xxsource, is primitive recursive.

Proof

Exercise.

Exercise proving the free for relation primitive recursive

Prove the proposition that the free for relation is primitive recursive

derivation in LK\Log{LK}source

Explain

In order to arithmetize derivations, we must represent derivations as numbers. Since derivations are trees of sequents where each inference carries also a label, a recursive representation is the most obvious approach: we represent a derivation as a tuple, the components of which are the end-sequent, the label, and the representations of the sub-derivations leading to the premises of the last inference.

Coding L K sequents and derivations

If Γ\Gammasource is a finite sequence of sentences, Γ=⟨A1,…,An⟩\Gamma = \tuple{!A_1, \dots, !A_n}source, then #Γ#=⟨#A1#,…,#An#⟩\Gn{\Gamma} = \tuple{\Gn{!A_1}, \dots, \Gn{!A_n}}source.

If Γ⇒Δ\Gamma \Sequent \Deltasource is a sequent, then a Gödel number of Γ⇒Δ\Gamma \Sequent \Deltasource is

#Γ⇒Δ#=⟨#Γ#,#Δ#⟩\Gn{\Gamma \Sequent \Delta} = \tuple{\Gn{\Gamma}, \Gn{\Delta}}source

If π\pisource is a derivation in LK\Log{LK}source, then #π#\Gn{\pi}source is defined as follows:

  1. If π\pisource consists only of the initial sequent Γ⇒Δ\Gamma \Sequent \Deltasource, then #π#\Gn{\pi}source is

    ⟨0,#Γ⇒Δ#⟩.\tuple{0, \Gn{\Gamma \Sequent \Delta}}.source

  2. If π\pisource ends in an inference with one or two premises, has Γ⇒Δ\Gamma \Sequent \Deltasource as its conclusion, and π1\pi_1source and π2\pi_2source are the immediate subproof ending in the premise of the last inference, then #π#\Gn{\pi}source is

    ⟨1,#π1#,#Γ⇒Δ#,k⟩ or⟨2,#π1#,#π2#,#Γ⇒Δ#,k⟩,& \tuple{1, \Gn{\pi_1}, \Gn{\Gamma \Sequent \Delta}, k} \text{ or}\\ & \tuple{2, \Gn{\pi_1}, \Gn{\pi_2}, \Gn{\Gamma \Sequent \Delta}, k},source

    respectively, where kksource is given by the following table according to which rule was used in the last inference:

    The table pairs each inference rule with its numerical code. Codes one through six are left and right weakening, contraction, and exchange in that order. Codes seven through twelve are left and right negation, conjunction, and disjunction in that order. Codes thirteen through eighteen are left and right conditional, universal quantifier, and existential quantifier in that order. Cut has code nineteen and equality has code twenty. Each rule and code is available as an explicit row in the linearized table.

    Rule:left weakeningright weakeningleft contractionright contractionleft exchangeright exchange
    kksource:123456
    Rule:left negationright negationleft conjunctionright conjunctionleft disjunctionright disjunction
    kksource:789101112
    Rule:left conditionalright conditionalleft universal quantifierright universal quantifierleft existential quantifierright existential quantifier
    kksource:131415161718
    Rule:cut=
    kksource:1920

Example coding a three node L K derivation

Consider the very simple derivation

Proof tree for the implication from a conjunction to its first conjunct

Three sequent nodes form one branch. The top initial sequent has capital A on both sides. Applying left conjunction yields the middle sequent with the conjunction of capital A and capital B on the left and capital A on the right. Applying right conditional to that middle node yields the bottom sequent with an empty left side and the implication from the conjunction to capital A on the right. Each inference has one premise.

  1. Premise: A⇒A!A \fCenter !Asource
  2. Rule or branch label: left conjunction
  3. Unary conclusion: A∧B⇒A!A \land !B \fCenter !Asource
  4. Rule or branch label: right conditional
  5. Unary conclusion: ⇒(A∧B)→A\fCenter (!A \land !B) \lif !Asource

The Gödel number of the derivation consisting only of the initial sequent would be p0=⟨0,#A⇒A#⟩p_0 = \tuple{0, \Gn{!A \Sequent !A}}source. The Gödel number of the derivation ending in the conclusion of ∧L\LeftR{\land}source would be p1=⟨1,p0,#A∧B⇒A#,9⟩p_1 = \tuple{1, p_0, \Gn{!A \land !B \Sequent !A}, 9}source (11source since ∧L\LeftR{\land}source has one premise, the Gödel number of the conclusion A∧B⇒A!A \land !B \Sequent !Asource, and 99source is the number coding ∧L\LeftR{\land}source). The Gödel number of the entire derivation then is ⟨1,p1,#⇒(A∧B)→A#,14⟩\tuple{1, p_1, \Gn{\Sequent (!A \land !B) \lif !A}, 14}source, i.e.,

⟨1,⟨1,⟨0,#A⇒A#⟩,#A∧B⇒A#,9⟩,#⇒(A∧B)→A#,14⟩.\tuple{1, \tuple{1, \tuple{0, \Gn{!A \Sequent !A}}, \Gn{!A \land !B \Sequent !A}, 9}, \Gn{\Sequent (!A \land !B) \lif !A}, 14}.source

Explain

Having settled on a representation of derivations, we must also show that we can manipulate such derivations primitive recursively, and express their essential properties and relations so. Some operations are simple: e.g., given a Gödel number ppsource of a derivation, EndSequent(p)=(p)(p)0+1\fn{EndSequent}(p) = (p)_{(p)_0+1}source gives us the Gödel number of its end-sequent and LastRule(p)=(p)(p)0+2\fn{LastRule}(p) = (p)_{(p)_0+2}source the code of its last rule. The property Sequent(s)\fn{Sequent}(s)source defined by

len(s)=2∧(∀i<len((s)0)+len((s)1))Sent(((s)0⌢(s)1)i)\len{s} = 2 \land \bforall{i<\len{(s)_0} + \len{(s)_1}}{\fn{Sent}(((s)_0 \concat (s)_1)_i)}source

holds of sssource iff sssource is the Gödel number of a sequent consisting of sentences. Some are much harder. We'll at least sketch how to do this. The goal is to show that the relation “π\pisource is a derivation of A!Asource from Γ\Gammasource” is a primitive recursive relation of the Gödel numbers of π\pisource and A!Asource.

Primitive recursiveness of checking the last L K inference

The property Correct(p)\fn{Correct}(p)source which holds iff the last inference in the derivation π\pisource with Gödel number ppsource is correct, is primitive recursive.

Proof

Γ⇒Δ\Gamma \Sequent \Deltasource is an initial sequent if either there is a sentence A!Asource such that Γ⇒Δ\Gamma \Sequent \Deltasource is A⇒A!A \Sequent !Asource, or there is a term ttsource such that Γ⇒Δ\Gamma \Sequent \Deltasource is ∅⇒t=t\emptyset \Sequent \eq[t][t]source. In terms of Gödel numbers, InitialSeq(s)\fn{InitialSeq}(s)source holds iff

(∃x<s)(Sent(x)∧s=⟨⟨x⟩,⟨x⟩⟩)∨(∃t<s)(Term(t)∧s=⟨0,⟨#=(#⌢t⌢#,#⌢t⌢#)#⟩⟩).\bexists{x < s}{} (\fn{Sent}(x) & \land s = \tuple{\tuple{x},\tuple{x}}) \lor {}\\ \bexists{t<s}{} (\fn{Term}(t) & \land s = \tuple{0, \tuple{\Gn{{\eq}(} \concat t \concat \Gn{,} \concat t \concat \Gn{)}}}).source

We also have to show that for each rule of inference RRsource the relation FollowsByR(p)\fn{FollowsBy}_R(p)source is primitive recursive, where FollowsByR(p)\fn{FollowsBy}_R(p)source holds iff ppsource is the Gödel number of derivation π\pisource, and the end-sequent of π\pisource follows by a correct application of RRsource from the immediate sub-derivations of π\pisource.

A simple case is that of the right conjunction rule. If π\pisource ends in a correct ∧R\RightR{\land}source inference, it looks like this:

Two premise right conjunction inference

The omitted subderivation pi sub one ends in a sequent with Gamma on the left and Delta followed by capital A on the right. The omitted subderivation pi sub two ends in a sequent with the same Gamma on the left and the same Delta followed by capital B on the right. Right conjunction uses those two ordered premises to conclude the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right. The blank top boxes are layout placeholders for omitted derivations, not additional axioms or empty sequents.

  1. Premise: empty premise placeholder
  2. Rule or branch label: π1\pi_1source
  3. Derived line: Γ⇒Δ,A\Gamma \fCenter \Delta, !Asource
  4. Premise: empty premise placeholder
  5. Rule or branch label: π2\pi_2source
  6. Derived line: Γ⇒Δ,B\Gamma \fCenter \Delta, !Bsource
  7. Rule or branch label: right conjunction
  8. Binary conclusion: Γ⇒Δ,A∧B\Gamma \fCenter \Delta, !A \land !Bsource

So, the last inference in the derivation π\pisource is a correct application of ∧R\RightR{\land}source iff there are sequences of sentences Γ\Gammasource and Δ\Deltasource as well as two sentences A!Asource and B!Bsource such that the end-sequent of π1\pi_1source is Γ⇒Δ,A\Gamma \Sequent \Delta, !Asource, the end-sequent of π2\pi_2source is Γ⇒Δ,B\Gamma \Sequent \Delta, !Bsource, and the end-sequent of π\pisource is Γ⇒Δ,A∧B\Gamma \Sequent \Delta, !A \land !Bsource. We just have to translate this into Gödel numbers. If s=#Γ⇒Δ#s = \Gn{\Gamma \Sequent \Delta}source then (s)0=#Γ#(s)_0 = \Gn{\Gamma}source and (s)1=#Δ#(s)_1 = \Gn{\Delta}source. So, FollowsBy∧R(p)\fn{FollowsBy}_{\RightR{\land}}(p)source holds iff

(∃g<p)(∃d<p)(∃a<p)(∃b<p)EndSequent(p)=⟨g,d⌢⟨#(#⌢a⌢#∧#⌢b⌢#)#⟩⟩∧EndSequent((p)1)=⟨g,d⌢⟨a⟩⟩∧EndSequent((p)2)=⟨g,d⌢⟨b⟩⟩∧(p)0=2∧LastRule(p)=10.& \bexists{g < p}{\bexists{d < p}{\bexists{a < p}{\bexists{b < p}{\quad}}}} \\ & \qquad \fn{EndSequent}(p) = \tuple{g, d \concat \tuple{\Gn{(} \concat a \concat \Gn{\land} \concat b \concat \Gn{)}}} \land {} \\ & \qquad \fn{EndSequent}((p)_1) = \tuple{g, d \concat \tuple{a}} \land {}\\ & \qquad \fn{EndSequent}((p)_2) = \tuple{g, d \concat \tuple{b}} \land {}\\ & \qquad (p)_0 = 2 \land \fn{LastRule}(p) = 10.source

The individual lines express, respectively, “there is a sequence (Γ\Gammasource) with Gödel number ggsource, there is a sequence (Δ\Deltasource) with Gödel number ddsource, a formula (A!Asource) with Gödel number aasource, and a formula (B!Bsource) with Gödel number bbsource,” such that “the end-sequent of π\pisource is Γ⇒Δ,A∧B\Gamma \Sequent \Delta, !A \land !Bsource,” “the end-sequent of π1\pi_1source is Γ⇒Δ,A\Gamma \Sequent \Delta, !Asource,” “the end-sequent of π2\pi_2source is Γ⇒Δ,B\Gamma \Sequent \Delta, !Bsource,” and “π\pisource has two immediate subderivations and the last inference rule is ∧R\RightR\landsource (with number 1010source).”

The last inference in π\pisource is a correct application of ∃R\RightR\lexistssource iff there are sequences Γ\Gammasource and Δ\Deltasource, a formula A!Asource, a variable xxsource, and a term ttsource, such that the end-sequent of π\pisource is Γ⇒Δ,∃xA\Gamma \Sequent \Delta, \lexists[x][!A]source and the end-sequent of π1\pi_1source is Γ⇒Δ,A[t/x]\Gamma \Sequent \Delta, \Subst{!A}{t}{x}source. So in terms of Gödel numbers, we have FollowsBy∃R(p)\fn{FollowsBy}_{\RightR\lexists}(p)source iff

(∃g<p)(∃d<p)(∃a<p)(∃x<p)(∃t<p)EndSequent(p)=⟨g,d⌢⟨#∃#⌢x⌢a⟩⟩∧EndSequent((p)1)=⟨g,d⌢⟨Subst(a,t,x)⟩⟩∧(p)0=1∧LastRule(p)=18.& \bexists{g<p}{\bexists{d<p}{\bexists{a<p}{\bexists{x<p}{\bexists{t<p}{\quad}}}}}\\ & \qquad \fn{EndSequent}(p) = \tuple{ g, d \concat \tuple{\Gn{\lexists} \concat x \concat a} } \land {}\\ & \qquad \fn{EndSequent}((p)_1) = \tuple{ g, d \concat \tuple{\fn{Subst}(a, t, x)} } \land {}\\ & \qquad (p)_0 = 1 \land \fn{LastRule}(p) = 18.source

We then define Correct(p)\fn{Correct}(p)source as

Sequent(EndSequent(p))∧[(LastRule(p)=1∧FollowsByWL(p))∨…∨(LastRule(p)=20∧FollowsBy=(p))∨(p)0=0∧InitialSeq(EndSequent(p))]\fn{Sequent}(\fn{EndSequent}(p)) \land {}\\ [(\fn{LastRule}(p) = 1 \land \fn{FollowsBy}_{\LeftR\Weakening}(p)) \lor \dots \lor {}\\ (\fn{LastRule}(p) = 20 \land \fn{FollowsBy}_{\eq}(p)) \lor {}\\ (p)_0 = 0 \land \fn{InitialSeq}(\fn{EndSequent}(p))]source

The first line ensures that the end-sequent of ppsource is actually a sequent consisting of sentences. The last line covers the case where ppsource is just an initial sequent.

Exercise on coding four further L K inference rules

Define the following properties as in the proposition on primitive recursive inference correctness:

  1. FollowsByCut(p)\fn{FollowsBy}_{\Cut}(p)source,

  2. FollowsBy→L(p)\fn{FollowsBy}_{\LeftR\lif}(p)source,

  3. FollowsBy=(p)\fn{FollowsBy}_{\eq}(p)source,

  4. FollowsBy∀R(p)\fn{FollowsBy}_{\RightR{\lforall}}(p)source.

For the last one, you will have to also show that you can test primitive recursively if the last inference of the derivation with Gödel number ppsource satisfies the eigenvariable condition, i.e., the eigenvariable aasource of the ∀R\RightR{\lforall}source does not occur in the end-sequent.

Primitive recursiveness of correct L K derivation codes

The relation Deriv(p)\fn{Deriv}(p)source which holds if ppsource is the Gödel number of a correct derivation π\pisource, is primitive recursive.

Proof

A derivation π\pisource is correct if every one of its inferences is a correct application of a rule, i.e., if every one of its sub-derivations ends in a correct inference. So, Deriv(p)\fn{Deriv}(p)source iff

(∀i<len(SubtreeSeq(p)))Correct((SubtreeSeq(p))i).\bforall{i<\len{\fn{SubtreeSeq}(p)}}{\fn{Correct}((\fn{SubtreeSeq}(p))_i)}.source

Primitive recursive proof relation from a primitive recursive premise set

Suppose Γ\Gammasource is a primitive recursive set of sentences. Then the relation PrfΓ(x,y)\Prf[\Gamma](x, y)source expressing “xxsource is the code of a derivation π\pisource of Γ0⇒A\Gamma_0 \Sequent !Asource for some finite Γ0⊆Γ\Gamma_0 \subseteq \Gammasource and yysource is the Gödel number of A!Asource” is primitive recursive.

Proof

Suppose “y∈Γy \in \Gammasource” is given by the primitive recursive predicate RΓ(y)R_\Gamma(y)source. We have to show that PrfΓ(x,y)\Prf[\Gamma](x, y)source which holds iff yysource is the Gödel number of a sentence A!Asource and xxsource is the code of an LK\Log{LK}source-derivation with end-sequent Γ0⇒A\Gamma_0 \Sequent !Asource is primitive recursive.

By the previous proposition, the property Deriv(x)\fn{Deriv}(x)source which holds iff xxsource is the code of a correct derivation π\pisource in LK\Log{LK}source is primitive recursive. If xxsource is such a code, then EndSequent(x)\fn{EndSequent}(x)source is the code of the end-sequent of π\pisource, and so (EndSequent(x))0(\fn{EndSequent}(x))_0source is the code of the left side of the end sequent and (EndSequent(x))1(\fn{EndSequent}(x))_1source the right side. So we can express “the right side of the end-sequent of π\pisource is A!Asource” as len((EndSequent(x))1)=1∧((EndSequent(x))1)0=y\len{(\fn{EndSequent}(x))_1} = 1 \land ((\fn{EndSequent}(x))_1)_0 = ysource. The left side of the end-sequent of π\pisource is of course automatically finite, we just have to express that every sentence in it is in Γ\Gammasource. Thus we can define PrfΓ(x,y)\Prf[\Gamma](x, y)source by

PrfΓ(x,y)⇔Deriv(x)∧(∀i<len((EndSequent(x))0))RΓ(((EndSequent(x))0)i)∧len((EndSequent(x))1)=1∧((EndSequent(x))1)0=y.\Prf[\Gamma](x, y) \defiff {}& \fn{Deriv}(x) \land {} \\ & \bforall{i < \len{(\fn{EndSequent}(x))_0}}{R_\Gamma(((\fn{EndSequent}(x))_0)_i)} \land {}\\ & \len{(\fn{EndSequent}(x))_1} = 1 \land ((\fn{EndSequent}(x))_1)_0 = y.source

derivation in Natural Deduction

Explain

In order to arithmetize derivations, we must represent derivations as numbers. Since derivations are trees of formulas where each inference carries one or two labels, a recursive representation is the most obvious approach: we represent a derivation as a tuple, the components of which are the number of immediate sub-derivations leading to the premises of the last inference, the representations of these sub-derivations, and the end-formula, the discharge label of the last inference, and a number indicating the type of the last inference.

Coding natural deduction derivations

If δ\deltasource is a derivation in natural deduction, then #δ#\Gn{\delta}source is defined inductively as follows:

  1. If δ\deltasource consists only of the assumption A!Asource, then #δ#\Gn{\delta}source is ⟨0,#A#,n⟩\tuple{0, \Gn{!A}, n}source. The number nnsource is 00source if it is an undischarged assumption, and the numerical label otherwise.

  2. If δ\deltasource ends in an inference with zero, one, two, or three premises, then #δ#\Gn{\delta}source is

    ⟨0,#A#,n,k⟩,⟨1,#δ1#,#A#,n,k⟩,⟨2,#δ1#,#δ2#,#A#,n,k⟩, or⟨3,#δ1#,#δ2#,#δ3#,#A#,n,k⟩,& \tuple{0, \Gn{!A}, n, k}, \\ & \tuple{1, \Gn{\delta_1}, \Gn{!A}, n, k}, \\ & \tuple{2, \Gn{\delta_1}, \Gn{\delta_2}, \Gn{!A}, n, k}, \text{ or}\\ & \tuple{3, \Gn{\delta_1}, \Gn{\delta_2}, \Gn{\delta_3}, \Gn{!A}, n, k},source

    respectively. Here δ1\delta_1source, δ2\delta_2source, δ3\delta_3source are the sub-derivations ending in the premise(s) of the last inference in δ\deltasource, A!Asource is the conclusion of the last inference in δ\deltasource, nnsource is the discharge label of the last inference (00source if the inference does not discharge any assumptions), and kksource is given by the following table according to which rule was used in the last inference.

    The table assigns sixteen rule codes. It pairs introduction and elimination for conjunction, disjunction, conditional, and negation; then intuitionistic and classical falsity rules; then introduction and elimination for universal quantification, existential quantification, and equality. The reading gives every rule and its corresponding code.

    Rule:conjunction introductionconjunction eliminationdisjunction introductiondisjunction elimination
    kksource:1234
    Rule:conditional introductionconditional eliminationnegation introductionnegation elimination
    kksource:5678
    Rule:intuitionistic falsity ruleclassical falsity ruleuniversal quantifier introductionuniversal quantifier elimination
    kksource:9101112
    Rule:existential quantifier introductionexistential quantifier eliminationequality introductionequality elimination
    kksource:13141516

Example of a recursively coded derivation

Consider the very simple derivation

Deriving a conditional from a conjunction assumption

A single branch has three nodes. The leaf is capital A and capital B under discharge label one. Conjunction elimination yields capital A without discharging it. Conditional introduction yields if capital A and capital B then capital A and discharges the original label one assumption.

  1. Premise: [A∧B]1\Discharge{!A \land !B}{1}source
  2. Rule or branch label: conjunction elimination
  3. Unary conclusion: A!Asource
  4. Discharge rule: conditional introduction; discharge label 1
  5. Unary conclusion: (A∧B)→A(!A \land !B) \lif !Asource

The Gödel number of the assumption would be d0=⟨0,#A∧B#,1⟩d_0 = \tuple{0, \Gn{!A \land !B}, 1}source. The Gödel number of the derivation ending in the conclusion of ∧Elim\Elim{\land}source would be d1=⟨1,d0,#A#,0,2⟩d_1 = \tuple{1, d_0, \Gn{!A}, 0, 2}source (11source since ∧Elim\Elim{\land}source has one premise, the Gödel number of conclusion A!Asource, 00source because no assumption is discharged, and 22source is the number coding ∧Elim\Elim{\land}source). The Gödel number of the entire derivation then is ⟨1,d1,#((A∧B)→A)#,1,5⟩\tuple{1, d_1, \Gn{((!A \land !B) \lif !A)}, 1, 5}source, i.e.,

⟨1,⟨1,⟨0,#(A∧B)#,1⟩,#A#,0,2⟩,#((A∧B)→A)#,1,5⟩.\tuple{1, \tuple{1, \tuple{0, \Gn{(!A \land !B)}, 1}, \Gn{!A}, 0, 2}, \Gn{((!A \land !B) \lif !A)}, 1, 5}.source

Explain

Having settled on a representation of derivations, we must also show that we can manipulate Gödel numbers of such derivations primitive recursively, and express their essential properties and relations. Some operations are simple: e.g., given a Gödel number ddsource of a derivation, EndFmla(d)=(d)(d)0+1\fn{EndFmla}(d) = (d)_{(d)_0+1}source gives us the Gödel number of its end-formula, DischargeLabel(d)=(d)(d)0+2\fn{DischargeLabel}(d) = (d)_{(d)_0 + 2}source gives us the discharge label and LastRule(d)=(d)(d)0+3\fn{LastRule}(d) = (d)_{(d)_0 + 3}source the number indicating the type of the last inference. Some are much harder. We'll at least sketch how to do this. The goal is to show that the relation “δ\deltasource is a derivation of A!Asource from Γ\Gammasource” is a primitive recursive relation of the Gödel numbers of δ\deltasource and A!Asource.

Primitive recursive assumption and discharge relations

The following relations are primitive recursive:

  1. A!Asource occurs as an assumption in δ\deltasource with label nnsource.

  2. All assumptions in δ\deltasource with label nnsource are of the form A!Asource (i.e., we can discharge the assumption A!Asource using label nnsource in δ\deltasource).

Proof

We have to show that the corresponding relations between Gödel numbers of formulas and Gödel numbers of derivations are primitive recursive.

  1. We want to show that Assum(x,d,n)\fn{Assum}(x, d, n)source, which holds if xxsource is the Gödel number of an assumption of the derivation with Gödel number ddsource labelled nnsource, is primitive recursive. This is the case if the derivation with Gödel number ⟨0,x,n⟩\tuple{0, x, n}source is a sub-derivation of ddsource. Note that the way we code derivations is a special case of the coding of trees introduced in the section on trees in Recursive Functions, so the primitive recursive function SubtreeSeq(d)\fn{SubtreeSeq}(d)source gives a sequence of Gödel numbers of all sub-derivations of ddsource (of length at most ddsource). So we can define

    Assum(x,d,n)⇔(∃i<d)(SubtreeSeq(d))i=⟨0,x,n⟩.\fn{Assum}(x, d, n) \defiff \bexists{i<d}{(\fn{SubtreeSeq}(d))_i = \tuple{0, x, n}}.source

  2. We want to show that Discharge(x,d,n)\fn{Discharge}(x, d, n)source, which holds if all assumptions with label nnsource in the derivation with Gödel number ddsource all are the formula with Gödel number xxsource. But this relation holds iff (∀y<d)(Assum(y,d,n)→y=x)\bforall{y<d}{(\fn{Assum}(y, d, n) \lif y = x)}source.

Primitive recursive correctness of the last inference

The property Correct(d)\fn{Correct}(d)source which holds iff the last inference in the derivation δ\deltasource with Gödel number ddsource is correct, is primitive recursive.

Proof

Here we have to show that for each rule of inference RRsource the relation FollowsByR(d)\fn{FollowsBy}_R(d)source is primitive recursive, where FollowsByR(d)\fn{FollowsBy}_R(d)source holds iff ddsource is the Gödel number of derivation δ\deltasource, and the end-formula of δ\deltasource follows by a correct application of RRsource from the immediate sub-derivations of δ\deltasource.

A simple case is that of the conjunction introduction rule. If δ\deltasource ends in a correct ∧Intro\Intro{\land}source inference, it looks like this:

Conjunction introduction from two subderivations

The left unexpanded subderivation delta sub one concludes capital A. The right unexpanded subderivation delta sub two concludes capital B. A binary conjunction introduction combines their conclusions into capital A and capital B. No assumptions are discharged by this last step.

  1. Premise: empty premise placeholder
  2. Rule or branch label: δ1\delta_1source
  3. Derived line: A!Asource
  4. Premise: empty premise placeholder
  5. Rule or branch label: δ2\delta_2source
  6. Derived line: B!Bsource
  7. Rule or branch label: conjunction introduction
  8. Binary conclusion: A∧B!A \land !Bsource

Then the Gödel number ddsource of δ\deltasource is ⟨2,d1,d2,#(A∧B)#,0,k⟩\tuple{2, d_1, d_2, \Gn{(!A \land !B)}, 0, k}source where EndFmla(d1)=#A#\fn{EndFmla}(d_1) = \Gn{!A}source, EndFmla(d2)=#B#\fn{EndFmla}(d_2) = \Gn{!B}source, n=0n=0source, and k=1k=1source. So we can define FollowsBy∧Intro(d)\fn{FollowsBy}_{\Intro\land}(d)source as

(d)0=2∧DischargeLabel(d)=0∧LastRule(d)=1∧EndFmla(d)=#(#⌢EndFmla((d)1)⌢#∧#⌢EndFmla((d)2)⌢#)#.(d)_0 = 2 \land \fn{DischargeLabel}(d) = 0 \land \fn{LastRule}(d) = 1 \land {}\\ \fn{EndFmla}(d) = {}\\ \Gn{(} \concat \fn{EndFmla}((d)_1) \concat \Gn{\land} \concat \fn{EndFmla}((d)_2) \concat \Gn{)}.source

Another simple example is the =Intro\Intro\eqsource rule. This has no premises, so (d)0=0(d)_0 = 0source, like assumptions. It also has no discharge label, i.e., n=0n=0source. However, A!Asource must be of the form t=t\eq[t][t]source, for a closed term ttsource. Here, a primitive recursive definition is

(d)0=0∧DischargeLabel(d)=0∧(∃t<d)(ClTerm(t)∧EndFmla(d)=#=(#⌢t⌢#,#⌢t⌢#)#).(d)_0 = 0 \land \fn{DischargeLabel}(d) = 0 \land {}\\ \bexists{t<d}{(\fn{ClTerm}(t) \land \fn{EndFmla}(d) = {}\\ \Gn{{\eq}(} \concat t \concat \Gn{,} \concat t \concat \Gn{)})}.source

For a more complicated example, FollowsBy→Intro(d)\fn{FollowsBy}_{\Intro{\lif}}(d)source holds iff the end-formula of δ\deltasource is of the form (A→B)(!A \lif !B)source, where the end-formula of δ1\delta_1source is B!Bsource, and any assumption in δ\deltasource labelled nnsource is of the form A!Asource. We can express this primitive recursively by

(d)0=1∧(∃a<d)(Discharge(a,(d)1,DischargeLabel(d))∧EndFmla(d)=(#(#⌢a⌢#→#⌢EndFmla((d)1)⌢#)#))(d)_0 = 1 \land {}\\ \bexists{a<d}{(\fn{Discharge}(a, (d)_1, \fn{DischargeLabel}(d)) \land {}}\\ \fn{EndFmla}(d) = (\Gn{(} \concat a \concat \Gn{\lif} \concat \fn{EndFmla}((d)_1) \concat \Gn{)}))source

(Think of aasource as the Gödel number of A!Asource).

For another example, consider existential quantifier introduction. Here, the last inference in δ\deltasource is correct iff there is a formula A!Asource, a closed term ttsource and a variable xxsource such that A[t/x]\Subst{!A}{t}{x}source is the end-formula of the derivation δ1\delta_1source and ∃xA\lexists[x][!A]source is the conclusion of the last inference. So, FollowsBy∃Intro(d)\fn{FollowsBy}_{\Intro{\lexists}}(d)source holds iff

(d)0=1∧DischargeLabel(d)=0∧(∃a<d)(∃x<d)(∃t<d)(ClTerm(t)∧Var(x)∧Subst(a,t,x)=EndFmla((d)1)∧EndFmla(d)=(#∃#⌢x⌢a)).(d)_0 = 1 \land \fn{DischargeLabel}(d) = 0 \land {} \\ \bexists{a < d}{\bexists{x<d}{\bexists{t<d}{ (\fn{ClTerm}(t) \land \fn{Var}(x) \land {}}}}\\ \fn{Subst}(a,t,x) = \fn{EndFmla}((d)_1) \land \fn{EndFmla}(d) = (\Gn{\lexists} \concat x \concat a)).source

We then define Correct(d)\fn{Correct}(d)source as

Sent(EndFmla(d))∧((LastRule(d)=1∧FollowsBy∧Intro(d))∨…∨(LastRule(d)=16∧FollowsBy=Elim(d))∨(∃n<d)(∃x<d)(d=⟨0,x,n⟩)).\fn{Sent}(\fn{EndFmla}(d)) \land ((\fn{LastRule}(d) = 1 \land \fn{FollowsBy}_{\Intro\land}(d)) \lor \dots \lor (\fn{LastRule}(d) = 16 \land \fn{FollowsBy}_{\Elim\eq}(d)) \lor \bexists{n<d}{\bexists{x<d}{(d = \tuple{0, x, n})}}).source

The first line ensures that the end-formula of ddsource is a sentence. The last line covers the case where ddsource is just an assumption.

Exercise on further inference tests

Define the following properties as in the proposition on primitive recursive inference correctness:

  1. FollowsBy→Elim(d)\fn{FollowsBy}_{\Elim{\lif}}(d)source,

  2. FollowsBy=Elim(d)\fn{FollowsBy}_{\Elim{\eq}}(d)source,

  3. FollowsBy∨Elim(d)\fn{FollowsBy}_{\Elim{\lor}}(d)source,

  4. FollowsBy∀Intro(d)\fn{FollowsBy}_{\Intro{\lforall}}(d)source.

For the last one, you will have to also show that you can test primitive recursively if the last inference of the derivation with Gödel number ddsource satisfies the eigenvariable condition, i.e., the eigenvariable aasource of the ∀Intro\Intro{\lforall}source inference occurs neither in the end-formula of ddsource nor in an open assumption of ddsource. You may use the primitive recursive predicate OpenAssum\fn{OpenAssum}source from the proposition on primitive recursive open assumptions for this.

Primitive recursive correctness of an entire derivation

The relation Deriv(d)\fn{Deriv}(d)source which holds if ddsource is the Gödel number of a correct derivation δ\deltasource, is primitive recursive.

Proof

A derivation δ\deltasource is correct if every one of its inferences is a correct application of a rule, i.e., if every one of its sub-derivations ends in a correct inference. So, Deriv(d)\fn{Deriv}(d)source iff

(∀i<len(SubtreeSeq(d)))Correct((SubtreeSeq(d))i)\bforall{i<\len{\fn{SubtreeSeq}(d)}}{\fn{Correct}((\fn{SubtreeSeq}(d))_i)}source

Primitive recursive open assumption relation

The relation OpenAssum(z,d)\fn{OpenAssum}(z, d)source that holds if zzsource is the Gödel number of an undischarged assumption A!Asource of the derivation δ\deltasource with Gödel number ddsource, is primitive recursive.

Proof

An occurrence of an assumption is discharged if it occurs with label nnsource in a sub-derivation of δ\deltasource that ends in a rule with discharge label nnsource. So A!Asource is an undischarged assumption of δ\deltasource if at least one of its occurrences is not discharged in δ\deltasource. We must be careful: δ\deltasource may contain both discharged and undischarged occurrences of A!Asource.

Consider a sequence δ0\delta_0source, dots, δk\delta_ksource where δ0=δ\delta_0 = \deltasource, δk\delta_ksource is the assumption [A]n\Discharge{!A}{n}source (for some nnsource), and δi+1\delta_{i+1}source is an immediate sub-derivation of δi\delta_isource. If such a sequence exists in which no δi\delta_isource ends in an inference with discharge label nnsource, then A!Asource is an undischarged assumption of δ\deltasource.

The primitive recursive function SubtreeSeq(d)\fn{SubtreeSeq}(d)source provides us with a sequence of Gödel numbers of all sub-derivations of δ\deltasource. Any sequence of Gödel numbers of sub-derivations of δ\deltasource is a subsequence of it. Being a subsequence of is a primitive recursive relation: Subseq(s,s′)\fn{Subseq}(s, s')source holds iff (∀i<len(s))∃j<len(s′)(s)i=(s′)j\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s')_j]}source. Being an immediate sub-derivation is as well: Subderiv(d,d′)\fn{Subderiv}(d, d')source iff (∃j<(d′)0)d=(d′)j+1\bexists{j<(d')_0}{d = (d')_{j+1}}source. So we can define OpenAssum(z,d)\fn{OpenAssum}(z, d)source by

(∃s<SubtreeSeq(d))(Subseq(s,SubtreeSeq(d))∧(s)0=d∧(∃n<d)((s)len(s)∸1=⟨0,z,n⟩∧(∀i<(len(s)∸1))(Subderiv((s)i+1,(s)i)∧DischargeLabel((s)i)≠n))).\bexists{s<\fn{SubtreeSeq}(d)}{(\fn{Subseq}(s, \fn{SubtreeSeq}(d)) \land (s)_0 = d \land {}} \\ \bexists{n<d}{((s)_{\len{s} \tsub 1} = \tuple{0, z, n} \land {}}\\ \bforall{i<(\len{s} \tsub 1)}{(\fn{Subderiv}((s)_{i+1}, (s)_i) \land {}}\\ \fn{DischargeLabel}((s)_i) \neq n))).source

Primitive recursive natural deduction proof relation relative to Gamma

Suppose Γ\Gammasource is a primitive recursive set of sentences. Then the relation PrfΓ(x,y)\Prf[\Gamma](x, y)source expressing “xxsource is the code of a derivation δ\deltasource of A!Asource from undischarged assumptions in Γ\Gammasource and yysource is the Gödel number of A!Asource” is primitive recursive.

Proof

Suppose “y∈Γy \in \Gammasource” is given by the primitive recursive predicate RΓ(y)R_\Gamma(y)source. We have to show that PrfΓ(x,y)\Prf[\Gamma](x, y)source which holds iff yysource is the Gödel number of a sentence A!Asource and xxsource is the code of a natural deduction derivation with end formula A!Asource and all undischarged assumptions in Γ\Gammasource is primitive recursive.

By the proposition on primitive recursive derivation checking, the property Deriv(x)\fn{Deriv}(x)source which holds iff xxsource is the Gödel number of a correct derivation δ\deltasource in natural deduction is primitive recursive. Thus we can define PrfΓ(x,y)\Prf[\Gamma](x, y)source by

PrfΓ(x,y)⇔Deriv(x)∧EndFmla(x)=y∧(∀z<x)(OpenAssum(z,x)→RΓ(z)).\Prf[\Gamma](x, y) \defiff {} & \fn{Deriv}(x) \land \fn{EndFmla}(x) = y \land {} \\ & \bforall{z < x}{(\fn{OpenAssum}(z, x) \lif R_\Gamma(z))}.source

Axiomatic derivation

Explain

In order to arithmetize axiomatic derivations, we must represent derivations as numbers. Since derivations are simply sequences of formulas, the obvious approach is to code every derivation as the code of the sequence of codes of formulas in it.

Coding axiomatic derivations as sequences

If δ\deltasource is an axiomatic derivation consisting of formulas A1!A_1source, dots, An!A_nsource, then #δ#\Gn{\delta}source is

⟨#A1#,…,#An#⟩.\tuple{\Gn{!A_1}, \dots, \Gn{!A_n}}.source

Example of a three line axiomatic derivation code

Consider the very simple derivation:

The three line axiomatic derivation

Line one is if capital B then capital B or capital A. Line two is the conditional from line one to if capital A then line one. Line three is if capital A then line one. The proof dependencies are from lines one and two to line three by modus ponens; this explanatory dependency is not a printed source annotation.

LineFormula
1.B→(B∨A)!B \lif (!B \lor !A)source
2.(B→(B∨A))→(A→(B→(B∨A)))(!B \lif (!B \lor !A)) \lif (!A \lif (!B \lif (!B \lor !A)))source
3.A→(B→(B∨A))!A \lif (!B \lif (!B \lor !A))source

The Gödel number of this derivation would be

⟨#B→(B∨A)#,#(B→(B∨A))→(A→(B→(B∨A)))#,#A→(B→(B∨A))#⟩.\openTuple\, & \Gn{!B \lif (!B \lor !A)}, \\ &\Gn{(!B \lif (!B \lor !A)) \lif (!A \lif (!B \lif (!B \lor !A)))},\\ & \Gn{!A \lif (!B \lif (!B \lor !A))} \,\closeTuple.source

Explain

Having settled on a representation of derivations, we must also show that we can manipulate such derivations primitive recursively, and express their essential properties and relations so. Some operations are simple: e.g., given a Gödel number ddsource of a derivation, (d)len(d)−1(d)_{\len{d}-1}source gives us the Gödel number of its end-formula. Some are much harder. We'll at least sketch how to do this. The goal is to show that the relation “δ\deltasource is a derivation of A!Asource from Γ\Gammasource” is primitive recursive in the Gödel numbers of δ\deltasource and A!Asource.

Primitive recursive axiomatic proof checks

The following relations are primitive recursive:

  1. A!Asource is an axiom.

  2. The iisource-th line in δ\deltasource is justified by modus ponens

  3. The iisource-th line in δ\deltasource is justified by QR.

  4. δ\deltasource is a correct derivation.

Proof

We have to show that the corresponding relations between Gödel numbers of formulas and Gödel numbers of derivations are primitive recursive.

  1. We have a given list of axiom schemas, and A!Asource is an axiom if it is of the form given by one of these schemas. Since the list of schemas is finite, it suffices to show that we can test primitive recursively, for each axiom schema, if A!Asource is of that form. For instance, consider the axiom schema

    B→(C→B).!B \lif (!C \lif !B).source

    A!Asource is an instance of this axiom schema if there are formulas B!Bsource and C!Csource such that we obtain A!Asource when we concatenate `((source' with B!Bsource with `→\lifsource' with `((source' with C!Csource with `→\lifsource' with B!Bsource and with `))))source'. We can test the corresponding property of the Gödel number nnsource of A!Asource, since concatenation of sequences is primitive recursive and the Gödel numbers of B!Bsource and C!Csource must be smaller than the Gödel number of A!Asource, since when the relation holds, both B!Bsource and C!Csource are sub-formulas of A!Asource. Hence, we can define:

    IsAxB→(C→B)(n)⇔(∃b<n)(∃c<n)(Sent(b)∧Sent(c)∧n=#(#⌢b⌢#→#⌢#(#⌢c⌢#→#⌢b⌢#))#).\fn{IsAx}_{!B \lif (!C \lif !B)}(n) \defiff \bexists{b< n}{ \bexists{c < n}{(\fn{Sent}(b) \land \fn{Sent}(c) \land {}}}\\ n = \Gn{(} \concat b \concat \Gn{\lif} \concat \Gn{(} \concat c \concat \Gn{\lif} \concat b \concat \Gn{))}).source

    If we have such a definition for each axiom schema, their disjunction defines the property IsAx(n)\fn{IsAx}(n)source, “nnsource is the Gödel number of an axiom.”

  2. The iisource-th line in δ\deltasource is justified by modus ponens iff there are lines jjsource and k<ik < isource where the sentence on line jjsource is some formula A!Asource, the sentence on line kksource is A→B!A \lif !Bsource, and the sentence on line iisource is B!Bsource.

    MP(d,i)⇔(∃j<i)(∃k<i)(d)k=#(#⌢(d)j⌢#→#⌢(d)i⌢#)#\fn{MP}(d, i) \defiff \bexists{j < i}{\bexists{k < i}{}}\\ (d)_k = \Gn{(} \concat (d)_j \concat \Gn{\lif} \concat (d)_i \concat \Gn{)}source

    Since bounded quantification, concatenation, and ==source are primitive recursive, this defines a primitive recursive relation.

  3. A line in δ\deltasource is justified by QR if it is of the form B→∀xA(x)!B \lif \lforall[x][!A(x)]source, a preceding line is B→A(c)!B \lif !A(c)source for some constant symbol ccsource, and ccsource does not occur in B!Bsource. This is the case iff

    1. there is a sentence B!Bsource and

    2. a formula A(x)!A(x)source with a single variable xxsource free so that

    3. line iisource contains B→∀xA(x)!B \lif \lforall[x][!A(x)]source

    4. some line j<ij < isource contains B→A[c/x]!B \lif \Subst{!A}{c}{x}source for a constant ccsource

    5. which does not occur in B!Bsource.

    All of these can be tested primitive recursively, since the Gödel numbers of B!Bsource, A(x)!A(x)source, and xxsource are less than the Gödel number of the formula on line iisource, and that of ccsource less than the Gödel number of the formula on line jjsource:

    QR1(d,i)⇔(∃j<i)(∃b<(d)i)(∃x<(d)i)(∃a<(d)i)(∃c<(d)j)(Var(x)∧Const(c)∧(d)i=#(#⌢b⌢#→#⌢#∀#⌢x⌢a⌢#)#∧(d)j=#(#⌢b⌢#→#⌢Subst(a,c,x)⌢#)#∧Sent(b)∧Sent(Subst(a,c,x))∧(∀k<len(b))(b)k≠(c)0)\fn{QR}_1(d,i)\defiff\bexists{j<i}{\bexists{b<(d)_i}{\bexists{x<(d)_i}{\bexists{a<(d)_i}{\bexists{c<(d)_j}{(\fn{Var}(x)\land\fn{Const}(c)\land(d)_i=\Gn{(}\concat b\concat\Gn{\lif}\concat\Gn{\lforall}\concat x\concat a\concat\Gn{)}\land(d)_j=\Gn{(}\concat b\concat\Gn{\lif}\concat\fn{Subst}(a,c,x)\concat\Gn{)}\land\fn{Sent}(b)\land\fn{Sent}(\fn{Subst}(a,c,x))\land\bforall{k<\len{b}}{(b)_k\neq(c)_0})}}}}}source

    Here we assume that ccsource and xxsource are the Gödel numbers of the constant and variable, respectively, considered as terms (i.e., not their symbol codes). We test that xxsource is the only free variable of A(x)!A(x)source by testing if A(x)[c/x]\Subst{!A(x)}{c}{x}source is a sentence, and ensure that ccsource does not occur in B!Bsource by requiring that every symbol of B!Bsource is different from (c)0(c)_0source.

    We leave the other version of QR as an exercise.

  4. ddsource is the Gödel number of a correct derivation iff every line in it is an axiom, or justified by modus ponens or QR. Hence:

    Deriv(d)⇔(∀i<len(d))(IsAx((d)i)∨MP(d,i)∨QR(d,i))\fn{Deriv}(d) \defiff \bforall{i < \len{d}}{(\fn{IsAx}((d)_i) \lor \fn{MP}(d,i) \lor \fn{QR}(d, i))}source

Exercise on axiom schemas and the other quantifier rule

Define the following relations as in the proposition on primitive recursive inference correctness:

  1. IsAxA→(B→(A∧B))(n)\fn{IsAx}_{!A \lif (!B \lif (!A \land !B))}(n)source,

  2. IsAx∀xA(x)→A(t)(n)\fn{IsAx}_{\lforall[x][!A(x)] \lif !A(t)}(n)source,

  3. QR2(d,i)\fn{QR}_{2}(d, i)source (for the other version of QR).

Primitive recursive axiomatic provability relation relative to Gamma

Suppose Γ\Gammasource is a primitive recursive set of sentences. Then the relation PrfΓ(x,y)\Prf[\Gamma](x, y)source expressing “xxsource is the code of a derivation δ\deltasource of A!Asource from Γ\Gammasource and yysource is the Gödel number of A!Asource” is primitive recursive.

Proof

Suppose “y∈Γy \in \Gammasource” is given by the primitive recursive predicate RΓ(y)R_\Gamma(y)source. We have to show that the relation PrfΓ(x,y)\Prf[\Gamma](x, y)source is primitive recursive, where PrfΓ(x,y)\Prf[\Gamma](x, y)source holds iff yysource is the Gödel number of a sentence A!Asource and xxsource is the code of a derivation of A!Asource from Γ\Gammasource.

By the previous proposition, the property Deriv(x)\fn{Deriv}(x)source which holds iff xxsource is the code of a correct derivation δ\deltasource is primitive recursive. However, that definition did not take into account the set Γ\Gammasource as an additional way to justify lines in the derivation. Our primitive recursive test of whether a line is justified by QR also left out of consideration the requirement that the constant ccsource is not allowed to occur in Γ\Gammasource. It is possible to amend our definition so that it takes into account Γ\Gammasource directly, but it is easier to use Deriv\fn{Deriv}source and the deduction theorem. Γ⊢A\Gamma \Proves !Asource iff there is some finite list of sentences B1!B_1source, dots, Bn∈Γ!B_n \in \Gammasource such that {B1,…,Bn}⊢A\{!B_1, \dots, !B_n\} \Proves !Asource. And by the deduction theorem, this is the case if ⊢(B1→(B2→⋯(Bn→A)⋯))\Proves (!B_1 \lif (!B_2 \lif \cdots (!B_n \lif !A)\cdots))source. Whether a sentence with Gödel number zzsource is of this form can be tested primitive recursively. So, instead of considering xxsource as the Gödel number of a derivation of the sentence with Gödel number yysource from Γ\Gammasource, we consider xxsource as the Gödel number of a derivation of a nested conditional of the above form from ∅\emptysetsource.

First, if we have a sequence of sentences, we can primitive recursively form the conditional with all these sentences as antecedents and given sentence as consequent:

hCond(s,y,0)=yhCond(s,y,n+1)=#(#⌢(s)n⌢#→#⌢hCond(s,y,n)⌢#)#Cond(s,y)=hCond(s,y,len(s))So we can define PrfΓ(x,y) byPrfΓ(x,y)⇔(∃s<sequenceBound(x,x))((x)len(x)−1=Cond(s,y)∧(∀i<len(s))(s)i∈Γ∧Deriv(x)).\fn{hCond}(s,y,0)=y \\ \fn{hCond}(s,y,n+1)=\Gn{(}\concat(s)_n\concat\Gn{\lif}\concat\fn{hCond}(s,y,n)\concat\Gn{)} \\ \fn{Cond}(s,y)=\fn{hCond}(s,y,\len{s}) \\ \intertext{So we can define $\Prf[\Gamma](x,y)$ by} \Prf[\Gamma](x,y)\defiff\bexists{s<\fn{sequenceBound}(x,x)}{((x)_{\len{x}-1}=\fn{Cond}(s,y)\land\bforall{i<\len{s}}{(s)_i\in\Gamma}\land\fn{Deriv}(x))}.source

The bound on sssource is given by considering that each (s)i(s)_isource is the Gödel number of a sub-formula of the last line of the derivation, i.e., is less than (x)len(x)−1(x)_{\len{x}-1}source. The number of antecedents B∈Γ!B \in \Gammasource, i.e., the length of sssource, is less than the length of the last line of xxsource.

Source disclosures