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](https://en.wikipedia.org/wiki/Kleene%27s_T_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.