From 605f7148fcf555b88c9016fa57bb937ac0cd0b71 Mon Sep 17 00:00:00 2001
From: Benedict Eastaugh <benedict@eastaugh.net>
Date: Mon, 9 Feb 2026 16:37:41 +0000
Subject: [PATCH 1/2] Fix definition of OpenAssum(z,d).

As written, a discharge of the assumption by the final inference (0)
would be ignored. This commit fixes that.
---
 content/incompleteness/arithmetization-syntax/proofs-in-nd.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
index 88dae9a7..03774830 100644
--- a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
+++ b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
@@ -297,7 +297,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}
 

From 36fc21c0533defa4c309dcce15733d2de448a07b Mon Sep 17 00:00:00 2001
From: Benedict Eastaugh <benedict@eastaugh.net>
Date: Mon, 9 Feb 2026 16:39:29 +0000
Subject: [PATCH 2/2] Fix definition of Subseq(s,s').

As written it checks for identity between s_i and s_j, two indexes
of elements of the same sequence s, rather than indexes of elements
of two distinct sequences s and s'. This commit fixes that.
---
 content/incompleteness/arithmetization-syntax/proofs-in-nd.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
index 03774830..291fa7d4 100644
--- a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
+++ b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
@@ -288,7 +288,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