Gödel numbering of natural deduction derivations using =Intro Inc fixes

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

@@ -30,9 +30,10 @@
     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 one, two, or three premises,
+    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,
@@ -175,12 +176,12 @@
     \concat \fn{EndFmla}((d)_2) \concat \Gn{)}.
   \end{multline*}
 
-  Another simple example is the $\Intro\eq$ rule. Here the premise is
-  an empty !!{derivation}, i.e., $(d)_1 = 0$, and no discharge label,
+  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 = 1 \land (d)_1 = 0 \land \fn{DischargeLabel}(d) = 0 \land {}\\
+    (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{)})}.
@@ -288,7 +289,7 @@
   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
+  $\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
@@ -297,7 +298,7 @@
       \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+1}) \neq n))).
+      \fn{DischargeLabel}((s)_i) \neq n))).
   \end{multline*}
 \end{proof}