Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom

Question

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.)

Background: I'm trying to understand the proof that V. A. Yankov (aka “Jankov”, “Ânkov” in ISO-9 transliteration, В. А. Янков in the original) gives in a 1963 paper of the nonrealizability of Scott's axiom $((¬¬a⇒a)⇒(¬a∨¬¬a))⇒(¬a∨¬¬a)$. It doesn't help that the paper (a) is in Russian (a language I learned a bit in school 30-ish years ago, but largely forgot since), (b) is very terse (it's not even clear to me whether Yankov is giving a sketch of proof to be detailed elsewhere and he never got around to it, or whether not proving the lemmas is his habitual mode of writing), and (c) probably contains at least one misprint that I don't see how to fix. Combine this with the fact that I'm not too familiar with this sort of reasoning, and I definitely need a bit of help.

The main difficulty isn't linguistic (thanks to Google Translate and all that), but I could be missing some clues in the original, so I'll copy both the Russian and a translation of the excerpt I'm interested in below.

(This argument does not seem to have been translated, or reproduced anywhere since. E.g., in the 2022 book V. A. Yankov on Non-Classical Logics, History and Philosophy of Mathematics edited by Citkin and Vadoulakis, Citkin's chapter “V. Yankov's Contributions to Propositional Logic” references the theorem in question (as theorem 2.11 in section 2.8 of the book), but does not reproduce the argument. Nor is it reproduced in Plisko's oft-cited 2009 paper “A Survey of Propositional Realizability Logic”. If I manage to fully decipher it, I'll try to put up a more readable paraphrase somewhere.)

Context: The original paper is: В. А. Янков (V. A. Yankov), “О реализуемых формулах логики высказываний” (“On the realizable formulae of propositional logic”), Доклады Академии наук СССР (Dokl. Akad. Nauk SSSR) 151:5 (1963), 1035–1037. I'm interested in the proof of theorem 2 (which is about one page long), but mostly I'm confused about the definitions at the start of the proof, and that's what my question is about.

So the context is, Yankov wants to prove that $((¬¬a⇒a)⇒(¬a∨¬¬a))⇒(¬a∨¬¬a)$ is not realizable and, in fact, that any realizable formula must take the value true in a certain 7-element Heyting algebra which is shown as figure 1 on page 1036 (I won't reproduce it here because it's not directly relevant to my question): this is his “theorem 2”.

The proof of the theorem is limited to the statement of five lemmas. Let me just sketch what is going on. After some initial definitions of $Q, P, R$ which is what I'm asking about, Yankov proves that (1) $∀y ¬¬ ∃z R(y,z)$, then he calls $g$ a one-to-one computable function whose range is a computably enumerable set but not computable set and $G$ its graph ($G(y,x)$ meaning $g(y)=x$) and defines $S(x) :⇔ ∃y(G(y,x) ∧ ∃z R(y,z))$ and proves (2) $∀x(¬¬S(x) ⇔ ∃y G(x,y))$, then (3) if $k$ realizes $¬¬S(x) ⇒ S(x)$ and if $g(y)=x$ then $k>y$, and (4) for all $x$, the formula $(¬¬S(x) ⇒ S(x)) ⇔ (S(x) ∨ ¬S(x))$ is realizable, but $∀x(¬¬S(x) ∨ ¬S(x))$ is not (I won't copy the statement of the fifth and final lemma, but the fourth is enough to get the nonrealizability of Scott's axiom).

The text: Here is the excerpt I'm trying make sense of, first in Russian (reproduced as faithfully as I could):

Наметим основные этапы доказательства этой теоремы ($\newcommand{\binexp}{\mathbin{\mathrm{exp}}}a \binexp b$ будем в дальнейшем обозначать то же, что и $a^b$).

Пусть $K_{y,z}$ — множество натуральных чисел вида

$$(2 \binexp y) · (3 \binexp ((2 \binexp p) · (3 \binexp ((2 \binexp z) . (3 \binexp q)))))$$

при данных y и z (все строчные латинские буквы означают переменные, которые в последующем будут пробегать натуральные числа). Тогда содержательный предикат «$t$ есть геделев номер общерекурсивной функции, значения которой принадлежат $K_{y,z}$», может быть выражен формулой $Q(t,y,z)$ логико-арифметического языка из (¹). Пусть $P(y,z$) — формула $∀t (t≤y ⊃ ¬Q(t,y,z))$, а $R(y,z)$ — формула $P(y,z) \,\&\, ∀t (t<z ⊃ ⊃ ¬P(y,z))$.

Лемма 1. Имеет место предложение, выражаемое формулой

$$∀y ¬¬∃z R(y,z)$$

Then in English translation (by Google Translate, then slightly edited):

Let us outline the main stages of the proof of this theorem ($a \binexp b$ will now denote $a^b$).

Let $K_{y,z}$ be the set of natural numbers of the form

$$(2 \binexp y) · (3 \binexp ((2 \binexp p) · (3 \binexp ((2 \binexp z) . (3 \binexp q)))))$$

given y and z (all lowercase Latin letters mean variables that will subsequently run through natural numbers). Then the meaningful[?] predicate “$t$ is the Gödel number of a general recursive function whose values belong to $K_{y,z}$” can be expressed by the formula $Q(t,y,z)$ of the logical-arithmetic language from (¹). Let $P(y,z)$ be the formula $∀t (t≤y ⊃ ¬Q(t,y,z))$, and $R(y,z)$ be the formula $P(y,z) \,\&\, ∀t (t<z ⊃ ⊃ ¬P(y,z))$.

Lemma 1. The following holds:

$$∀y ¬¬∃z R(y,z)$$

Reference (¹) is just a reference to Kleene's Introduction to metamathematics.

The motivation for $K_{y,z} := \lbrace \langle y, \langle p,\langle z,q\rangle\rangle\rangle : p,q\in\mathbb{N} \rbrace$ where $\langle i,j\rangle := 2^i 3^j$ already leaves me a bit perplexed.

But the really puzzling part for me is the definition of $R(y,z)$. I left Yankov's notation of $⊃$ for implication, but I don't know what to make of $⊃⊃$: it's probably just a typo (or line break convention) since one $⊃$ occurs at the end of a line and the next one at the start of the next line, but I'm not sure. Even if I take $⊃⊃$ to mean just $⊃$, the quantifier still makes no sense: why would you quantify on $t$ less than $z$ a formula where $t$ doesn't occur? So there's certainly another typo here, but since I have no intuition of what these definitions are trying to achieve, I don't know whether I should correct $R(y,z)$ as $P(y,z) ∧ ∀t (t<z ⇒ ¬P(y,t))$ or $P(y,z) ∧ ∀t (t<y ⇒ ¬P(t,z))$ or something else.

So, anyway:

Question: Does someone understand what Yankov is trying to do with these definitions? Most importantly, how do I fix the one for $R$?

Answer 1

So, I didn't understand the exact details of what Yankov was trying to do with his $K$ and $Q,P,R$ (the definition of $K$ probably depends on the details of the coding he uses for realizability, which I don't know), but I think I can infer a proof of theorem 2 from his list of lemmata, at least insofar as showing that Scott's axiom $((¬¬a⇒a)⇒(¬a∨¬¬a))⇒(¬a∨¬¬a)$ isn't realizable, which should be essentially Yankov's argument, as follows.

Conventions: Fix a standard Gödel numbering $(φ_x)$ of general recursive functions of one variable (which I'll abusively call “Turing machines”). As is quite standard, I will be writing $T$ for Kleene's (primitive recursive) normal form predicate, that is, $T(x,i,y)$ means “$y$ encodes a computation trace of $φ_x$ for input $i$” (and in particular, $φ_x(i){\downarrow}$ will be taken to mean $∃y.T(x,i,y)$, where this $y$ is in fact unique) and $U$ for the corresponding result extraction function (so, $φ_x(i){\downarrow} = n$ means $∃y.(T(x,i,y)∧U(y)=n)$). To make the argument slightly more digestable, I will be assuming a coding of pairs $⟨m,n⟩$ such that $⟨m,n⟩ ≥ \max(m,n)$ (see footnote 1 below for where this is used).

The key idea: The core of the proof is this: if $S_0(x)$ denotes $φ_x(0){\downarrow}$ (i.e., $∃y.T(x,0,y)$), then the formula “$∀ x. (¬¬S_0(x) ∨ ¬ S_0(x))$” is not realizable (because a realizer for this would solve the Halting problem by deciding whether $φ_x(0){\downarrow}$). Now we want to “tweak” $S_0(x)$ and replace it by some $S(x)$ which is classically equivalent to it, so $∀ x. (S(x) ∨ ¬ S(x))$ still isn't realizable, but so as to make “$∀ x. ((¬¬S(x) ⇒ S(x)) ⇒ (S(x) ∨ ¬ S(x)))$” realizable. That is, we want a realizer for “$¬¬S(x) ⇒ S(x)$” to act as a “hint” to let us decide whether the $x$-th Turing machine halts or not. And the neat trick (Yankov's lemma 3) is to simply arrange for this “hint” $k$ to be so large (in the case $φ_x(0){\downarrow}$) that we can ascertain $φ_x(0){\downarrow}$ simply by running the machine up to that point; in other words, the smart but counterintuitive thing is that we don't use the realizer $k$ of $¬¬S(x) ⇒ S(x)$ as a program (taking a realizer of $¬¬S(x)$ and returning one of $S(x)$), but simply as a bound on the computation trace of $φ_x(0)$. We will arrange for $k$ to be large enough by bounding a kind of Busy Beaver function for all $t≤y$.

Now for the actual proof: Let $S(x)$ be the formula (of Heyting arithmetic) which says informally:

The $x$-th Turing machine halts ($φ_x(0){\downarrow}$), i.e., it has an execution trace $y$; furthermore, there is a $z$ which is strictly greater than $φ_t(0)$ for any $t≤y$ such that $φ_t(0){\downarrow}$.

or formally:

$$ ∃y.(T(x,0,y) \; ∧ \; ∃z.∀t≤y.∀v.(T(t,0,v)⇒U(v)<z)) $$

Loosely speaking, we are asserting that the $x$-th Turing machine halts and that there is a bound $z$ on some kind of Busy Beaver function of its execution trace $y$.

Classically, $S(x)$ is just equivalent to $φ_x(0){\downarrow}$, since $∃z.∀t≤y.∀v.(T(t,0,v)⇒U(v)<z)$ is provable (note that intuitionistically, merely $¬¬∃z.∀t≤y.∀v.(T(t,0,v)⇒U(v)<z)$ is provable).

So certainly, $∀ x. (¬¬S(x) ∨ ¬ S(x))$ isn't realizable. Also note that if $φ_x(0){\downarrow}$ then any natural number (in particular $0$) realizes $¬¬S(x)$ (because $¬S(x)$ has no realizer).

Now assume we have a realizer $k$ of $¬¬S(x) ⇒ S(x)$. This is a Turing machine which takes a realizer of $¬¬S(x)$ and returns one of $S(x)$. Suppose $φ_x(0){\downarrow}$, say $T(x,0,y)$. Then also $φ_k(0){\downarrow}$ (since $0$ is a realizer of $¬¬S(x)$) and its value is a realizer of $S(x)$. But then, because of the assumption on the encoding of pairs¹, this value $φ_k(0)$ is $≥z$ for some strict upper bound $z$ on $φ_t(0)$ for any $t≤y$ such that $φ_t(0){\downarrow}$. So $φ_k(0)$ itself is such a bound: therefore, $k>y$.

Now we can realize the formula “$∀ x. ((¬¬S(x) ⇒ S(x)) ⇒ (¬¬S(x) ∨ ¬ S(x)))$” as follows: given $x$, and given $k$ realizing $¬¬S(x) ⇒ S(x)$, the previous paragraph shows that if $φ_x(0){\downarrow}$ then $k$ is greater than $y$ such that $T(x,0,y)$, so we test for all $y<k$ whether $T(x,0,y)$: this lets us decide whether $φ_x(0){\downarrow}$ or not, and we return the case $¬¬S(x)$ or the case $¬S(x)$ (along with a trivial realizer) according to what we found. Since $∀ x. ((¬¬S(x) ⇒ S(x)) ⇒ (¬¬S(x) ∨ ¬ S(x)))$ is intuitionistically equivalent to $∀ x. ((¬¬S(x) ⇒ S(x)) ⇒ (S(x) ∨ ¬ S(x)))$, we have also realized the latter.

Having given an $S(x)$ such that $∀ x. ((¬¬S(x) ⇒ S(x)) ⇒ (S(x) ∨ ¬ S(x)))$ is realizable but not $∀ x. (¬¬S(x) ∨ ¬ S(x))$, we can state that Scott's axiom $((¬¬a⇒a)⇒(¬a∨¬¬a))⇒(¬a∨¬¬a)$ isn't realizable (even in the weak sense that substituting any arithmetical formula for $a$ and taking the universal closure would be realizable). ∎

1. What we use is that if $k$ realizes $∃u.(\cdots)$ then $k≥u$ for a $u$ witnessing this (since $k$ will be a pair $⟨u,\cdots⟩$).

Remark: I replaced Yankov's $g(y)=x$ by $T(x,0,y)$ in the above, as this seemed more economical, but pædagogically this is perhaps not the best choice, as $T$ actually plays two different roles in the proof as I wrote it. So, in case this makes things clearer: the $T(x,0,y)$ and the $T(t,0,v)$ are really unrelated: we could replace the former by $g(y)=x$ where $g$ is some primitive recursive function whose range is undecidable.