Skip to main content
MathOverflow

Return to Question

add a short version of the question at start
Source Link
Gro-Tsen
Gro-Tsen
  • 32.4k
  • 5
  • 86
  • 372

Short version: Various things are known about realizability of propositional formulas for Kleene's “first algebra” (i.e., $\mathbb{N}$), like examples of realizable but unprovable formulas, and some that aren't realizable. Is anything similar known for Kleene's “second algebra” (i.e., $\mathbb{N}^{\mathbb{N}}$), perhaps looking for a computable realizer?

(Long version, with all appropriate definitions and examples, follows.)

Setup: Let $\mathcal{A}$ be a(n untyped!) partial combinatory algebra (PCA) whose (partial) operation will be denoted ‘$\bullet$’: the case where $\mathcal{A}$ is Kleene's second algebra $\mathcal{K} _ 2$ (defined here) interests me most for this question; the case of Kleene's first algebra $\mathcal{K} _ 1$ (namely $\mathbb{N}$ with the $e\bullet n$ being as the value of the $e$-th general recursive function at $n$, if it is defined) will be important for comparison. More generally, rather than a single PCA, one might consider the “relative” case described by a pair $(\mathcal{A},\mathcal{A} _\#)$ where $\mathcal{A} _\#$ is a sub-PCA of $\mathcal{A}$, the important case here being that of $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ where $\mathcal{K} _ 2^{\mathrm{eff}}$ is the sub-PCA of $\mathcal{K} _ 2$ consisting of computable functions $\mathbb{N}\to\mathbb{N}$.

This is equivalent to the internal logic of the realizability (resp. relative realizability) topos defined by $\mathcal{A}$ (resp. $(\mathcal{A},\mathcal{A} _\#)$). (E.g., propositional realizability for $\mathcal{K} _ 1$ is the internal logic of the effective topos, while that for $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ is that of the Kleene-Vesley topos.)

Setup: Let $\mathcal{A}$ be a(n untyped!) partial combinatory algebra (PCA) whose (partial) operation will be denoted ‘$\bullet$’: the case where $\mathcal{A}$ is Kleene's second algebra $\mathcal{K} _ 2$ (defined here) interests me most for this question; the case of Kleene's first algebra $\mathcal{K} _ 1$ (namely $\mathbb{N}$ with the $e\bullet n$ being as the value of the $e$-th general recursive function at $n$, if it is defined) will be important for comparison. More generally, rather than a single PCA, one might consider the “relative” case described by a pair $(\mathcal{A},\mathcal{A} _\#)$ where $\mathcal{A} _\#$ is a sub-PCA of $\mathcal{A}$, the important case here being that of $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ where $\mathcal{K} _ 2^{\mathrm{eff}}$ is the sub-PCA of $\mathcal{K} _ 2$ consisting of computable functions $\mathbb{N}\to\mathbb{N}$.

This is equivalent to the internal logic of the realizability (resp. relative realizability) topos defined by $\mathcal{A}$ (resp. $(\mathcal{A},\mathcal{A} _\#)$).

Short version: Various things are known about realizability of propositional formulas for Kleene's “first algebra” (i.e., $\mathbb{N}$), like examples of realizable but unprovable formulas, and some that aren't realizable. Is anything similar known for Kleene's “second algebra” (i.e., $\mathbb{N}^{\mathbb{N}}$), perhaps looking for a computable realizer?

(Long version, with all appropriate definitions and examples, follows.)

Setup: Let $\mathcal{A}$ be a(n untyped!) partial combinatory algebra (PCA) whose (partial) operation will be denoted ‘$\bullet$’: the case where $\mathcal{A}$ is Kleene's second algebra $\mathcal{K} _ 2$ (defined here) interests me most for this question; the case of Kleene's first algebra $\mathcal{K} _ 1$ (namely $\mathbb{N}$ with the $e\bullet n$ being as the value of the $e$-th general recursive function at $n$, if it is defined) will be important for comparison. More generally, rather than a single PCA, one might consider the “relative” case described by a pair $(\mathcal{A},\mathcal{A} _\#)$ where $\mathcal{A} _\#$ is a sub-PCA of $\mathcal{A}$, the important case here being that of $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ where $\mathcal{K} _ 2^{\mathrm{eff}}$ is the sub-PCA of $\mathcal{K} _ 2$ consisting of computable functions $\mathbb{N}\to\mathbb{N}$.

This is equivalent to the internal logic of the realizability (resp. relative realizability) topos defined by $\mathcal{A}$ (resp. $(\mathcal{A},\mathcal{A} _\#)$). (E.g., propositional realizability for $\mathcal{K} _ 1$ is the internal logic of the effective topos, while that for $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ is that of the Kleene-Vesley topos.)

Source Link
Gro-Tsen
Gro-Tsen
  • 32.4k
  • 5
  • 86
  • 372

What is known about propositional realizability for the second Kleene algebra and related PCAs?

Setup: Let $\mathcal{A}$ be a(n untyped!) partial combinatory algebra (PCA) whose (partial) operation will be denoted ‘$\bullet$’: the case where $\mathcal{A}$ is Kleene's second algebra $\mathcal{K} _ 2$ (defined here) interests me most for this question; the case of Kleene's first algebra $\mathcal{K} _ 1$ (namely $\mathbb{N}$ with the $e\bullet n$ being as the value of the $e$-th general recursive function at $n$, if it is defined) will be important for comparison. More generally, rather than a single PCA, one might consider the “relative” case described by a pair $(\mathcal{A},\mathcal{A} _\#)$ where $\mathcal{A} _\#$ is a sub-PCA of $\mathcal{A}$, the important case here being that of $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ where $\mathcal{K} _ 2^{\mathrm{eff}}$ is the sub-PCA of $\mathcal{K} _ 2$ consisting of computable functions $\mathbb{N}\to\mathbb{N}$.

The following definition is supposed to be fairly standard, but let me recall it because it's not so easy to find as there are slight variations in what a propositional formula being “realizable” means (see “Note” below). Experts should probably skip this part.

Definition: If $\varphi(X_1,\ldots,X_n)$ is a propositional formula in $n$ variables, and $P_1,\ldots,P_n \subseteq \mathcal{A}$, we define a subset $\dot\varphi(P_1,\ldots,P_n)$ of $\mathcal{A}$ by induction (i.e., by dotting all connectors) from $$ \newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}} \newcommand{\dottedland}{\mathbin{\dot\land}} \newcommand{\dottedlor}{\mathbin{\dot\lor}} \newcommand{\dottedtop}{\mathord{\dot\top}} \newcommand{\dottedbot}{\mathord{\dot\bot}} \newcommand{\dottedneg}{\mathop{\dot\neg}} \begin{aligned} P\dottedland Q &:= \{\langle p,q\rangle : p\in P, q\in Q\}\\ P\dottedlor Q &:= \{\langle \overline{0},p\rangle : p\in P\} \cup \{\langle \overline{1},q\rangle : p\in Q\}\\ P\dottedlimp Q &:= \{f\in\mathcal{A} :\; (\forall p\in P)\; (f\bullet p){\downarrow} \in Q\}\\ \dottedtop &:= \mathcal{A}\\ \dottedbot &:= \varnothing\\ \end{aligned} $$ (where $\langle –,–\rangle$ is a standard coding of pairs in $\mathcal{A}$, and $\overline{0},\overline{1}$ are, say, Church numerals). We then say that $\varphi(X_1,\ldots,X_n)$ is “realizable” (or to remove possible ambiguity, uniformly realizable) when $$ \bigcap_{P_1,\ldots,P_n \subseteq \mathcal{A}} \dot\varphi(P_1,\ldots,P_n) $$ is inhabited (i.e., non-empty, since this all takes place in classical logic externally), or, in the relative case described by $(\mathcal{A},\mathcal{A} _\#)$, when it is inhabited by an element of $\mathcal{A} _\#$. (One might also extend the definition to second-order propositional formulas, i.e., formulas in Girard's system F, by adding $$ \begin{aligned} \dot\forall P. \dot\varphi(P) &:= \bigcap_{P\subseteq \mathcal{A}} \dot\varphi(P)\\ \dot\exists P. \dot\varphi(P) &:= \bigcup_{P\subseteq \mathcal{A}} \dot\varphi(P)\\ \end{aligned} $$ — but I prefer to keep the focus on plain propositional formulas.)

This is equivalent to the internal logic of the realizability (resp. relative realizability) topos defined by $\mathcal{A}$ (resp. $(\mathcal{A},\mathcal{A} _\#)$).

In particular, any provable formula of intuitionistic propositional logic is realizable.

Note however, that the definition given above uses arbitrary subsets of $\mathcal{A}$ in various places. In the case of $\mathcal{K} _ 1$, there are variations around the notion of propositional realizability where one might say, e.g., that $\varphi(X_1,\ldots,X_n)$ is realizable when any first-order arithmetic formula obtained by substituting arbitrary formulas (possibly with free variables) for $X_1,\ldots,X_n$ is realizable. As far as I understand, no difference is known between these different notions, and all known propisitional formulas realizable for $\mathcal{K} _ 1$ are, in fact, realizable with the strong “uniform” notion described above.

Context: (Mostly Soviet) mathematicians in the 1960–1970's investigated propositional realizability for $\mathcal{K} _ 1$, finding examples of some formulas that are realizable despite not being intuitionistically provable, and examples of formulas that aren't realizable despite being classically provable. A good survey on such results is Plisko's “A Survey of Propositional Realizability Logic”, Bull. Symbolic Logic 15 (2009) 1–42. Examples of realizable-but-not-provable formulas for $\mathcal{K} _ 1$ include: $$ \begin{aligned} &((\neg\neg D\Rightarrow D)\Rightarrow(\neg D\lor\neg\neg D)) \Rightarrow(\neg D\lor\neg\neg D)\\ \text{where}\quad &D := \neg X_1 \lor \neg X_2 \end{aligned} \tag{*} $$ (the first one discovered, and due to G. F. Rose) or $$ \begin{aligned} &\big(\neg (X_1 \land X_2) \land (\neg X_1 \Rightarrow (Y_1 \lor Y_2)) \land (\neg X_2 \Rightarrow (Y_1 \lor Y_2))\big)\\ \mathrel{\Rightarrow} &\big((\neg X_1 \Rightarrow Y_1)\lor(\neg X_2 \Rightarrow Y_1)\lor(\neg X_1 \Rightarrow Y_2)\lor(\neg X_2 \Rightarrow Y_2)\big)\\ \end{aligned} \tag{**} $$ (which is due to G. S. Ceitin and discussed here). Examples of interesting non realizable formulas for $\mathcal{K} _ 1$ include: $$ (\neg X \Rightarrow (Y_1\lor Y_2)) \Rightarrow (\neg X\Rightarrow Y_1)\lor (\neg X\Rightarrow Y_2) \tag{†} $$ (the “Kreisel-Putnam” axiom, whose non-realizability is easy given two computably inseparable sets) or $$ ((\neg\neg X\Rightarrow X)\Rightarrow(\neg X\lor\neg\neg X)) \Rightarrow(\neg X\lor\neg\neg X) \tag{‡} $$ (the “Scott axiom”, for the non-realizability of which see here).

I should also note that it is (as far as I know) an open question whether the set of realizable formulas for $\mathcal{K} _ 1$ is recursively enumerable, and it is also open whether it is co-recursively enumerable.

QUESTION: Are any results analogous to the above-mentioned ones known for other specific PCAs such as Kleene's second algebra $\mathcal{K} _ 2$, of in relative cases such as $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$? Or perhaps for general classes of PCAs (including formulas realizable for “all” PCAs or those realizable for “some” PCA)?

Comments: I am making my question very open because since already the case of $\mathcal{K} _ 1$ seems confined to a handful of papers in Russian (some of which haven't ever been translated) I suspect there's even less in the literature about $\mathcal{K} _ 2$ or such, so anything is worth taking; but maybe there's a reason why $\mathcal{K} _ 2$ or $(\mathcal{K} _ 2, \mathcal{K} _ 2^{\mathrm{eff}})$ is actually simpler than $\mathcal{K} _ 1$. Concerning specific formulas such as the examples above, the proof that (*) and (**) are realizable for $\mathcal{K} _ 1$ doesn't seem to work for $\mathcal{K} _ 2$, but this doesn't mean they're not realizable and I've been unable to settle this either way; if I'm not mistaken, (†) isn't realizable over any PCA; hovewever, the proof that (‡) isn't realizable seems specific to $\mathcal{K} _ 1$, and, again, I don't see how to handle the question of its realizability over $\mathcal{K} _ 2$.