6
$\begingroup$

In Realizability: A Historical Essay [Jaap van Oosten, 2002], it is said that recursive realizability and HA provability do not concur, because although every HA provable closed formula is realizable, not every realizable closed formula is HA provable. Van Oosten points out that Propositional calculus and realizability [G.F. Rose] first proved this, but his example is a bit unwieldy and the old syntax a bit terse. Van Oosten also notes, in a footnote, the following simple formula due to G.S. Tseitin, which would be realizable but not HA provable:

$$ \big[\neg (A \land B) \land (\neg A \to (C \lor D)) \land (\neg B \to (C \lor D))\big] \to \big[(\neg A \to C)\lor(\neg B \to C)\lor(\neg A \to D)\lor(\neg B \to D)\big] $$

I get how this formula is not HA provable, because it's essentially just De Morgan. But I don't see how this would be recursive realizable? Somehow De Morgen is intertwined twice, but I don't see how this would cleverly sitestep the otherwise unrealizable $\neg (A\land B) \to (\neg A \lor \neg B)$.

Improve this question
$\endgroup$
2

1 Answer 1

Reset to default
4
$\begingroup$

Let us first have a look at the core obstace for $$\neg (A \wedge B) \rightarrow (\neg A \vee \neg B)$$ Negated formulas do not have computational content, so $\neg (A \wedge B)$ is only a promise that either $A$ or $B$ is false, but does not provide any useful information. But we need to explicit compute a bit telling us whether $\neg A$ or $\neg B$ is going to be realized, and we have no input to compute this from.

Now in the given formula, we have three premises: As before, $\neg (A \wedge B)$ is merely a promise, but contains no information. $\neg A \rightarrow (C \vee D)$ is realized by a Turing machine $M_1$ that if $\neg A$ holds, will terminate, and tell us either that $C$ holds (and provide a realizer), or that $D$ holds (and provide a realizer). Likewise, $\neg B \rightarrow (C \vee D)$ gives a Turing machine $M_2$, working analogously.

The promise that $\neg (A \wedge B)$ guarantees that at least one of $M_1$ and $M_2$ halts. Markov's principle lets us compute the index of one that does. For example, assume that $M_1$ halts and claims that $C$ holds (and gives a claimed realizer of $C$). Classically, this means one of two things: Either $\neg A$ holds, in which case $M_1$ is required to be correct, or $\neg A$ does not hold. In either case, we can now claim that $\neg A \rightarrow C$ (on the righthand side of the big implication), and give the claimed realizer of $C$ as the output here. Any other combination of what machine $M_1$, $M_2$ halts, and what they are claiming then, also gives us one of the cases on the right.

Improve this answer
$\endgroup$
2
  • $\begingroup$ But wait a second. You say "Either $\neg A$ holds, in which case $M_1$ is required to be correct, or $\neg A$ does not hold." But this is not true: if $M_1$ halts and gives $\langle i,p\rangle$ where $i = 1$ and hence $p$ is a claimed realizer of $C$, then we indeed do not know whether $n : \neg A$ or not. If so, $M_1$ is correct, and $p$ is indeed a realizer of $C$. But if not, then we do not know $\neg A$ to be false (i.e. $A$ to hold), we just ruled out a single counterexample. $\endgroup$ Commented Aug 21, 2018 at 11:51
  • 1
    $\begingroup$ @KelleyvanEvert I think the thing that needs to be pointed out to answer your comment is that, for a negative formula like $\neg A$, either all natural numbers realize it (precisely when there is no realizer of $A$), or none do (precisely when there is a realizer of $A$). So if the input $n$ to $M_1$ is not a realizer of $\neg A$, we have not just “ruled out a single counterexample”, we know there is no realizer of $\neg A$. $\endgroup$ Commented Dec 6, 2023 at 14:15

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.