more detail in inc/artihmetization-of-syntax

Author: rzach

incompleteness/arithmetization-syntax/coding-formulas.tex

@@ -17,20 +17,19 @@
 \begin{proof}
 The number $x$ is the G\"odel number of an atomic !!{formula} iff
 \begin{enumerate}
-\item there are $n$, $j < x$, and $z_1$, \dots, $z_n < x$ such that
+\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 z_1 \concat \Gn{,} \concat \dots \concat
-\Gn{,} \concat z_n \concat \Gn{)}
+x = \Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)} \text{, or}
 \]
-and for each $l < n$, $z_l$ is the G\"odel number of a term, or
-\item there are $z1, z_2 < x$ such that $x = z_1 \concat \Gn{\eq}
-  \concat \eq z_2$ and $z_1$ and $z_2$ are terms.
+\item there are $z_1, z_2 < x$ such that $x = z_1 \concat \Gn{\eq}
+  \concat \eq z_2$ and $\fn{Term}(z_1)$ and $\fn{Term}(z_2)$.
 \end{enumerate}
 \end{proof}
 
 \begin{prop}
 The relation $\fn{Frm}(x)$ which holds iff $x$ is the G\"odel number
-of a !!a{formula} is primitive recursive.
+of !!a{formula} is primitive recursive.
 \end{prop}
 
 \begin{proof}

incompleteness/arithmetization-syntax/coding-terms.tex

@@ -29,7 +29,7 @@
 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 formed
 from !!{constant}s and !!{variable}s according the the formation rules
-for terms. To express that a putative such formation sequence follows
+for terms. To express that such a putative formation sequence follows
 the 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
@@ -43,22 +43,23 @@
 bounded quantification.
 
 Suppose $y$ is the number that codes the sequence $s_0$, \dots, $s_{k-1}$,
-i.e., $S = \tuple{\Gn{s_0}, \dots, \Gn{s_k}}$.  It codes a formation
+i.e., $y = \tuple{\Gn{s_0}, \dots, \Gn{s_k}}$.  It codes a formation
 sequence for the term with G\"odel number~$x$ iff for all $i < k$:
 \begin{enumerate}
 \item there is a $j$ such that $(y)_i = \Gn{\Obj v_j}$, or
 \item there is a $j$ such that $(y)_i = \Gn{\Obj c_j}$, 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 z_1 \concat \Gn{,} \concat \dots
-\concat \Gn{,} \concat z_n \concat \Gn{)},
+(y)_i = \Gn{\Obj f^n_j(} \concat \fn{flatten}(z) \concat \Gn{)},
 \]
 \end{enumerate}
-and moreover $s_{k-1} = x$.
+and moreover $(y)_{k-1} = x$.  The function
+$\fn{flatten}(z)$ turns the 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{t_1, \dots, t_n}$, in (3) are
+and the code~$z$ of the sequence~$\tuple{z_1, \dots, z_n}$, in (3) are
 all less than~$y$. We can replace $k$ above with $\len{y}$. Hence we
 can express ``$y$ is the code of a formation sequence of the term with
 G\"odel number~$x$'' in a way that shows that this relation is

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

@@ -23,53 +23,143 @@
 \begin{enumerate}
 \item $\tuple{0, \Gn{\Gamma \Sequent \Delta}}$ if $\Pi$ consists only
   of the initial sequent $\Gamma \Sequent \Delta$.
-\item $\tuple{1, k, \Gn{\Gamma \Sequent \Delta}, \Gn{\Pi'}}$ if $\Pi$
+\item $\tuple{1, \Gn{\Gamma \Sequent \Delta}, k, \Gn{\Pi'}}$ if $\Pi$
   ends in an inference with one premise, $k$ is given by the following
   table according to which rule was used in the last inference, and
   $\Pi'$ is the immediate subproof ending in the premise of the last
   inference.
 
-\begin{tabular}{lcccccc}
+\begin{tabular}{lccccccc}
 \text{Rule:} & \text{Contr} & $\lnot$ left & $\lnot$ right & 
-   $\land$ left$_{1}$ & $\land$ left$_{2}$ & $\lor$ right$_1$ \\
+   $\land$ left  & $\lor$ right & $\lif$ right \\
 $k$: & 1 & 2 & 3 & 4 & 5 & 6 \\[2ex]
-\text{Rule:} & $\lor$ right$_2$ & $\lif$ right & $\lforall$ left & 
-   $\lforall$ right & $\lexists$ left & $\lexists$ right \\
-$k$: & 7 & 8 & 9 & 10 & 11 & 12
+\text{Rule:} & $\lforall$ left & 
+   $\lforall$ right & $\lexists$ left & $\lexists$ right & = \\
+$k$: & 7 & 8 & 9 & 10 & 11  
 \end{tabular}
-\item $\tuple{2, k, \Gn{\Gamma \Sequent \Delta}, \Gn{\Pi'},
+\item $\tuple{2, \Gn{\Gamma \Sequent \Delta}, k, \Gn{\Pi'},
   \Gn{\Pi''}}$ if $\Pi$ ends in an inference with two premises, $k$ is
   given by the following table according to which rule was used in the
   last inference, and $\Pi'$, $\Pi''$ are the the immediate subproof
   ending in the laft and right premise of the last inference,
   respectively.
 
-\begin{tabular}{lcccccccccccc}
-\text{Rule:} & \text{Cut} & $\land$ right & $\lor$ left & $\lif$ left & $=$\\
-$k$: & 1 & 2 & 3 & 4 & 5
+\begin{tabular}{lcccc}
+\text{Rule:} & \text{Cut} & $\land$ right & $\lor$ left & $\lif$ left \\
+$k$: & 1 & 2 & 3 & 4 
 \end{tabular}
 \end{enumerate}
 \end{defn}
 
 \begin{prop}
+\ollabel{prop:followsby}
 The following relations are primitive recursive:
 \begin{enumerate}
 \item $!A \in \Gamma$.
 \item $\Gamma \Sequent \Delta$ is an initial sequent.
 \item $\Gamma \Sequent \Delta$ follows from $\Gamma' \Sequent \Delta'$
-  (and $\Gamma' \Sequent \Delta'$) by a rule of $\Log{LK}$.
+  (and $\Gamma'' \Sequent \Delta''$) by a rule of $\Log{LK}$.
 \item $\Pi$ is a correct $\Log{LK}$-!!{derivation}.
 \end{enumerate}
 \end{prop}
 
 \begin{proof}
-Exercise.
+\begin{enumerate}
+\item $\fn{IsIn}(x, g) = \lexists[i < \len{g}][(g)_i = x]$.
+\item $\fn{InitSeq}(s) = \lexists[x < s][(\fn{Sent}(x) \land s =
+  \tuple{\tuple{x},\tuple{x}})] \lor \lexists[t<s][(\fn{Term}(t) \land
+  s = \tuple{0, t\concat \eq \concat t})]$.
+\item Here we have to show that for each rule of inference~$R$ the
+  relation $\fn{FollowsBy}_R(s, s')$ which holds if $s$ and $s'$ are
+  the G\"odel numbers of conclusion and premise of a correct
+  application of~$R$ is primitive recursive.  If $R$ has two premises,
+  $\fn{FollowsBy}_R$ of course has three arguments.
+
+For instance, $\Gamma \Sequent \Delta$ follows from $\Gamma' \Sequent
+\Delta'$ by $\lexists$right iff there is a formula~$!A$, a
+variable~$x$ and a closed term~$t$ such that $\Gamma = \Gamma'$,
+$\Subst{!A}{t}{x} \in \Delta'$, $\lexists[x][!A] \in \Delta$, and for
+every $!B \in \Delta$, either $!B = \lexists[x][!A]$ or $!B \in
+\Gamma'$.  We just have to translate into G\"odel numbers.  If $s =
+\Gn{\Gamma \Sequent \Delta}$ then $(s)_0 = \Gn{\Gamma}$ and $(s)_1 =
+\Gn{\Gamma}$. So:
+\begin{align*}
+\fn{FollowsBy}_{\lexists \text{right}}(s, s') \defiff {} & 
+\lexists[f<s][\lexists[x<s][\lexists[t<s'][(\fn{Frm}(f) \land \fn{Var}(x) \land \fn{Term}(t) \land {}]]] \\
+& \fn{Subst}(f,t,x) \in (s')_1 \land \#(\lexists) \concat x \concat f \in (s)_1 \land {}\\
+& \lforall[i < \len{(s)_1}][(((s)_1)_i = \#(\lexists) \concat x \concat f \lor ((s)_1)_i \in (s')_1)])
+\end{align*}
+\item We first define a helper relation $\fn{hDeriv}(s,n)$ which holds
+  if $s$ codes a correct derivation at least to $n$ inferences up from
+  the end sequent.  If $n=0$ we let the relation be satisfied by
+  default.  Otherwise, $\fn{hDeriv}(s, n+1)$ iff either $s$ consists
+  just of an initial sequent, or it ends in a correct inference and
+  the codes of the immediate sub!!{derivation}s satisfy
+  $\fn{nDeriv}(s, n)$.
+\begin{align*}
+\fn{nDeriv}(s, 0) \defiff {} & \True\\
+\fn{nDeriv}(s, n+1) \defiff {} & ((s)_0 = 0 \land \fn{InitialSeq}((s)_1)) \lor{}\\
+& ((s)_0 = 1 \land {}\\
+& \quad ((s)_2 = 1 \land \fn{FollowsBy}_{\text{Contr}}((s)_1, ((s)_3)_1)) \lor{}\\
+& \qquad \vdots\\
+& \quad ((s)_2 = 11 \land \fn{FollowsBy}_{=}((s)_1, ((s)_3)_1)) \land {}\\
+& \quad \fn{nDeriv}((s)_3, n)) \lor {}\\
+& ((s)_0 = 2 \land {}\\
+& \quad ((s)_2 = 1 \land \fn{FollowsBy}_{\text{Cut}}((s)_1, ((s)_3)_1), ((s)_4)_1)) \lor{}\\
+& \qquad \vdots\\
+& \quad ((s)_2 = 4 \land \fn{FollowsBy}_{\lif\text{left}}((s)_1, ((s)_3)_1), ((s)_4)_1)) \land {}\\
+& \quad \fn{nDeriv}((s)_3, n) \land \fn{nDeriv}((s)_4, n))
+\end{align*}
+This is a primitive recursive definition, if the number~$n$ is large
+enough, e.g., larger than the maximum number of inferences between an
+initial sequent and the end sequent in~$s$, it holds of $s$ iff $s$ is
+the G\"odel number of a correct !!{derivation}.  So we can now define
+$\fn{Deriv}(s)$ by $\fn{nDeriv}(s,s)$.
+\end{enumerate}
 \end{proof}
 
+\begin{prob}
+Define the following relations as in
+\olref[inc][art][plk]{prop:followsby}:
+\begin{enumerate}
+\item $\fn{FollowsBy}_{\land\text{right}}(s, s', s'')$,
+\item $\fn{FollowsBy}_{\eq}(s, s')$,
+\item $\fn{FollowsBy}_{\lforall\text{right}}(s, s', s'')$.
+\end{enumerate}
+\end{prob}
+
 \begin{prop}
 Suppose $\Gamma$ is a primitive recursive set of !!{sentence}s.  Then
-the relation ``$\Pi$ is !!a{derivation} of $\Gamma_0 \Sequent !A$ for
-some finite $\Gamma_0 \subseteq \Gamma$'' is primitive recursive.
+the relation $\fn{Pr}_\Gamma(x, y)$ expressing ``$x$ is the G\"odel
+number of a sentence~$!A$ and $y$ is the code of !!a{derivation}~$\Pi$
+of $\Gamma_0 \Sequent !A$ for some finite $\Gamma_0 \subseteq
+\Gamma$'' is primitive recursive.
 \end{prop}
 
+\begin{proof}
+Suppose ``$x \in \Gamma$'' is given by the primitive recursive
+predicate~$R_\Gamma(x)$. We have to show that $\fn{Pr}_\Gamma(x, y)$
+which holds iff $x$ is the G\"odel number of a sentence~$!A$ and $y$
+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}(y)$ which holds
+iff $y$`is the code of a correct derivation~$\Pi$ in $\Log{LK}$ is
+primitive recursive.  If $y$ is such a code, then $(y)_1$ is the code
+of the end sequent of`$\Pi$, and so $((y)_1)_0$ is the code of the
+left side of the end sequent and $((y)_1)_1$ the right side. So we can
+express ``the right side of the end sequent of~$\Pi$ is~$!A$'' as
+$\len{((y)_1)_1} = 1 \land (((y)_1)_1)_0 = x$.  The left side of the
+end sequent of $\Pi$ is of course automatically finite, we just have
+to express that every sentence in it is in~$\Gamma$.  Thus we can
+define $\fn{Pr}_\Gamma(x, y)$ by
+\begin{align*}
+\Prov_\Gamma(x, y) \defiff {}&
+\fn{Sent}(x) \land \fn{Deriv}(y) \land {} \\
+& \lforall[i <
+  \len{((y)_1)_0}][(((y)_1)_0)_i \in \Gamma] \land {}\\
+& \len{((y)_1)_1} = 1 \land (((y)_1)_1)_0 = x
+\end{align*}
+\end{proof}
+
 \end{document}