Skip to content

Commit fa2e528

Browse files
beastaughrzach
authored andcommitted
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.
1 parent 1f1b69d commit fa2e528

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@
288288
of~$\delta$. Any sequence of G\"odel numbers of sub-!!{derivation}s
289289
of~$\delta$ is a subsequence of it. Being a subsequence of is a
290290
primitive recursive relation: $\fn{Subseq}(s, s')$ holds iff
291-
$\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s)_j]}$. Being an
291+
$\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s')_j]}$. Being an
292292
immediate sub-!!{derivation} is as well: $\fn{Subderiv}(d, d')$ iff
293293
$\bexists{j<(d')_0}{d = (d')_j}$. So we can define
294294
$\fn{OpenAssum}(z, d)$ by

0 commit comments

Comments
 (0)