Incompleteness

Arithmetization of Syntax

content/incompleteness/arithmetization-syntax/arithmetization-syntax.tex

% Part: incompleteness% Chapter: arithmetization-syntax\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{inc}{art}{Arithmetization of Syntax}\begin{editorial}  Note that arithmetization for signed tableaux is not yet available.\end{editorial}\olimport{introduction}\olimport{coding-symbols}\olimport{coding-terms}\olimport{coding-formulas}\olimport{substitution}\iftag{prfSC}{%  \olimport{proofs-in-lk}}{}\iftag{prfND}{%  \olimport{proofs-in-nd}}{}\iftag{prfAX}{  \olimport{proofs-in-ax}}{}\OLEndChapterHook\end{document}

content/incompleteness/arithmetization-syntax/introduction.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{int}\olsection{Introduction}In order to connect computability and logic, we need a way to talkabout the objects of logic (symbols, terms, !!{formula}s,!!{derivation}s), operations on them, and their properties andrelations, in a way amenable to computational treatment.  We can dothis directly, by considering computable functions and relations onsymbols, sequences of symbols, and other objects built from them.Since the objects of logical syntax are all finite and built from!!a{enumerable} sets of symbols, this is possible for some models ofcomputation.  But other models of computation---such as the recursivefunctions----are restricted to numbers, their relations and functions.Moreover, ultimately we also want to be able to deal with syntaxwithin certain theories, specifically, in theories formulated in thelanguage of arithmetic.  In these cases it is necessary to\emph{arithmetize} syntax, i.e., to represent syntactic objects,operations on them, and their relations, as numbers, arithmeticalfunctions, and arithmetical relations, respectively. The idea, whichgoes 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., thereare infinitely many !!{variable}s, and even infinitely many!!{function}s of each arity~$n$. But of course it's possible to assignnumbers to symbols systematically in such a way that, say, $\Obj v_2$and $\Obj v_3$ are assigned different codes. Sequences of symbols(such as terms and !!{formula}s) are a bigger challenge. But if we candeal with sequences of numbers purely arithmetically (e.g., by thepowers-of-primes coding of sequences), we can extend the coding ofindividual symbols to coding of sequences of symbols, and then furtherto sequences or other arrangements of !!{formula}s, such as!!{derivation}s. This extended coding is called ``G\"odel numbering.''Every term, !!{formula}, and !!{derivation} is assigned a G\"odelnumber.By coding sequences of symbols as sequences of their codes, and bychoosing a system of coding sequences that can be dealt with usingcomputable functions, we can then also deal with G\"odel numbers usingcomputable functions.  In practice, all the relevant functions will beprimitive recursive.  For instance, computing the length of a sequenceand computing the $i$-th element of a sequence from the code of thesequence are both primitive recursive. If the number coding thesequence is, e.g., the G\"odel number of !!a{formula}~$!A$, weimmediately see that the length of !!a{formula} and the (code of the)$i$-th symbol in !!a{formula} can also be computed from the G\"odelnumber of~$!A$. It is a bit harder to prove that, e.g., the propertyof being the G\"odel number of a correctly formed term or of a correct!!{derivation} is primitive recursive.  It is nevertheless possible,because the sequences of interest (terms, !!{formula}s,!!{derivation}s) are inductively defined.As an example, consider the operation of substitution. If $!A$ is aformula, $x$ a variable, and $t$ a term, then $\Subst{!A}{t}{x}$ isthe result of replacing every free occurrence of~$x$ in~$!A$ by~$t$.Now suppose we have assigned G\"odel numbers to $!A$, $x$, $t$---say,$k$, $l$, and $m$, respectively.  The same scheme assigns a G\"odelnumber to $\Subst{!A}{t}{x}$, say,~$n$.  This mapping---of $k$, $l$,and $m$ to $n$---is the arithmetical analog of the substitutionoperation. When the substitution operation maps $!A$, $x$, $t$ to$\Subst{!A}{t}{x}$, the arithmetized substitution functions maps theG\"odel numbers $k$, $l$, $m$ to the G\"odel number~$n$.  We will seethat this function is primitive recursive.Arithmetization of syntax is not just of abstract interest, althoughit was originally a non-trivial insight that languages like thelanguage of arithmetic, which do not come with mechanisms for``talking about'' languages can, after all, formalize complexproperties of expressions.  It is then just a small step to ask what atheory in this language, such as Peano arithmetic, can \emph{prove}about its own language (including, e.g., whether !!{sentence}s areprovable or true).  This leads us to the famous limitative theorems ofG\"odel (about unprovability) and Tarski (the undefinability oftruth). But the trick of arithmetizing syntax is also important inorder to prove some important results in computability theory, e.g.,about the computational power of theories or the relationship betweendifferent models of computability.  The arithmetization of syntaxserves as a model for arithmetizing other objects and properties. Forinstance, it is similarly possible to arithmetize configurations andcomputations (say, of Turing machines). This makes it possible tosimulate computations in one model (e.g., Turing machines) in another(e.g., recursive functions).\end{document}

content/incompleteness/arithmetization-syntax/coding-symbols.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: coding-symbols\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{cod}\olsection{Coding Symbols}The basic language~$\Lang L$ 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 ,\]together with !!{enumerable} sets of variables and !!{constant}s, and!!{enumerable} sets of !!{function}s and !!{predicate}s of arbitraryarity.  We can assign \emph{codes} to each of these symbols in such away that every symbol is assigned a unique number as its code, and notwo different symbols are assigned the same number.  We know that thisis possible since the set of all symbols is !!{enumerable} and sothere 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 assome information about it, e.g., the arity of !!a{function}) from itscode in a computable way.  There are many possible ways of doing this,of course.  Here is one such way, which uses primitive recursivefunctions.  (Recall that $\tuple{n_0, \dots, n_k}$ is the numbercoding the sequence of numbers $n_0$, \dots, $n_k$.)\begin{defn}If $s$ is a symbol of~$\Lang L$, let the \emph{symbol code}~$\scode s$ bedefined as follows:\begin{enumerate}\item If $s$ is among the logical symbols, $\scode s$ is given by the  following table:\[\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}\]\item If $s$ is the $i$-th variable $\Obj v_i$, then $\scode s = \tuple{1, i}$.\item If $s$ is the $i$-th !!{constant}~$\Obj c_i$, then  $\scode s = \tuple{2, i}$.\item If $s$ is the $i$-th $n$-ary !!{function}~$\Obj f_i^n$, then  $\scode s = \tuple{3, n, i}$.\item If $s$ is the $i$-th $n$-ary !!{predicate}~$\Obj P_i^n$, then  $\scode s = \tuple{4, n, i}$.\end{enumerate}\end{defn}\begin{prop}The following relations are primitive recursive:\begin{enumerate}\item $\fn{Fn}(x, n)$ iff $x$ is the code of $\Obj f^n_i$ for  some~$i$, i.e., $x$ is the code of an $n$-ary !!{function}.\item $\fn{Pred}(x, n)$ iff $x$ is the code of $\Obj P^n_i$ for  some~$i$ or $x$ is the code of $\eq$ and $n = 2$, i.e., $x$ is the  code of an $n$-ary !!{predicate}.\end{enumerate}\end{prop}\begin{defn}If $s_0, \dots, s_{n-1}$ is a sequence of symbols, its \emph{G\"odel  number} is $\tuple{\scode{s_0}, \dots, \scode{s_{n-1}}}$.\end{defn}\begin{explain}Note that \emph{codes} and \emph{G\"odel numbers} are differentthings. For instance, the variable~$\Obj v_5$ has a code~$\scode{\Obj  v_5} = \tuple{1, 5} = 2^2\cdot 3^6$. But the variable~$\Obj v_5$considered as a term is also a sequence of symbols (oflength~$1$). The \emph{G\"odel number}~$\Gn{\Obj v_5}$ of the\emph{term}~$\Obj v_5$ is $\tuple{\scode{\Obj v_5}} = 2^{\scode{\Obj    v_5} + 1} = 2^{2^2\cdot 3^6 + 1}$.\end{explain}\begin{ex}Recall that if $k_0$, \dots, $k_{n-1}$ is a sequence of numbers, thenthe code of the sequence $\tuple{k_0, \dots, k_{n-1}}$ in thepower-of-primes coding is\[2^{k_0+1}\cdot3^{k_1+1}\cdot \dots \cdot p_{n-1}^{k_{n-1}+1},\]where $p_i$ is the $i$-th prime (starting with $p_0 = 2$). So forinstance, the formula $\eq[\Obj v_0][\Obj 0]$, or, more explicitly,${\eq}(\Obj v_0,\Obj c_0)$, has the G\"odel number\[\tuple{\scode{\eq},\scode{(},\scode{\Obj v_0},\scode{,}, \scode{\Obj    c_0},\scode{)}}.\]Here, $\scode{\eq}$ is $\tuple{0,7} = 2^{0+1}\cdot3^{7+1}$, $\scode{\Obj v_0}$ is $\tuple{1,0} = 2^{1+1}\cdot3^{0+1}$,etc. So $\Gn{=(\Obj v_0,\Obj c_0)}$ is\begin{multline*}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} \cdot13^{\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} \cdot13^{2^1\cdot3^{10}+1} = \\2^{13\,123}\cdot 3^{39\,367}\cdot 5^{13}\cdot 7^{354\,295}\cdot11^{25}\cdot13^{118\,099}.\end{multline*}\end{ex}\end{document}

content/incompleteness/arithmetization-syntax/coding-terms.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: coding-terms\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{trm}\olsection{Coding Terms}\begin{explain}A term is simply a certain kind of sequence of symbols: it is built upinductively from constants and variables according to the formationrules for terms.  Since sequences of symbols can be coded asnumbers---using a coding scheme for the symbols plus a way to codesequences of numbers---assigning G\"odel numbers to terms is notdifficult.  The challenge is rather to show that the property a numberhas if it is the G\"odel number of a correctly formed term iscomputable, or in fact primitive recursive.\end{explain}!!^{variable}s and !!{constant}s are the simplest terms, and testingwhether $x$ is the G\"odel number of such a term is easy:$\fn{Var}(x)$ holds if $x$ is $\Gn{\Obj v_i}$ for some~$i$. In other words,$x$~is a sequence of length~$1$ and its single element $(x)_0$ is thecode of some !!{variable}~$\Obj v_i$, i.e., $x$ is $\tuple{\tuple{1, i}}$ forsome~$i$. Similarly, $\fn{Const}(x)$ holds if $x$ is $\Gn{\Obj c_i}$ forsome~$i$. Both of these relations are primitive recursive, since ifsuch an $i$ exists, it must be $< x$:\begin{align*}  \fn{Var}(x) & \defiff \bexists{i<x}{x = \tuple{\tuple{1, i}}}\\  \fn{Const}(x) & \defiff \bexists{i<x}{x = \tuple{\tuple{2, i}}}\end{align*}\begin{prop}\ollabel{prop:term-primrec}The relations $\fn{Term}(x)$ and $\fn{ClTerm}(x)$ which hold iff $x$is the G\"odel number of a term or a closed term, respectively, areprimitive recursive.\end{prop}\begin{proof}A sequence of symbols~$s$ is a term iff there is a sequence~$s_0$,\dots, $s_{k-1} = s$ of terms which records how the term~$s$ was formedfrom !!{constant}s and !!{variable}s according to the formation rulesfor terms. To express that such a putative formation sequence followsthe formation rules it has to be the case that, for each $i < k$, either\begin{enumerate}\item $s_i$ is !!a{variable}~$\Obj v_j$, or\item $s_i$ is !!a{constant}~$\Obj c_j$, or\item $s_i$ is built from $n$ terms $t_1$, \dots, $t_n$ occurring  prior to place~$i$ using an $n$-place !!{function}~$\Obj f^n_j$.\end{enumerate}To show that the corresponding relation on G\"odel numbers isprimitive recursive, we have to express this condition primitiverecursively, i.e., using primitive recursive functions, relations, andbounded quantification.Suppose $y$ is the number that codes the sequence $s_0$, \dots, $s_{k-1}$,i.e., $y = \tuple{\Gn{s_0}, \dots, \Gn{s_{k-1}}}$.  It codes a formationsequence for the term with G\"odel number~$x$ iff for all $i < k$:\begin{enumerate}\item $\fn{Var}((y)_i)$, or\item $\fn{Const}((y)_i)$, or\item there is an $n$ and a number~$z = \tuple{z_1, \dots, z_n}$ such  that each $z_l$ is equal to some $(y)_{i'}$ for $i' < i$ and\[(y)_i = \Gn{\Obj f^n_j(} \concat \fn{flatten}(z) \concat \Gn{)},\]\end{enumerate}and moreover $(y)_{k-1} = x$.  (The function $\fn{flatten}(z)$ turnsthe sequence $\tuple{\Gn{t_1}, \dots, \Gn{t_n}}$ into $\Gn{t_1, \dots,  t_n}$ and is primitive recursive.)The indices $j$, $n$, the G\"odel numbers $z_l$ of the terms $t_l$,and the code~$z$ of the sequence~$\tuple{z_1, \dots, z_n}$, in (3) areall less than~$y$.  We can replace $k$ above with $\len{y}$.  Hence wecan express ``$y$ is the code of a formation sequence of the term withG\"odel number~$x$'' in a way that shows that this relation isprimitive recursive.We now just have to convince ourselves that there is a primitiverecursive bound on~$y$.  But if $x$ is the G\"odel number of a term,it must have a formation sequence with at most $\len{x}$ terms (sinceevery term in the formation sequence of~$s$ must start at some placein~$s$, and no two subterms can start at the same place).  The G\"odelnumber of each subterm of~$s$ is of course $\le x$.  Hence, therealways is a formation sequence with code $\le p_{k-1}^{k(x+1)}$, where$k=\len{x}$.For $\fn{ClTerm}$, simply leave out the clause for !!{variable}s.\end{proof}\begin{prob}Show that the function $\fn{flatten}(z)$, which turns the sequence$\tuple{\Gn{t_1}, \dots, \Gn{t_n}}$ into $\Gn{t_1, \dots, t_n}$, isprimitive recursive.\end{prob}\begin{prop}\ollabel{prop:num-primrec}  The function $\fn{num}(n) = \Gn{\num{n}}$ is primitive recursive.\end{prop}\begin{proof}  We define $\fn{num}(n)$ by primitive recursion:  \begin{align*}    \fn{num}(0) & = \Gn{\Obj 0}\\    \fn{num}(n+1) & = \Gn{\prime(} \concat \fn{num}(n) \concat \Gn{)}.  \end{align*}\end{proof}\end{document}

content/incompleteness/arithmetization-syntax/coding-formulas.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: coding-formulas\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{frm}\olsection{Coding \printtoken{P}{formula}}Once we have defined the relation $\fn{Term}(x)$ primitiverecursively, we can use it to define the corresponding relation for!!{formula}s, $\fn{Frm}(x)$ primitive recursively.\begin{prop}The relation $\fn{Atom}(x)$ which holds iff $x$ is the G\"odel numberof an atomic !!{formula}, is primitive recursive.\end{prop}\begin{proof}The number $x$ is the G\"odel number of an atomic !!{formula} iffone of the following holds:\begin{enumerate}\item There are $n$, $j < x$, and $z < x$ such that for each $i < n$,  $\fn{Term}((z)_i)$ and $x = $\[\Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)}.\]\item There are $z_1, z_2 < x$ such that $\fn{Term}(z_1)$,  $\fn{Term}(z_2)$, and $x = $\[\Gn{{\eq}(} \concat z_1 \concat \Gn{,} \concat z_2 \concat{\Gn{)}}.\]  \tagitem{prvFalse}{$x = \Gn{\lfalse}$.}{}  \tagitem{prvTrue}{$x = \Gn{\ltrue}$.}{}\end{enumerate}\end{proof}\begin{prop}\ollabel{prop:frm-primrec}The relation $\fn{Frm}(x)$ which holds iff $x$ is the G\"odel numberof !!a{formula} is primitive recursive.\end{prop}\begin{proof}A sequence of symbols~$s$ is !!a{formula} iff there is formationsequence~$s_0$, \dots, $s_{k-1} = s$ of !!{formula} which recordshow~$s$ was formed from atomic !!{formula}s according to theformation rules.  The code for each $s_i$ (and indeed of the code ofthe sequence $\tuple{s_0, \dots, s_{k-1}}$) is less than the code~$x$of~$s$.\end{proof}\begin{prob}Give a detailed proof of \olref[inc][art][frm]{prop:frm-primrec} alongthe lines of the first proof of\olref[inc][art][trm]{prop:term-primrec}.\end{prob}\begin{prop}\ollabel{prop:freeocc-primrec}The relation $\fn{FreeOcc}(x, z, i)$, which holds iff the $i$-thsymbol of the formula with G\"odel number~$x$ is a free occurrence ofthe variable with G\"odel number~$z$, is primitive recursive.\end{prop}\begin{proof}Exercise.\end{proof}\begin{prob}Prove \olref[inc][art][frm]{prop:freeocc-primrec}.  You may make useof the fact that any substring of !!a{formula} which is !!a{formula}is a sub-!!{formula} of it.\end{prob}\begin{prop}The property $\fn{Sent}(x)$ which holds iff $x$~is the G\"odelnumber of !!a{sentence} is primitive recursive.\end{prop}\begin{proof}A !!{sentence} is !!a{formula} without free occurrences of!!{variable}s. So $\fn{Sent}(x)$ holds iff\begin{multline*}\bforall{i<\len{x}}{\bforall{z<x}{}}\\(\bexists{j<z}{z=\Gn{\Obj v_j}} \lif \lnot\fn{FreeOcc}(x,z,i)).\end{multline*}\end{proof}\end{document}

content/incompleteness/arithmetization-syntax/substitution.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: substitution\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{sub}\olsection{Substitution}Recall that substitution is the operation of replacing all freeoccurrences of !!a{variable}~$u$ in !!a{formula}~$!A$ by a term~$t$,written $\Subst{!A}{t}{u}$. This operation, when carried out onG\"odel numbers of !!{variable}s, !!{formula}s, and terms, isprimitive recursive.\begin{prop}\ollabel{prop:subst-primrec}There is a primitive recursive function $\fn{Subst}(x, y, z)$ with theproperty that\[\fn{Subst}(\Gn{!A}, \Gn{t}, \Gn{u}) = \Gn{\Subst{!A}{t}{u}}.\]\end{prop}\begin{proof}We can then define a function $\fn{hSubst}$ by primitive recursion asfollows:\begin{multline*}\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}\end{multline*}$\fn{Subst}(x, y, z)$ can now be defined as $\fn{hSubst}(x, y, z, \len{x})$.\end{proof}\begin{prop}\ollabel{prop:free-for}The relation $\fn{FreeFor}(x, y, z)$, which holds iff the term withG\"odel number~$y$ is !!{free for} the variable with G\"odelnumber~$z$ in the formula with G\"odel number~$x$, is primitiverecursive.\end{prop}\begin{proof} Exercise. \end{proof}\begin{prob}Prove \olref[inc][art][sub]{prop:free-for}\end{prob}\end{document}

content/incompleteness/arithmetization-syntax/proofs-in-lk.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: proofs-in-lk\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{plk}\olsection{\usetoken{P}{derivation} in $\Log{LK}$}\begin{explain}In order to arithmetize !!{derivation}s, we must represent!!{derivation}s as numbers. Since !!{derivation}s are trees of sequentswhere each inference carries also a label, a recursiverepresentation is the most obvious approach: we represent a!!{derivation} as a tuple, the components of which are theend-sequent, the label, and the representations of thesub-!!{derivation}s leading to the premises of the last inference.\end{explain}\begin{defn}If $\Gamma$ is a finite sequence of !!{sentence}s, $\Gamma =\tuple{!A_1, \dots, !A_n}$, then $\Gn{\Gamma} = \tuple{\Gn{!A_1},  \dots, \Gn{!A_n}}$.If $\Gamma \Sequent \Delta$ is a sequent, then a G\"odel number of$\Gamma \Sequent \Delta$ is\[\Gn{\Gamma \Sequent \Delta} = \tuple{\Gn{\Gamma}, \Gn{\Delta}}\]If $\pi$ is !!a{derivation} in $\Log{LK}$, then $\Gn{\pi}$ is definedas follows:\begin{enumerate}\item If $\pi$ consists only  of the initial sequent $\Gamma \Sequent \Delta$, then $\Gn{\pi}$ is   \[    \tuple{0, \Gn{\Gamma \Sequent \Delta}}.  \]\item If $\pi$ ends in an inference with one or two premises, has  $\Gamma \Sequent \Delta$ as its conclusion, and $\pi_1$ and $\pi_2$ are the immediate subproof ending  in the premise of the last inference, then $\Gn{\pi}$ is   \begin{align*}    & \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},   \end{align*}  respectively, where $k$ is given by the following table according to  which rule was used in the last inference:  \begin{tabular}{lccccccc}    \text{Rule:} & \LeftR{\Weakening} & \RightR{\Weakening} &    \LeftR{\Contraction} & \RightR{\Contraction} &    \LeftR{\Exchange} & \RightR{\Exchange} \\    $k$: & 1 & 2 & 3 & 4 & 5 & 6 \\[2ex]    \text{Rule:} & \LeftR{\lnot} & \RightR{\lnot} &    \LeftR{\land} & \RightR{\land} &     \LeftR{\lor} & \RightR{\lor} \\    $k$: & 7 & 8 & 9 & 10 & 11 & 12 \\[2ex]    \text{Rule:} & \LeftR{\lif} & \RightR{\lif} &    \LeftR{\lforall} & \RightR{\lforall} &    \LeftR{\lexists} & \RightR{\lexists} \\    $k$: & 13 & 14 & 15 & 16 & 17 & 18 \\[2ex]    \text{Rule:} & \Cut & = \\    $k$: & 19 & 20  \end{tabular}\end{enumerate}\end{defn}\begin{ex}  Consider the very simple !!{derivation}  \begin{prooftree}    \Axiom$!A \fCenter !A$    \RightLabel{\LeftR{\land}}    \UnaryInf$!A \land !B \fCenter !A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter (!A \land !B) \lif !A$  \end{prooftree}  The G\"odel number of the initial sequent would be $p_0 = \tuple{0,    \Gn{!A \Sequent !A}}$.  The G\"odel number of the !!{derivation}    ending in the conclusion of~$\LeftR{\land}$ would be $p_1 =    \tuple{1, p_0, \Gn{!A \land !B \Sequent !A}, 9}$ ($1$ since    $\LeftR{\land}$ has one premise, the G\"odel number of the    conclusion~$!A \land !B \Sequent !A$, and $9$ is the number coding    $\LeftR{\land}$). The G\"odel number of the entire !!{derivation} then    is $\tuple{1, p_1, \Gn{\Sequent (!A \land !B) \lif !A)}, 14}$, i.e.,  \[  \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}.  \]\end{ex}\begin{explain}Having settled on a representation of !!{derivation}s, we must alsoshow that we can manipulate such !!{derivation}s primitive recursively,and express their essential properties and relations so.  Someoperations are simple: e.g., given a G\"odel number~$p$ of!!a{derivation}, $\fn{EndSeq}(p) = (p)_{(p)_0+1}$ gives us the G\"odelnumber of its end-sequent and $\fn{LastRule}(p) = (p)_{(p)_0+2}$ thecode of its last rule.  The property $\fn{Sequent}(s)$ defined by\[  \len{s} = 2 \land \bforall{i<\len{(s)_0} + \len{(s)_1}}{\fn{Sent}(((s)_0 \concat (s)_1)_i)}\]holds of $s$ iff $s$ is the G\"odel number of a sequent consisting of!!{sentence}s. Some are much harder.  We'll at least sketch how to dothis.  The goal is to show that the relation ``$\pi$ is!!a{derivation} of~$!A$ from~$\Gamma$'' is a primitive recursiverelation of the G\"odel numbers of $\pi$ and~$!A$.\end{explain}\begin{prop}\ollabel{prop:followsby}  The property $\fn{Correct}(p)$ which holds iff the last inference in  the !!{derivation}~$\pi$ with G\"odel number~$p$ is correct, is  primitive recursive.\end{prop}\begin{proof}  $\Gamma \Sequent \Delta$ is an initial sequent if either there  is !!a{sentence}~$!A$ such that $\Gamma \Sequent \Delta$ is $!A  \Sequent !A$, or there is a term~$t$ such that $\Gamma \Sequent  \Delta$ is $\emptyset \Sequent \eq[t][t]$.  In terms of G\"odel  numbers, $\fn{InitSeq}(s)$ holds iff  \begin{align*}  \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{)}}}).  \end{align*}  We also have to show that for each rule of inference~$R$ the  relation $\fn{FollowsBy}_R(p)$ is primitive recursive, where  $\fn{FollowsBy}_R(p)$ holds iff $p$ is the G\"odel number of  !!{derivation}~$\pi$, and the end-sequent of~$\pi$ follows  by a correct application of~$R$ from the immediate  sub-!!{derivation}s of~$\pi$.  A simple case is that of the \RightR{\land} rule. If $\pi$ ends in  a correct $\RightR{\land}$ inference, it looks like this:  \begin{prooftree}    \AxiomC{}    \RightLabel{$\pi_1$}    \Deduce$\Gamma \fCenter \Delta, !A$        \AxiomC{}    \RightLabel{$\pi_2$}    \Deduce$\Gamma \fCenter \Delta, !B$    \RightLabel{\RightR\land}    \BinaryInf$\Gamma \fCenter \Delta, !A \land !B$  \end{prooftree}  So, the last inference in the !!{derivation} $\pi$  is a correct application of $\RightR{\land}$ iff  there are sequences of !!{sentence}s $\Gamma$ and $\Delta$  as well as two !!{sentence}s $!A$ and~$!B$ such that  the end-sequent of $\pi_1$ is $\Gamma \Sequent \Delta, !A$,  the end-sequent of $\pi_2$ is $\Gamma \Sequent \Delta, !B$,  and the end-sequent of $\pi$ is $\Gamma \Sequent \Delta, !A \land !B$.  We just have to translate this into G\"odel  numbers.  If $s = \Gn{\Gamma \Sequent \Delta}$ then $(s)_0 =  \Gn{\Gamma}$ and $(s)_1 = \Gn{\Delta}$.  So,  $\fn{FollowsBy}_{\RightR{\land}}(p)$ holds iff\begin{align*}& \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.\end{align*}The individual lines express, respectively, ``there is asequence~($\Gamma$) with G\"odel number~$g$, there is asequence~($\Delta$) with G\"odel number~$d$, !!a{formula}~($!A$) withG\"odel number~$a$, and !!a{formula}~($!B$) with G\"odel number~$b$,''such that ``the end-sequent of $\pi$ is $\Gamma \Sequent \Delta, !A\land !B$,'' ``the end-sequent of $\pi_1$ is $\Gamma \Sequent \Delta,!A$,'' ``the end-sequent of $\pi_2$ is $\Gamma \Sequent \Delta, !B$,''and ``$\pi$ has two immediate subderivations and the last inferencerule is $\RightR\land$ (with number~$10$).''The last inference in~$\pi$ is a correct application of$\RightR\lexists$ iff there are sequences $\Gamma$ and $\Delta$,!!a{formula}~$!A$, a variable~$x$, and a term~$t$, such thatthe end-sequent of $\pi$ is $\Gamma \Sequent \Delta, \lexists[x][!A]$and the end-sequent of $\pi_1$ is $\Gamma \Sequent \Delta,\Subst{!A}{t}{x}$. So in terms of G\"odel numbers, we have$\fn{FollowsBy}_{\RightR\lexists}(p)$iff\begin{align*}  & \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.\end{align*}We then define $\fn{Correct}(p)$ as\begin{multline*}  \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))]\end{multline*}The first line ensures that the end-sequent of~$d$ is actually asequent consisting of !!{sentence}s. The last line covers the casewhere $p$ is just an initial sequent.\end{proof}\begin{prob}  Define the following properties as in  \olref[inc][art][plk]{prop:followsby}:  \begin{enumerate}  \item $\fn{FollowsBy}_{\Cut}(p)$,  \item $\fn{FollowsBy}_{\LeftR\lif}(p)$,  \item $\fn{FollowsBy}_{\eq}(p)$,  \item $\fn{FollowsBy}_{\RightR{\lforall}}(p)$.  \end{enumerate}  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\"odel number~$p$ satisfies the eigenvariable  condition, i.e., the eigenvariable~$a$ of the $\RightR{\lforall}$  does not occur in the end-sequent.  \end{prob}  \begin{prop}  \ollabel{prop:deriv}  The relation $\fn{Deriv}(p)$ which holds if $p$ is the G\"odel  number of a correct !!{derivation}~$\pi$, is primitive recursive.\end{prop}\begin{proof}  !!^a{derivation}~$\pi$ is correct if every one of its inferences  is a correct application of a rule, i.e., if every one of its  sub-!!{derivation}s ends in a correct inference. So, $\fn{Deriv}(d)$  iff  \[  \bforall{i<\len{\fn{SubtreeSeq}(p)}}{\fn{Correct}((\fn{SubtreeSeq}(p))_i}.  \]\end{proof}\begin{prop}Suppose $\Gamma$ is a primitive recursive set of !!{sentence}s.  Thenthe relation $\Prf[\Gamma](x, y)$ expressing ``$x$ is the code of!!a{derivation}~$\pi$ of $\Gamma_0 \Sequent !A$ for some finite$\Gamma_0 \subseteq \Gamma$ and $y$ is the G\"odel number of~$!A$'' isprimitive recursive.\end{prop}\begin{proof}Suppose ``$y \in \Gamma$'' is given by the primitive recursivepredicate~$R_\Gamma(y)$.  We have to show that $\Prf[\Gamma](x, y)$which holds iff $y$ is the G\"odel number of a sentence~$!A$ and$x$~is the code of an $\Log{LK}$-!!{derivation} with end-sequent$\Gamma_0 \Sequent !A$ is primitive recursive.By the previous proposition, the property $\fn{Deriv}(x)$ which holdsiff $x$ is the code of a correct !!{derivation}~$\pi$ in $\Log{LK}$ isprimitive recursive.  If $x$ is such a code, then $\fn{EndSequent}(x)$is the code of the end-sequent of~$\pi$, and so$(\fn{EndSequent}(x))_0$ is the code of the left side of the endsequent and $(\fn{EndSequent}(x))_1$ the right side.  So we canexpress ``the right side of the end-sequent of~$\pi$ is~$!A$'' as$\len{(\fn{EndSequent}(x))_1} = 1 \land ((\fn{EndSequent}(x))_1)_0 =x$.  The left side of the end-sequent of $\pi$ is of courseautomatically finite, we just have to express that every sentence init is in~$\Gamma$.  Thus we can define $\Prf[\Gamma](x, y)$ by\begin{align*}\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.\end{align*}\end{proof}\end{document}

content/incompleteness/arithmetization-syntax/proofs-in-nd.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: proofs-in-nd\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{pnd}\olsection{\usetoken{P}{derivation} in Natural Deduction}\begin{explain}In order to arithmetize !!{derivation}s, we must represent!!{derivation}s as numbers. Since !!{derivation}s are trees of!!{formula}s where each inference carries one or two labels, arecursive representation is the most obvious approach: we represent a!!{derivation} as a tuple, the components of which are the number ofimmediate sub-!!{derivation}s leading to the premises of the lastinference, the representations of these sub-!!{derivation}s, and theend-!!{formula}, the discharge label of the last inference, and anumber indicating the type of the last inference.\end{explain}\begin{defn}  If $\delta$ is !!a{derivation} in natural deduction, then $\Gn{\delta}$ is  defined inductively as follows:  \begin{enumerate}  \item     If $\delta$ consists only of the assumption~$!A$, then $\Gn{\delta}$    is $\tuple{0, \Gn{!A}, n}$. The number~$n$ is~$0$ if it is an    !!{undischarged} assumption, and the numerical label otherwise.  \item     If $\delta$ ends in an inference with zero, one, two, or three premises,    then $\Gn{\delta}$ is    \begin{align*}      & \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},    \end{align*}    respectively.  Here $\delta_1$, $\delta_2$, $\delta_3$ are the    sub-!!{derivation}s ending in the premise(s) of the last inference    in $\delta$, $!A$ is the conclusion of the last inference    in~$\delta$, $n$ is the discharge label of the last inference ($0$    if the inference does not discharge any assumptions), and $k$~is    given by the following table according to which rule was used in the    last inference.      \begin{tabular}{lccccccc}      \text{Rule:} & \Intro{\land} & \Elim{\land} & \Intro{\lor} & \Elim{\lor} \\      $k$: & 1 & 2 & 3 & 4  \\[1.5ex]      \text{Rule:} &  \Intro{\lif} & \Elim{\lif} & \Intro{\lnot} & \Elim{\lnot} \\      $k$: & 5 & 6 & 7 & 8 \\[1.5ex]      \text{Rule:}  &  \FalseInt & \FalseCl & \Intro{\lforall} & \Elim{\lforall} \\      $k$: & 9 & 10 & 11 & 12 \\[1.5ex]      \text{Rule:} & \Intro{\lexists} & \Elim{\lexists} & \Intro{\eq} & \Elim{\eq} \\      $k$: & 13 & 14 & 15 & 16     \end{tabular}  \end{enumerate}\end{defn}\begin{ex}  Consider the very simple !!{derivation}  \begin{prooftree}    \AxiomC{$\Discharge{!A \land !B}{1}$}    \RightLabel{\Elim{\land}}    \UnaryInfC{$!A$}    \DischargeRule{\Intro{\lif}}{1}    \UnaryInfC{$(!A \land !B) \lif !A$}  \end{prooftree}  The G\"odel number of the assumption would be $d_0 = \tuple{0,    \Gn{!A \land !B}, 1}$.  The G\"odel number of the !!{derivation}  ending in the conclusion of~$\Elim{\land}$ would be $d_1 = \tuple{1,     d_0, \Gn{!A}, 0, 2}$ ($1$ since $\Elim{\land}$ has one premise,  the G\"odel number of conclusion~$!A$, $0$ because no assumption is  discharged, and $2$ is the number coding $\Elim{\land}$). The G\"odel  number of the entire !!{derivation} then is  $\tuple{1, d_1, \Gn{((!A \land !B) \lif      !A)}, 1, 5}$, i.e.,  \[  \tuple{1, \tuple{1, \tuple{0, \Gn{(!A \land !B)}, 1}, \Gn{!A}, 0, 2},    \Gn{((!A \land !B) \lif !A)}, 1, 5}.  \]\end{ex}\begin{explain}Having settled on a representation of !!{derivation}s, we must alsoshow that we can manipulate G\"odel numbers of such !!{derivation}sprimitive recursively, and express their essential properties andrelations.  Some operations are simple: e.g., given a G\"odelnumber~$d$ of !!a{derivation}, $\fn{EndFmla}(d) = (d)_{(d)_0+1}$gives us the G\"odel number of its end-!!{formula},$\fn{DischargeLabel}(d) = (d)_{(d)_0 + 2}$ gives us the dischargelabel and $\fn{LastRule}(d) = (d)_{(d)_0 + 3}$ the number indicatingthe type of the last inference.  Some are much harder.  We'll at leastsketch how to do this.  The goal is to show that the relation``$\delta$ is !!a{derivation} of~$!A$ from~$\Gamma$'' is a primitiverecursive relation of the G\"odel numbers of $\delta$ and~$!A$.\end{explain}\begin{prop}  The following relations are primitive recursive:  \begin{enumerate}  \item $!A$ occurs as an assumption in~$\delta$ with label~$n$.  \item All assumptions in $\delta$ with label~$n$ are of the form~$!A$    (i.e., we can !!{discharge} the assumption~$!A$ using label~$n$    in~$\delta$).  \end{enumerate}\end{prop}\begin{proof}  We have to show that the corresponding relations between G\"odel  numbers of !!{formula}s and G\"odel numbers of !!{derivation}s are  primitive recursive.  \begin{enumerate}  \item We want to show that $\fn{Assum}(x, d, n)$, which holds if $x$    is the G\"odel number of an assumption of the !!{derivation} with    G\"odel number~$d$ labelled~$n$, is primitive recursive.  This is    the case if the !!{derivation} with G\"odel number~$\tuple{0, x,      n}$ is a sub-!!{derivation} of~$d$. Note that the way we code    !!{derivation}s is a special case of the coding of trees introduced in    \olref[cmp][rec][tre]{sec}, so the primitive recursive function    $\fn{SubtreeSeq}(d)$ gives a sequence of G\"odel numbers of all    sub-!!{derivation}s of~$d$ (of length at most $d$). So we can    define    \[    \fn{Assum}(x, d, n) \defiff \bexists{i<d}{(\fn{SubtreeSeq}(d))_i =      \tuple{0, x, n}}.    \]  \item We want to show that $\fn{Discharge}(x, d, n)$, which holds if    all assumptions with label~$n$ in the !!{derivation} with G\"odel    number~$d$ all are the !!{formula} with G\"odel number~$x$.  But    this relation holds iff $\bforall{y<d}{(\fn{Assum}(y, d, n) \lif y      = x)}$.  \end{enumerate}\end{proof}\begin{prop}  \ollabel{prop:followsby}  The property $\fn{Correct}(d)$ which holds iff the last inference in  the !!{derivation}~$\delta$ with G\"odel number~$d$ is correct, is  primitive recursive.\end{prop}\begin{proof}  Here we have to show that for each rule of inference~$R$ the  relation $\fn{FollowsBy}_R(d)$ is primitive recursive, where  $\fn{FollowsBy}_R(d)$ holds iff $d$ is the G\"odel number of  !!{derivation}~$\delta$, and the end-!!{formula} of~$\delta$ follows  by a correct application of~$R$ from the immediate  sub-!!{derivation}s of~$\delta$.  A simple case is that of the \Intro{\land} rule. If $\delta$ ends in  a correct $\Intro{\land}$ inference, it looks like this:  \begin{prooftree}    \AxiomC{}    \RightLabel{$\delta_1$}    \DeduceC{$!A$}        \AxiomC{}    \RightLabel{$\delta_2$}    \DeduceC{$!B$}    \RightLabel{\Intro\land}    \BinaryInfC{$!A \land !B$}  \end{prooftree}  Then the G\"odel number~$d$ of~$\delta$ is $\tuple{2, d_1, d_2,    \Gn{(!A \land !B)}, 0, k}$ where $\fn{EndFmla}(d_1) = \Gn{!A}$,  $\fn{EndFmla}(d_2) = \Gn{!B}$, $n=0$, and $k=1$. So we can define  $\fn{FollowsBy}_{\Intro\land}(d)$ as  \begin{multline*}    (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{)}.  \end{multline*}  Another simple example is the $\Intro\eq$ rule. This has no premises,  so $(d)_0 = 0$, like assumptions. It also has no discharge label,  i.e., $n=0$.  However, $!A$ must be of the form $\eq[t][t]$, for a  closed term~$t$. Here, a primitive recursive definition is  \begin{multline*}    (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{)})}.  \end{multline*}  For a more complicated example, $\fn{FollowsBy}_{\Intro{\lif}}(d)$  holds iff the end-!!{formula} of~$\delta$ is of the form $(!A \lif  !B)$, where the end-!!{formula} of $\delta_1$ is~$!B$, and any  assumption in~$\delta$ labelled~$n$ is of the form~$!A$.  We can  express this primitive recursively by  \begin{multline*}    (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{)}))  \end{multline*}  (Think of $a$ as the G\"odel number of~$!A$).  For another example, consider \Intro{\lexists}.  Here, the last  inference in~$\delta$ is correct iff there is !!a{formula}~$!A$, a  closed term~$t$ and !!a{variable}~$x$ such that $\Subst{!A}{t}{x}$  is the end-!!{formula} of the !!{derivation}~$\delta_1$ and  $\lexists[x][!A]$ is the conclusion of the last inference.  So,  $\fn{FollowsBy}_{\Intro{\lexists}}(d)$ holds iff  \begin{multline*}    (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)).  \end{multline*}  We then define $\fn{Correct}(d)$ as  \begin{multline*}    \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})}}.  \end{multline*}  The first line ensures that the end-!!{formula} of~$d$ is a  sentence. The last line covers the case where $d$ is just an  assumption.\end{proof}\begin{prob}  Define the following properties as in  \olref[inc][art][pnd]{prop:followsby}:  \begin{enumerate}  \item $\fn{FollowsBy}_{\Elim{\lif}}(d)$,  \item $\fn{FollowsBy}_{\Elim{\eq}}(d)$,  \item $\fn{FollowsBy}_{\Elim{\lor}}(d)$,  \item $\fn{FollowsBy}_{\Intro{\lforall}}(d)$.  \end{enumerate}  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\"odel number~$d$ satisfies the eigenvariable  condition, i.e., the eigenvariable~$a$ of the $\Intro{\lforall}$  inference occurs neither in the end-!!{formula} of~$d$ nor in an  open assumption of~$d$. You may use the primitive recursive  predicate $\fn{OpenAssum}$ from  \olref[inc][art][pnd]{prop:openassum} for this.\end{prob}\begin{prop}  \ollabel{prop:deriv}  The relation $\fn{Deriv}(d)$ which holds if $d$ is the G\"odel  number of a correct !!{derivation}~$\delta$, is primitive recursive.\end{prop}\begin{proof}  !!^a{derivation}~$\delta$ is correct if every one of its inferences  is a correct application of a rule, i.e., if every one of its  sub-!!{derivation}s ends in a correct inference. So, $\fn{Deriv}(d)$  iff  \[  \bforall{i<\len{\fn{SubtreeSeq}(d)}}{\fn{Correct}((\fn{SubtreeSeq}(d))_i)}  \]\end{proof}\begin{prop}  \ollabel{prop:openassum} The relation $\fn{OpenAssum}(z, d)$ that  holds if $z$ is the G\"odel number of !!a{undischarged} assumption~$!A$  of the !!{derivation}~$\delta$ with G\"odel number~$d$, is primitive  recursive.\end{prop}\begin{proof}  An occurrence of an assumption is !!{discharged} if it occurs with  label~$n$ in a sub-!!{derivation} of~$\delta$ that ends in a rule  with discharge label~$n$. So $!A$ is !!a{undischarged} assumption  of~$\delta$ if at least one of its occurrences is not !!{discharged}  in~$\delta$. We must be careful: $\delta$ may contain both  !!{discharged} and !!{undischarged} occurrences of~$!A$.  Consider a sequence $\delta_0$, \dots, $\delta_k$ where $\delta_0 =  \delta$, $\delta_k$ is the assumption $\Discharge{!A}{n}$  (for some~$n$), and $\delta_{i+1}$ is an immediate sub-!!{derivation}  of~$\delta_i$. If such a sequence exists in which no $\delta_i$  ends in an inference with discharge label~$n$, then $!A$ is  !!a{undischarged} assumption of~$\delta$.  The primitive recursive function $\fn{SubtreeSeq}(d)$ provides us  with a sequence of G\"odel numbers of all sub-!!{derivation}s  of~$\delta$. Any sequence of G\"odel numbers of sub-!!{derivation}s  of~$\delta$ is a subsequence of it. Being a subsequence of is a  primitive recursive relation: $\fn{Subseq}(s, s')$ holds iff  $\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s')_j]}$. Being an  immediate sub-!!{derivation} is as well: $\fn{Subderiv}(d, d')$ iff  $\bexists{j<(d')_0}{d = (d')_j}$. So we can define  $\fn{OpenAssum}(z, d)$ by  \begin{multline*}    \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))).  \end{multline*}\end{proof}\begin{prop}  \ollabel{prop:prf-prim-rec}  Suppose $\Gamma$ is a primitive recursive set of !!{sentence}s.  Then the relation $\Prf[\Gamma](x, y)$ expressing ``$x$ is the code  of !!a{derivation}~$\delta$ of $!A$ from !!{undischarged}  assumptions in~$\Gamma$ and $y$ is the G\"odel number of~$!A$'' is  primitive recursive.\end{prop}\begin{proof}  Suppose ``$y \in \Gamma$'' is given by the primitive recursive  predicate~$R_\Gamma(y)$.  We have to show that $\Prf[\Gamma](x, y)$  which holds iff $y$ is the G\"odel number of a sentence~$!A$ and  $x$~is the code of a natural deduction !!{derivation} with end  !!{formula}~$!A$ and all !!{undischarged} assumptions in~$\Gamma$ is  primitive recursive.  By \olref{prop:deriv}, the property $\fn{Deriv}(x)$ which holds iff  $x$ is the G\"odel number of a correct !!{derivation}~$\delta$ in  natural deduction is primitive recursive. Thus we can define  $\Prf[\Gamma](x, y)$ by  \begin{align*}    \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))}.  \end{align*}\end{proof}\end{document}

content/incompleteness/arithmetization-syntax/proofs-in-ax.tex

% Part: incompleteness% Chapter: arithmetization-syntax% Section: proofs-in-ax\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{art}{pax}\olsection{Axiomatic \usetoken{P}{derivation}}\begin{explain}In order to arithmetize axiomatic !!{derivation}s, we must represent!!{derivation}s as numbers. Since !!{derivation}s are simply sequencesof !!{formula}s, the obvious approach is to code every !!{derivation}as the code of the sequence of codes of !!{formula}s in it.\end{explain}\begin{defn}If $\delta$ is an axiomatic !!{derivation} consisting of !!{formula}s$!A_1$, \dots,~$!A_n$, then $\Gn{\delta}$ is\[\tuple{\Gn{!A_1}, \dots, \Gn{!A_n}}.\]\end{defn}\begin{ex}  Consider the very simple !!{derivation}:  \begin{derivation}  1. & $!B \lif (!B \lor !A)$ \\  2. & $(!B \lif (!B \lor !A)) \lif (!A  \lif (!B \lif (!B \lor !A)))$\\  3. & $!A  \lif (!B \lif (!B \lor !A))$  \end{derivation}  The G\"odel number of this !!{derivation} would be  \begin{align*}  \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.  \end{align*}\end{ex}\begin{explain}Having settled on a representation of !!{derivation}s, we must alsoshow that we can manipulate such !!{derivation}s primitive recursively, andexpress their essential properties and relations so.  Some operationsare simple: e.g., given a G\"odel number~$d$ of !!a{derivation},$(d)_{\len{d}-1}$ gives us the G\"odel number of its end-!!{formula}.  Some aremuch harder.  We'll at least sketch how to do this.  The goal is toshow that the relation ``$\delta$ is !!a{derivation} of~$!A$from~$\Gamma$'' is primitive recursive in the G\"odel numbers of$\delta$ and~$!A$.\end{explain}\begin{prop}\ollabel{prop:followsby}The following relations are primitive recursive:\begin{enumerate}\item $!A$ is an axiom.\item The $i$-th line in $\delta$ is justified by modus ponens\item The $i$-th line in $\delta$ is justified by \QR.\item $\delta$ is a correct !!{derivation}.\end{enumerate}\end{prop}\begin{proof}We have to show that the corresponding relations between G\"odelnumbers of !!{formula}s and  G\"odel numbers of !!{derivation}s are primitive recursive.\begin{enumerate}\item We have a given list of axiom schemas, and $!A$ 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$ is of that form. For  instance, consider the axiom schema  \[  !B \lif (!C \lif !B).  \]  $!A$ is an instance of this axiom schema if there are !!{formula}s  $!B$ and $!C$ such that we obtain $!A$ when we concatenate `$($'  with $!B$ with `$\lif$' with `$($' with $!C$ with `$\lif$' with $!B$  and with~`$))$'. We can test the corresponding property of the  G\"odel number $n$ of~$!A$, since concatenation of sequences is  primitive recursive and the G\"odel numbers of $!B$ and $!C$ must  be smaller than the G\"odel number of~$!A$, since when the relation  holds, both $!B$ and $!C$ are sub-!!{formula}s of~$!A$. Hence, we  can define:  \begin{multline*}  \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{))}).  \end{multline*}  If we have such a definition for each axiom schema, their  disjunction defines the property $\fn{IsAx}(n)$, ``$n$~is the  G\"odel number of an axiom.''\item The $i$-th line in $\delta$ is justified by modus ponens iff there  are lines $j$ and $k < i$ where the !!{sentence} on line~$j$ is some  formula $!A$, the sentence on line~$k$ is $!A \lif !B$, and the  sentence on line~$i$ is~$!B$.  \begin{multline*}    \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{)}  \end{multline*}  Since bounded quantification, concatenation, and $=$ are primitive  recursive, this defines a primitive recursive relation. \item A line in $\delta$ is justified by \QR{} if it is of the form  $!B \lif \lforall[x][!A(x)]$, a preceding line is $!B \lif !A(c)$  for some !!{constant}~$c$, and $c$ does on occur in~$!B$. This is  the case iff  \begin{enumerate}  \item there is !!a{sentence}~$!B$ and  \item !!a{formula}~$!A(x)$ with a single variable~$x$ free so that  \item line $i$ contains $!B \lif \lforall[x][!A(x)]$  \item some line $j < i$ contains $!B \lif \Subst{!A}{c}{x}$ for a constant~$c$  \item which does not occur in~$!B$.  \end{enumerate}  All of these can be tested primitive recursively, since the G\"odel  numbers of $!B$, $!A(x)$, and $x$ are less than the G\"odel number of the  formula on line~$i$, and that of $a$ less than the G\"odel number of the  formula on line~$j$:  \begin{multline*}    \fn{QR}_1(d, i) \defiff \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})  \end{multline*}  Here we assume that $c$ and $x$ are the G\"odel numbers of the  variable and constant considered as terms (i.e., not their symbol  codes).  We test that $x$ is the only free variable of~$!A(x)$ by  testing if $\Subst{!A(x)}{c}{x}$ is !!a{sentence}, and ensure that  $c$ does not occur in $!B$ by requiring that every symbol of~$!B$ is  different from~$c$.  We leave the other version of \QR{} as an exercise.\item $d$ is the G\"odel number of a correct !!{derivation} iff every  line in it is an axiom, or justified by modus ponens or~\QR. Hence:  \[  \fn{Deriv}(d) \defiff \bforall{i < \len{d}}{(\fn{IsAx}((d)_i) \lor    \fn{MP}(d,i) \lor \fn{QR}(d, i))}  \]\end{enumerate}\end{proof}\begin{prob}Define the following relations as in\olref[inc][art][pax]{prop:followsby}:\begin{enumerate}\item $\fn{IsAx}_{!A \lif (!B \lif (!A \land !B))}(n)$,\item $\fn{IsAx}_{\lforall[x][!A(x)] \lif !A(t)}(n)$,\item $\fn{QR}_{2}(d, i)$ (for the other version of \QR).\end{enumerate}\end{prob}\begin{prop}Suppose $\Gamma$ is a primitive recursive set of !!{sentence}s.  Thenthe relation $\Prf[\Gamma](x, y)$ expressing ``$x$ is the code of!!a{derivation}~$\delta$ of $!A$ from~$\Gamma$ and $y$ is the G\"odelnumber of~$!A$'' is primitive recursive.\end{prop}\begin{proof}Suppose ``$y \in \Gamma$'' is given by the primitive recursivepredicate~$R_\Gamma(y)$.  We have to show that the relation$\Prf[\Gamma](x, y)$ is primitive recursive, where $\Prf[\Gamma](x,y)$ holds iff $y$ is the G\"odel number of !!a{sentence}~$!A$ and$x$~is the code of !!a{derivation} of~$!A$ from $\Gamma$.By the previous proposition, the property $\fn{Deriv}(x)$ which holdsiff $x$ is the code of a correct !!{derivation}~$\delta$ is primitiverecursive. However, that definition did not take into account the set$\Gamma$ as an additional way to justify lines in the !!{derivation}. Ourprimitive recursive test of whether a line is justified by \QR{} alsoleft out of consideration the requirement that the constant~$c$ is notallowed to occur in~$\Gamma$. It is possible to amend our definition sothat it takes into account $\Gamma$ directly, but it is easier to use$\fn{Deriv}$ and the deduction theorem. $\Gamma \Proves !A$ iffthere is some finite list of !!{sentence}s $!B_1$, \dots, $!B_n \in\Gamma$ such that $\{!B_1, \dots, !B_n\} \Proves !A$. And by thededuction theorem, this is the case if $\Proves (!B_1 \lif (!B_2 \lif\cdots (!B_n \lif !A)\cdots))$. Whether !!a{sentence} with G\"odelnumber~$z$ is of this form can be tested primitive recursively.  So,instead of considering $x$ as the G\"odel number of !!a{derivation} ofthe !!{sentence} with G\"odel number~$y$ \emph{from $\Gamma$}, we consider$x$ as the G\"odel number of !!a{derivation} of a nested conditionalof the above form from~$\emptyset$.First, if we have a sequence of !!{sentence}s, we can primitiverecursively form the conditional with all these sentences asantecedents and given !!{sentence} as consequent:\begin{align*}  \fn{hCond}(s, y, 0) & = y \\  \fn{hCond}(s, y, n+1) & = \Gn{(} \concat (s)_{n} \concat \Gn{\lif}  \concat \fn{Cond}(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)}{(} \\  &\qquad (x)_{\len{x}-1} = \fn{Cond}(s,y) \land {} \\  &\qquad\bforall{i<\len{s}}{(s)_i \in \Gamma} \land {} \\  &\qquad\fn{Deriv}(x)).\end{align*}The bound on~$s$ is given by considering that each $(s)_i$ is theG\"odel number of a sub-!!{formula} of the last line of the !!{derivation},i.e., is less than $(x)_{\len{x}-1}$. The number of antecedents $!B\in \Gamma$, i.e., the length of~$s$, is less than the length of thelast line of~$x$.\end{proof}\end{document}