From 605f7148fcf555b88c9016fa57bb937ac0cd0b71 Mon Sep 17 00:00:00 2001 From: Benedict Eastaugh Date: Mon, 9 Feb 2026 16:37:41 +0000 Subject: [PATCH 1/3] 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 Date: Mon, 9 Feb 2026 16:39:29 +0000 Subject: [PATCH 2/3] 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 From bea07fd1f4a1ffa2b0138d3215552eb4264ef085 Mon Sep 17 00:00:00 2001 From: Benedict Eastaugh Date: Mon, 9 Feb 2026 20:10:29 +0000 Subject: [PATCH 3/3] =?UTF-8?q?Correct=20G=C3=B6del=20numbering=20of=20der?= =?UTF-8?q?ivations=20to=20include=20=3DIntro.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This sets their value to <0,e,n,k> where e is the Gödel number of an equation of the form t=t, n=0 is the discharge label, and k=15. This resolves an issue where it wasn't clear what Gödel number applications of =Intro should have, since Gödel numbers of applications of rules were defined only for rules with non-zero numbers of premises, while a later proof assumed that the rule had one premise which was the empty derivation tree <>. --- .../arithmetization-syntax/proofs-in-nd.tex | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex index 291fa7d4..f2681674 100644 --- a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex +++ b/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