An Application of the Yankov Characteristic Formulas

Abstract

A detailed exposition of one of the author’s old results concerning the relationship between the propositional logic of realizability and the logic of Medvedev is given. The characteristic formulas introduced by Yankov play a decisive role in the proof. Along the way, a brief overview of Yankov’s contribution to the study of propositional logic of realizability is given.

1 Introduction

It is a great honor and pleasure for me to publish an article in a volume dedicated to V. A. Yankov. I don’t know him personally, but his work in the field of mathematical logic has had a strong influence on my research. As a student, I carefully studied his articles. We can say that Vadim Anatolyevich was my correspondence teacher.

V.A.Yankov’s works are devoted to non-classical logics. In this article we consider his contribution to the study of the propositional logic of realizability and one application of his ideas to the study of the relationship between the propositional logic of realizability and Medvedev’s logic of finite problems.

2 Intuitionistic Propositional Logic

From the intuitionistic point of view, a proposition is true if it is proved. Thus the truth of a proposition is connected with its proof. In order to avoid any confusion with formal proofs, we shall use the term ‘a verification’  instead of ‘a proof’. This understanding of the meaning of propositions leads to an original interpretation of logical connectives and quantifiers stated by L. E. J. Brouwer, A. N. Kolmogorov, and A. Heyting. Namely for every true proposition A we can consider its verification as a text justifying A. Now, if A and B are propositions, then

• a verification of a conjunction $A\, \& \,B$ is a text containing a verification of A and a verification of B;

• a verification of a disjunction $A\vee B$ is a text containing a verification of A or a verification of B and indicating which of them is verified;

• a verification of an implication $A\rightarrow B$ is a text describing a general effective operation for obtaining a verification of B from every verification of A;

• a verification of a negative proposition $\lnot A$ is a verification of the proposition $A\rightarrow \bot$, where $\bot$ is a proposition having no verification.

If A(x) is a predicate with a parameter x over a domain M given in an appropriate way, then

• a verification of an universal proposition $\forall x\,A(x)$ is a text describing a general effective operation which allows to obtain a verification of A(m) for every given $m\in M$;

• a verification of an existential proposition $\exists x\,A(x)$ is a text indicating a concrete $m\in M$ and containing a verification of the proposition A(m).

Of course, this semantics is very informal and is not precise from the mathematical point of view. Nevertheless it is enough for formulating intuitionistically valid logical principles. We shall consider the principles of intuitionistic propositional logic, i.e., those expressible by propositional formulas.

Propositional formulas are constructed in the usual way from a countable set of propositional variables $p,q,r,\dots$ (possibly with subscripts) and connectives &, $\vee ,\rightarrow ,\lnot$. $A(p_1,\ldots ,p_n)$ will denote a propositional formula containing no variables other than $p_1,\ldots ,p_n$. The formula $(A\rightarrow B)\,$ & $\,(B\rightarrow A)$ will be denoted as $A\equiv B$.

A propositional formula $A(p_1,\ldots ,p_n)$ is called intuitionistically valid if every proposition of the form $A(A_1,\ldots ,A_n)$, where $A_1,\ldots ,A_n$ are arbitrary propositions, is intuitionistically true. Thus intuitionistically valid formulas can be considered as principles of intuitionistic propositional logic. The first axiomatization of intuitionistic propositional logic was proposed by A. N. Kolmogorov (1925). Another more wide axiom system of intuitionistic propositional calculus IPC was later proposed by A. Heyting (1930). If $A_1,\dots ,A_n$ are propositional formulas, let $\textsf{IPC}+A_1+\dots +A_n$ be the calculus obtained by adding the formulas $A_1,\dots ,A_n$ as axiom schemes to IPC. Formulas A and B are deductively equivalent if $\textsf{IPC}+A\vdash B$ and $\textsf{IPC}+B\vdash A$.

The problem of completeness of the calculus IPC can not be stated in a precise mathematical form because intuitionistic semantics is very informal. It can be made more precise if we define in a mathematical mode two key notions used in the above description of the informal semantics, namely the notions of a verification and a general effective operation. We consider some interpretations of intuitionistic propositional logic.

3 Heyting Algebras and Yankov’s Characteristic Formulas

We start with an abstract algebraic interpretation. A logical matrix $\mathfrak {M}$ is a non-empty set M with a distinguished element 1 equipped with an unary operation $\lnot$ and binary operations &, $\vee$, and $\rightarrow$ such that for any elements $x,y\in M$ the following conditions hold:

• if $1\rightarrow x=1$, then $x=1$;

• if $x\rightarrow y=y\rightarrow x=1$, then $x=y$.

A valuation on $\mathfrak {M}$ is a function f assigning to each propositional variable p some element $f(p)\in M$. Any valuation is extended to all propositional formulas in a natural way. We say that a formula A is valid in $\mathfrak {M}$ and write $\mathfrak {M}\models A$ if $f(A)=1$ for each valuation f on $\mathfrak {M}$. If $f(A)\not =1$, we say that f refutes A on $\mathfrak {M}$. A formula A is refutable on a logical matrix $\mathfrak {M}$ iff there is a valuation refuting A on $\mathfrak {M}$.

A logical matrix $\mathfrak {M}$ is called a model of a propositional calculus if all the formulas deducible in the calculus are valid in $\mathfrak {M}$. Models of IPC are called Heyting algebras or pseudo-Boolean algebras. If $\mathfrak {M}$ is a Heyting algebra, then one can define a partial order $\le$ on $\mathfrak {M}$ in the following way: if $a,b\in \mathfrak {M}$, then $a\le b$ iff $a\rightarrow b=1$. A detailed exposition of pseudo-Boolean algebras can be found in the book Rasiowa and Sikorski (1963). By Completeness Theorem (see e.g. Jaśkowski 1936), if a propositional formula A is not deducible in $\textsf{IPC}$, then there exists a finite Heyting algebra $\mathfrak M$ such that A is not valid in $\mathfrak M$.

Consider some notions introduced by V. A. Yankov (1963b). A finite logical matrix $\mathfrak M$ is called a finite implicative structure iff $\mathfrak M$ is a model of the calculus IPC. Thus, by Completeness Theorem, finite implicative structures are exactly the finite Heyting algebras. We reformulate other Yankov’s definitions replacing the term ‘a finite implicative structure’ by ‘a finite Heyting algebra’.

There are two important ways of constructing Heyting algebras. Cartesian product of algebras $\mathfrak {M}_1,\dots ,\mathfrak {M}_n$ is a Heyting algebra defined as the set $M_1\times \dots \times M_n$ equipped with the component-wise operations. Another operation $\Gamma$ for any Heyting algebra $\mathfrak {M}$ gives an algebra $\Gamma (\mathfrak {M})$ obtained by adding to $\mathfrak {M}$ a new element $\omega$ with the property: $x\le \omega$ for each $x\not =1$ in $\mathfrak M$ and $\omega \le 1$.

A finite Heyting algebra $\mathfrak {M}$ is called Gödelean iff for any its elements a, b, whenever $a\vee b=1$, we have either $a=1$ or $b=1$. If a finite Heyting algebra $\mathfrak {M}$ contains more than one element, then it is easy to prove that $\mathfrak {M}$ is Gödelean iff there is an element $\omega$ which is the greatest among the elements different from 1. This element is called a Gödelean element of the algebra $\mathfrak {M}$. Note that in Completeness Theorem, one can do only with finite Gödelean algebras. Moreover, every algebra of the form $\Gamma (\mathfrak M)$ is Gödelean.

Let $\mathfrak {M}$ be a finite Gödelean algebra, $\omega$ be its Gödelean element. To each element $a\in \mathfrak {M}$ assign in a one-to-one way a propositional variable $p_a$. Let K be the conjunction of all the formulas $p_{a\circ b}\equiv p_a\circ p_b$ ($\circ \in \{$ &,$\vee ,\rightarrow \}$) and $p_{\lnot a}\equiv \lnot p_a$ for $a,b\in \mathfrak {M}$. Thus the formula K simulates the tables defining the operations & , $\vee$, $\rightarrow$, and $\lnot$. The formula $K\rightarrow p_\omega$ is called a characteristic formula for $\mathfrak {M}$ and is denoted by $X_\mathfrak {M}$. It is obvious that the evaluation $f(p_a)=a$ refutes $X_\mathfrak {M}$ on $\mathfrak {M}$. Yankov has proved the following theorem (see Jankov 1963b, Theorem 2).

Theorem 8.1

For any finite Gödelean algebra $\mathfrak {M}$ and any propositional formula A, the following conditions are equivalent:

(1) $\textsf{IPC}+A\vdash X_\mathfrak {M}$;

(2) $\mathfrak {M}\not \models A$.

A property S of propositional formulas is called intuitionistic if the fact that a formula A has the property S implies that every formula deducible in the calculus $\textsf{IPC}+A$ has this property too. The following theorem (Jankov 1963b, Theorem 3) is a consequence of Theorem 8.1.

Theorem 8.2

For any finite Gödelean algebra $\mathfrak {M}$ and any intuitionistic property S, the following conditions are equivalent:

(1) each formula having the property S is valid in $\mathfrak {M}$;

(2) the formula $X_\mathfrak {M}$ does not have the property S.

This theorem is important in studying various semantics for intuitionistic propositional logic. Let an interpretation (a semantics) of propositional formulas be given. Suppose that $\textsf{IPC}$ is sound with respect to this semantics and we are interested in completeness of $\textsf{IPC}$. If there exists a formula A valid in this semantics and nondeducible in $\textsf{IPC}$, then A is refuted on a finite Gödelean algebra $\mathfrak {M}$. In this case, the formula $X_\mathfrak {M}$ is also valid and nondeducible. Thus we can look for an example of this kind among the characteristic formulas.

We say that elements $a_1,\ldots ,a_n$ of a finite Gödelean algebra $\mathfrak {M}$ form a base if every element in $\mathfrak {M}$ can be obtained from $a_1,\ldots ,a_n$ by means of $\lnot$, & , $\vee$, and $\rightarrow$. The following theorem proved by Yankov (see Jankov 1963b, Theorem 4) is useful for applications.

Theorem 8.3

If a finite Gödelean algebra $\mathfrak {M}$ has a base consisting of k elements, then there is a formula A with k propositional variables such that A and $X_\mathfrak {M}$ are deductively equivalent.

4 Medvedev Logic

Heyting algebras give a rather formal characterization of intuitionistic propositional logic. An interesting although informal interpretation of that logic was proposed by Kolmogorov (1932). He considers propositional formulas as schemes of problems. Let A and B be arbitrary problems. Then $A\,$ & $\,B$ is the problem ‘To solve the problems A and B’, $A\vee B$ is the problem ‘To solve the problem A or to solve the problem B’, $A\rightarrow B$ is the problem ‘To reduce the problem B to the problem A’, i.e., ‘To solve the problem B assuming that a solution of the problem A is given’, the problem $\lnot A$ is the problem $A\rightarrow \bot$, where $\bot$ is a problem having no solution. A propositional formula $A(p_1,\dots ,p_n)$ is considered as a principle of the logic of problems if there exists a uniform solution for all the problems of the form $A(A_1,\dots ,A_n)$, where $A_1,\dots ,A_n$ are arbitrary problems. Kolmogorov shows that the calculus IPC is sound with respect to this interpretation: all the formulas deducible in IPC are principles of the logic of problems.

In order to state the problem of completeness of IPC relative to the interpretation by means of problems, we have to make the notion of a problem more precise from the mathematical point of view. This was done by Yu. T. Medvedev (1962). A finite problem is a pair $\langle F,X\rangle$, where F is a finite non-empty set, X is its subset (possibly empty). Intuitively, F is the set of possible solutions of the problem, X is the set of its actual solutions. Let $\bot$ be a fixed problem without any actual solutions, for example, $\bot =\langle \{0\},\emptyset \rangle$. For a finite problem $\mathfrak {A}=\langle F,X\rangle$ we denote F by $\varphi (\mathfrak {A})$ and X by $\chi (\mathfrak {A})$. Logical operations on finite problems are defined in the following way:

$$ \varphi (\mathfrak {A}\, \& \,\mathfrak {B})=\varphi (\mathfrak {A})\times \varphi (\mathfrak {B}),\, \chi (\mathfrak {A}\, \& \,\mathfrak {B})=\chi (\mathfrak {A})\times \chi (\mathfrak {B}),$$

where $X\times Y$ means Cartesian product;

$$\varphi (\mathfrak {A}\vee \mathfrak {B})=\varphi (\mathfrak {A})\oplus \varphi (\mathfrak {B}),\, \chi (\mathfrak {A}\vee \mathfrak {B})=\chi (\mathfrak {A})\oplus \chi (\mathfrak {B}),$$

where $X\oplus Y=(X\times \{0\})\cup (Y\times \{1\})$;

$$\varphi (\mathfrak {A}\rightarrow \mathfrak {B})=\varphi (\mathfrak {B})^{\varphi (\mathfrak {A})},\, \chi (\mathfrak {A}\rightarrow \mathfrak {B})= \{f\in \varphi (\mathfrak {B})^{\varphi (\mathfrak {A})}\mid f(\chi (\mathfrak {A}))\subseteq \chi (\mathfrak {B})\},$$

where $Y^X$ means the set of maps $f:X\rightarrow Y$;

$$\lnot \mathfrak {A}=\mathfrak {A}\rightarrow \bot .$$

Let $A(p_1,\dots ,p_n)$ be a propositional formula, $\mathfrak {A}_1,\dots ,\mathfrak {A}_n$ be finite problems. Then $A(\mathfrak {A}_1,\dots ,\mathfrak {A}_n)$ is a finite problem obtained by substituting $\mathfrak {A}_1,\dots ,\mathfrak {A}_n$ for $p_1,\dots ,p_n$ in $A(p_1,\dots ,p_n)$.

Let $\mathcal {F}$ be a system of non-empty finite sets $F_1,\dots ,F_n$. We say that a propositional formula $A(p_1,\dots ,p_n)$ is valid over $\mathcal {F}$ if there exists an uniform actual solution for all the problems of the form $A(\mathfrak {A},\dots ,\mathfrak {A}_n)$, where $\mathfrak {A},\dots ,\mathfrak {A}_n$ are finite problems such that $\varphi (\mathfrak {A}_i)=F_i$ ($i=1,\dots ,n$). A propositional formula $A(p_1,\dots ,p_n)$ is called finitely valid if it is valid over every system $F_1,\dots ,F_n$. The set of finitely valid formulas is called Medvedev Logic; we denote it by ML.

Every formula deducible in IPC is finitely valid, but IPC is not complete relative to Medvedev’s interpretation. For example, the formulas

$$\begin{aligned} (\lnot p\rightarrow q\vee r)\rightarrow ((\lnot p\rightarrow q)\vee (\lnot p\rightarrow r)) \end{aligned}$$

(8.1)

and

$$\begin{aligned} ((\lnot \lnot p\rightarrow p)\rightarrow (\lnot p\vee \lnot \lnot p))\rightarrow (\lnot p\vee \lnot \lnot p) \end{aligned}$$

(8.2)

are finitely valid but are not deducible in IPC.

No axiomatization of ML is known, but it is proved that it can not be axiomatized by any system of axiom schemes with bounded number of variables (see Maksimova et al. 1979). In particular, this logic is not finitely axiomatizable.

It was proved Medvedev (1966) that ML has a finite model property: there exists a sequence of finite Heyting algebras $\Phi ^n$ ($n=1,2,\dots$) such that a propositional formula A is in Medvedev Logic iff $\forall n\,[\Phi ^n\models A]$. The sequence $\Phi ^n$ is defined as follows. Let $I_n=\{1,2,\ldots ,n\}$ ($n\ge 1$), $\sigma ^n$ be the family of its non-empty subsets, i.e., $\sigma ^n=\{E\mid E\subseteq I_n \text{ and } E\not =\emptyset \}$. For $\sigma \subseteq \sigma ^n$, its closure is defined as the family $\sigma ^*=\{E\in \sigma ^n\mid \exists E_0\,[E_0\in \sigma \text{ and } E_0\subseteq E]\}$. A family $\sigma$ is called closed if $\sigma ^*=\sigma$. In other words, $\sigma$ is closed iff $E\in \sigma$ implies that all supersets of E are in $\sigma$. The operation $^*$ has the following properties: (1) $\emptyset ^*=\emptyset$; (2) $\sigma ^*\supseteq \sigma$; (3) $\sigma ^{**}=\sigma ^*$; (4) $(\sigma _1\cup \sigma _2)^*=\sigma _1^*\cup \sigma _2^*$; (5) if $\sigma _1$ and $\sigma _2$ are closed, then $\sigma _1\cap \sigma _2$ is closed.

Let $\Phi ^n$ be the set of all closed families, i.e., $\Phi ^n=\{\sigma \subseteq \sigma ^n\mid \sigma ^*=\sigma \}.$ Define operations & , $\vee$, $\rightarrow$, and $\lnot$ on $\Phi ^n$ as follows: $\sigma _1\, \& \,\sigma _2=\sigma _1\cup \sigma _2$; $\sigma _1\vee \sigma _2=\sigma _1\cap \sigma _2$; $\sigma _1\rightarrow \sigma _2=(\overline{\sigma _1}\cap \sigma _2)^*$; $\lnot \sigma _1=(\overline{\sigma _1})^*$, where $\overline{\sigma _1}=\sigma ^n\setminus \sigma _1$. The set $\Phi ^n$ with these operations and a partial order $\le$ defined as $a\le b\leftrightharpoons a\supseteq b$, is a Heyting algebra. Its greatest element relative to $\le$ is $\emptyset$ and the least element is $\sigma ^n$.

The following theorem was proved by Medvedev (1966, Theorem 1).

Theorem 8.4

A propositional formula F is finitely valid iff $\Phi ^n\models F$ for any $n\ge 1$.

Note that $\Phi ^n$ is a Gödelean algebra. Namely $\omega _n=\{I_n\}$ is its Gödelean element. Thus for each algebra $\Phi ^n$, we can construct its characteristic formula $X_n$. For example, consider the case $n=3$. We have that $I_3=\{1,2,3\}$ and $\sigma ^3$ consists of the following 7 elements: $a_i=\{i\}$, where $i=1,2,3$, $a_{ij}=\{i,j\}$, where $i,j=1,2,3$, $i\not =j$, and $a_{123}=I_3$. There are 18 closed subfamilies of $\sigma ^3$. Let us find all of them. Evidently, the closed 7-element family $\textbf{a}_0=\sigma ^3$ is the greatest element relative to $\subseteq$ (and the least element relative to $\le$). Removing from it one of the minimal elements $a_1,a_2,a_3$, we obtain the closed 6-element families $\textbf{a}_1=\sigma ^3\setminus \{a_1\}$, $\textbf{a}_2=\sigma ^3\setminus \{a_2\}$, $\textbf{a}_3=\sigma ^3\setminus \{a_3\}$. Note that in this case, $\textbf{a}_0=\textbf{a}_1\cup \textbf{a}_2=\textbf{a}_1\, \& \,\textbf{a}_2$. After removing from $\textbf{a}_0$ a pair of minimal elements, we obtain the following closed 5-element families $\textbf{a}_4=\textbf{a}_1\cap \textbf{a}_2=\textbf{a}_1\vee \textbf{a}_2$, $\textbf{a}_5=\textbf{a}_1\cap \textbf{a}_3=\textbf{a}_1\vee \textbf{a}_3$, $\textbf{a}_6=\textbf{a}_2\cap \textbf{a}_3=\textbf{a}_2\vee \textbf{a}_3$. Further, removing from $\textbf{a}_0$ all the minimal elements $a_1,a_2,a_3$, we obtain the closed 4-element family $\textbf{a}_7=\textbf{a}_1\cap \textbf{a}_2\cap \textbf{a}_3=\textbf{a}_1\vee \textbf{a}_2\vee \textbf{a}_3$. Removing from $\textbf{a}_0$ the element $a_{12}$, in order to obtain a closed family, we must remove also the elements $a_1$ and $a_2$. Thus we obtain the closed 4-element family $\textbf{a}_8=\{a_3,a_{13},a_{23},a_{123}\}$. Note that $\textbf{a}_8=\lnot \textbf{a}_3$. Indeed, $\overline{\textbf{a}_3}$ is the family $\{a_3\}$ and $\textbf{a}_8$ is its closure. In the same manner, we obtain the closed 4-element families $\textbf{a}_9=\lnot \textbf{a}_2$ and $\textbf{a}_{10}=\lnot \textbf{a}_1$. Removing from $\textbf{a}_7$ the minimal element $a_{12}$, we obtain the closed 3-element family $\textbf{a}_{11}=\{a_{13},a_{23},a_{123}\}=\textbf{a}_7\cap \textbf{a}_8=\textbf{a}_7\vee \textbf{a}_8$. In the same way, we obtain the closed 3-element families $\textbf{a}_{12}=\textbf{a}_7\cap \textbf{a}_9=\textbf{a}_7\vee \textbf{a}_9$, $\textbf{a}_{13}=\textbf{a}_7\cap \textbf{a}_{10}=\textbf{a}_7\vee \textbf{a}_{10}$. Other closed 2-element families are $\textbf{a}_{14}=\textbf{a}_{11}\cap \textbf{a}_{12}=\textbf{a}_{11}\vee \textbf{a}_{12}$, $\textbf{a}_{15}=\textbf{a}_{11}\cap \textbf{a}_{13}=\textbf{a}_{11}\vee \textbf{a}_{13}$, $\textbf{a}_{16}=\textbf{a}_{12}\cap \textbf{a}_{13}=\textbf{a}_{12}\vee \textbf{a}_{13}$. Finally, we have the Gödelean element of the algebra $\Phi ^3$, namely $\textbf{a}_{17}=\{I_3\}=\textbf{a}_8\cap \textbf{a}_9\cap \textbf{a}_{10}=\textbf{a}_8\vee \textbf{a}_9\vee \textbf{a}_{10}$, and the greatest relative to $\le$ element $\textbf{a}_{18}=\emptyset =\lnot \textbf{a}_0$. A visual diagram of the algebra $\Phi ^3$ is provided in [Citkin 1978, Fig. 2].

We see that the elements $\textbf{a}_1$, $\textbf{a}_2$, $\textbf{a}_3$ form a base for the algebra $\Phi ^3$. By Yankov’s Theorem 8.3, there is a propositional formula L with three variables such that L is deductively equivalent to the characteristic formula $X_3$. In order to obtain a formula L, we assign the variables $p_1,p_2,p_3$ to the elements $\textbf{a}_1,\textbf{a}_2,\textbf{a}_3$ and simulate the tables defining the operations of the algebra $\Phi ^3$ by propositional formulas bearing in mind that all the elements are obtained from the basic ones by means of $\lnot , \& ,\vee ,\rightarrow$. It turned out that the elements $\textbf{a}_8,\textbf{a}_9,\textbf{a}_{10}$, i.e., $\lnot \textbf{a}_1, \lnot \textbf{a}_2,\lnot \textbf{a}_3$, form a base as well. For example, the Gödelean element $\textbf{a}_{17}$ can be presented as $\lnot \textbf{a}_1\vee \lnot \textbf{a}_2\vee \lnot \textbf{a}_3$. Thus we can construct the formula L from $\lnot p_1,\lnot p_2,\lnot p_3$. A general method of constructing such a formula is described in Jankov (1969). In our case, we obtain the following formula:

$$ \begin{aligned} \begin{array}{l} (\lnot \lnot p_1\equiv (\lnot p_2\, \& \lnot p_3))\, \& \,\,(\lnot \lnot p_2\equiv (\lnot p_3\, \& \lnot p_1))\, \& \, (\lnot \lnot p_3\equiv (\lnot p_1\, \& \lnot p_2))\, \& \\ \& \,((\lnot p_1\rightarrow (\lnot p_1\vee \lnot p_3))\rightarrow (\lnot p_2\vee \lnot p_3))\, \& \\ \& \,((\lnot p_2\rightarrow (\lnot p_3\vee \lnot p_1))\rightarrow (\lnot p_3\vee \lnot p_1))\, \& \\ \& \,((\lnot p_3\rightarrow (\lnot p_1\vee \lnot p_2))\rightarrow (\lnot p_1\vee \lnot p_2)) \rightarrow (\lnot p_1\vee \lnot p_2\vee \lnot p_3). \end{array} \end{aligned}$$

(8.3)

5 Propositional Logic of Realizability

Another way of a specification of the informal intuitionistic semantics is to define a mathematically precise notion of a general effective operation. There is such a notion in mathematics, namely the notion of an algorithm. A variant of intuitionistic semantics based on interpreting effective operations as algorithms was proposed by S. C. Kleene. He introduced (see Kleene 1945) the notion of recursive realizability for the sentences of first-order arithmetic. The main idea was to consider natural numbers as the codes of verifications and partial recursive functions as effective operations. Partial recursive functions are coded by their Gödel numbers. A code of a verification of a sentence is called a realization of the sentence.

The unary partial recursive function with the Gödel number x will be denoted by $\{x\}$. The relation ‘a natural number e realizes an arithmetic sentence A’  ($e\,\textsf{r}\,A$) is defined by induction on the number of logical connectives and quantifiers in A.

• If A is an atomic sentence $t_1=t_2$, then $e\,\textsf{r}\,A$ means that $e=0$ and A is true.

• $e\,\textsf{r}\,(A\, \& \,B)$ iff e is of the form $2^a\cdot 3^b$ and $a\,\textsf{r}\,A$, $b\,\textsf{r}\,B$.

• $e\,\textsf{r}\,(A\vee B)$ means that either e is of the form $2^0\cdot 3^a$ and $a\,\textsf{r}\,A$ or e is of the form $2^1\cdot 3^b$ and $b\,\textsf{r}\,B$.

• $e\,\textsf{r}\,(A\rightarrow B)$ means that for any a, if $a\,\textsf{r}\,A$, then $\{e\}(a)\,\textsf{r}\,B$.

• $e\,\textsf{r}\,\lnot A$ means that $e\,\textsf{r}\,(A\rightarrow 0=1)$.

• $e\,\textsf{r}\,\forall x\,A(x)$ means that for any n, $\{e\}(n)\,\textsf{r}\,A(n)$.

• $e\,\textsf{r}\,\exists x\,A(x)$ means that e is of the form $2^n\cdot 3^a$ and $a\,\textsf{r}\,A(n)$.

The following theorem is proved by D. Nelson (1947).

Theorem 8.5

Every formula deducible in intuitionistic arithmetic $\textsf{HA}$ is realizable.

There are various variants of the notion of realizability for propositional formulas. Let $A(p_1,\ldots ,p_n)$ be a propositional formula, $A_1,\ldots ,A_n$ be arithmetical sentences. Then $A(A_1,\ldots ,A_n)$ is an arithmetical sentence obtained by substituting $A_1,\ldots ,A_n$ for $p_1,\ldots ,p_n$ in $A(p_1,\ldots ,p_n)$. It follows from the proof of Nelson Theorem that for any propositional formula A deducible in IPC, there exists a number a such that $a\,\textsf{r}\,A(A_1,\ldots ,A_n)$ for any arithmetical sentences $A_1,\ldots ,A_n$. In this sense, deducible formulas are uniformly realizable.

The incompleteness of IPC with respect to recursive realizability was discovered by G. F. Rose (1953), who has found a propositional formula which is uniformly realizable but is not deducible in IPC. Later other examples of this kind were proposed by various authors. Deductive interrelations between them are completely studied by D. P.  Skvortsov (1995). He found a list of four realizable propositional formulas which are deductively independent in IPC and any other known realizable formula is deducible from these four formulas.

Yankov made some contributions to the study of propositional realizability logic. His paper Jankov (1963a) is dedicated to this topic. In particular, Yankov proposed new examples of realizable propositional formulas which are not deducible in IPC. These formulas are:

(1) $(\lnot (p\, \& \,q)\, \& \,\lnot (\lnot p\, \& \,\lnot q)\,$ &$\,((\lnot \lnot p\rightarrow p)\rightarrow (p\vee \lnot p))\,$ &

& $\,((\lnot \lnot q\rightarrow q)\rightarrow (q\vee \lnot q)))\rightarrow (\lnot p\vee \lnot q)$;

(2) a series of formulas $I_n$ ($n\ge 3$), where $I_n$ is the formula

&$_{1\le i<j\le n}\lnot (p_i\, \& \,p_j)\,$ &   & $_{1\le i<n}$ (( &$_{1\le j<n,j\not = i}\lnot p_j)\rightarrow (p_i\vee p_n))\rightarrow (p_n\vee \lnot p_n);$

(3) a series of formulas $K_n$ ($n\ge 3$), where $K_n$ is the formula

&$_{1\le i<j\le n}(\lnot (p_i\, \& \,p_j)$  & (( &$_{1\le k\le n.k\not =i,k\not =j}\lnot p_k)\rightarrow (p_i\vee p_j))\rightarrow$ $\vee$ $_{1\le i\le n}p_i.$

Note that the first formula is included in Skvortsov’s list.

Yankov shows deductive relationships between his formulas and the Rose formula. Besides, he considers the 7-element Heyting algebra $\mathfrak M=\Gamma (\Gamma (I_0)\times I_0)$, where $I_0$ is the classical two-element algebra $\{0,1\}$. Yankov proves that all realizable propositional formulas are valid in $\mathfrak M$. In this case, simulating the algebra $\mathfrak M$ in the language of arithmetic is used. Namely, an arithmetical formula $F_a(x)$ is assigned to every element $a\in \mathfrak M$ in such a way that operations in $\mathfrak M$ correspond to the logical operations over formulas in the realizability semantics. For example, if $a\rightarrow b=c$ in $\mathfrak M$, then the formula $\forall x\,((F_a(x)\rightarrow F_b(x))\equiv F_c(x))$ is realizable. At the same time, the formula $\forall x\,F_a(x)$ is realizable only in the case $a=1$. This method was later used by the author in the proof of the completeness of the disjunction-free part of $\textsf{IPC}$ relative to realizability (see Plisko 1973).

It turns out that the formula (8.2) is refuted on the algebra $\mathfrak M$. In fact, this formula is deductively equivalent to the characteristic formula of the algebra $\mathfrak M$. Since realizability is an intuitionistic property of propositional formulas, it follows from Yankov’s Theorem 8.2 that the formula (8.2) is not realizable. This formula is of interest because the Rose formula is a substitutional instance of (8.2). Namely, the Rose formula is obtained by substituting $\lnot q\vee \lnot r$ for p in (8.2).

A comprehensive survey of propositional realizability logic can be found in Plisko (2009).

6 Realizability and Medvedev Logic

We consider relations between propositional logic of realizability and Medvedev Logic. First of all, note that there are propositional formulas in Medvedev Logic which are not realizable, for example, the formulas (8.1) and (8.2). Consider the converse inclusion. Imagine that we are looking for a propositional formula F that is realizable but is not finitely valid. We know that such a formula should be refuted on the algebra $\Phi ^n$ for an appropriate n. On the other hand, realizability is an intuitionistic property. Thus by Yankov’s Theorem 8.2, if the formula F is realizable and is refuted on $\Phi ^n$, then the characteristic formula $X_n$ of the algebra $\Phi ^n$ is realizable. Moreover, the formula $X_n$ is not finitely valid. Thus we can consider only the formulas $X_n$. It turned out that $X_3$ is already the formula we are looking for. Of course, any formula which is deductively equivalent to $X_3$ has the desired property. We have constructed above such a formula, namely (8.3). Denote it by $\textbf{L}(p_1,p_2,p_3)$.

Theorem 8.6

The formula $\textbf{L}(p_1,p_2,p_3)$ is uniformly realizable.

Proof

We prove that there exists a natural number e such that for any arithmetical sentences $\text{ A}_1,\text{ A}_2,\text{ A}_3$, e realizes the arithmetical sentence $\textbf{L}(\text{ A}_1,\text{ A}_2,\text{ A}_3)$, i.e., the sentence

$$ \begin{aligned} \begin{array}{l} (\lnot \lnot \text{ A}_1\equiv (\lnot \text{ A}_2\, \& \lnot \text{ A}_3))\, \& \,(\lnot \lnot \text{ A}_2\equiv (\lnot \text{ A}_3\, \& \lnot \text{ A}_1))\, \& \,(\lnot \lnot \text{ A}_3\equiv (\lnot \text{ A}_1\, \& \lnot \text{ A}_2))\, \& \\ \& \,((\lnot \text{ A}_1\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_3))\rightarrow (\lnot \text{ A}_2\vee \lnot \text{ A}_3))\, \& \\ \& \,((\lnot \text{ A}_2\rightarrow (\lnot \text{ A}_3\vee \lnot \text{ A}_1))\rightarrow (\lnot \text{ A}_3\vee \lnot \text{ A}_1))\, \& \\ \& \,((\lnot \text{ A}_3\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2))\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2)) \rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2\vee \lnot \text{ A}_3) \end{array} \end{aligned}$$

(8.4)

Begin with some auxiliary statements. Let $\pi _0,\pi _1,\pi _2,\ldots$ be sequential prime numbers, and $(a)_i$ be the exponent with which the prime number $\pi _i$ appears in the decomposition of the number a into prime factors.

Lemma 8.1

Let f be a total recursive function with values 0 and 1. Then there exists a number x such that either $(\{x\}(x))_0=0$ and $f(x)=1$ or $(\{x\}(x))_0=1$ and $f(x)=0.$

Proof

This is an easy exercise in the theory of recursive functions.

Lemma 8.2

Suppose that the formula

$$ \begin{aligned} (\lnot \lnot \text{ A}_1\equiv (\lnot \text{ A}_2\, \& \lnot \text{ A}_3)) \& (\lnot \lnot \text{ A}_2\equiv (\lnot \text{ A}_3\, \& \lnot \text{ A}_1)) \& (\lnot \lnot \text{ A}_3\equiv (\lnot \text{ A}_1\, \& \lnot \text{ A}_2)) \end{aligned}$$

(8.5)

is realizable and numbers $a_1,a_2,a_3$ are such that

$$a_1\,\textbf{r}\,((\lnot \text{ A}_1\rightarrow (\lnot \text{ A}_2\vee \lnot \text{ A}_3))\rightarrow (\lnot \text{ A}_2\vee \lnot \text{ A}_3)),$$

$$a_2\,\textbf{r}\,((\lnot \text{ A}_2\rightarrow (\lnot \text{ A}_3\vee \lnot \text{ A}_1))\rightarrow (\lnot \text{ A}_3\vee \lnot \text{ A}_1)),$$

$$a_3\,\textbf{r}\,((\lnot \text{ A}_3\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2))\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2)).$$

For any x and $i=1,2,3$, let $f_i(x)=(\{a_i\}(x))_0$ and $\alpha (x)$ be the Gödel number of the constant function $g(y)=2^{(\{x\}(x))_0}\cdot 3^0.$ Then there exist x and $i\in \{1,2,3\}$ such that either $(\{x\}(x))_0=0$ and $f_i(\alpha (x))=1$ or $(\{x\}(x))_0=1$ and $f_i(\alpha (x))=0.$

Proof

It follows from realizability of the formula (8.5) that exactly two of the formulas $\lnot \text{ A}_1,\lnot \text{ A}_2,\lnot \text{ A}_3$ are realizable. As the situation is absolutely symmetric, let us consider the case when $\lnot \text{ A}_1$ and $\lnot \text{ A}_2$ are realizable and $\lnot \text{ A}_3$ is not. Then the formula $\lnot \text{ A}_3\rightarrow (\lnot \text{ A}_1\vee \lnot \text{ A}_2)$ is realized by every number, thus $\{a_3\}$ is a total recursive function. The function $\alpha$ is also total and recursive. Therefore the function $f(x)=f_3(\alpha (x))$ is total, and we obtain the proposition under the proof as an immediate consequence of Lemma 8.1.

Let a realization of the premise of the formula (8.4) be given. It follows that the formula (8.5) is realizable and numbers $a_1,a_2,a_3$ as in Lemma 8.2 can be found effectively. Then, by Lemma 8.2, there exist x and $i\in \{1,2,3\}$ such that either $(\{x\}(x))_0=0$ and $f_i(\alpha (x))=1$ or $(\{x\}(x))_0=1$ and $f_i(\alpha (x))=0$, where $f_i$ and $\alpha$ are the same functions as in Lemma 8.2. Note that the number x can be found effectively. Now we can describe an algorithm which allows to find a realization of the conclusion of the formula (8.4). Obviously, it is enough to indicate a realizable member in the disjunction $\lnot \text{ A}_1\vee \lnot \text{ A}_2\vee \lnot \text{ A}_3$. We state that:

• if $i=1$ and $f_1(\alpha (x))=0$, then $\lnot \text{ A}_2$ is realizable;

• if $i=1$ and $f_1(\alpha (x))=1$, then $\lnot \text{ A}_3$ is realizable;

• if $i=2$ and $f_2(\alpha (x))=0$, then $\lnot \text{ A}_3$ is realizable;

• if $i=2$ and $f_2(\alpha (x))=1$, then $\lnot \text{ A}_1$ is realizable;

• if $i=3$ and $f_3(\alpha (x))=0$, then $\lnot \text{ A}_1$ is realizable;

• if $i=3$ and $f_3(\alpha (x))=1$, then $\lnot \text{ A}_2$ is realizable.

Consider the first case, namely $f_1(\alpha (x))=0$ for some x such that $(\{x\}(x))_0=1$. Note that $\{x\}(x)$ is defined and $\alpha (x)$ is the Gödel number of the constant function whose only value is $2^{(\{x\}(x))_0}\cdot 3^0$. We have to prove that $\lnot \text{ A}_2$ is realizable. Assume that $\lnot \text{ A}_2$ is not realizable. Then $\lnot \text{ A}_1$ and $\lnot \text{ A}_3$ are realizable. In this case, the number $\alpha (x)$ is a realization of the formula $\lnot \text{ A}_1\rightarrow (\lnot \text{ A}_2\vee \lnot \text{ A}_3)$. Indeed, every number a realizes $\lnot \text{ A}_1$. Note that $\{\alpha (x)\}(a)=2^{(\{x\}(x))_0}\cdot 3^0=2^1\cdot 3^0$ and in fact, this number realizes the formula $\lnot \text{ A}_2\vee \lnot \text{ A}_3$. Therefore $\{a_1\}(\alpha (x))$ realizes the formula $\lnot \text{ A}_2\vee \lnot \text{ A}_3$ and $(\{a_1\}(\alpha (x))_0=1$, that is $f_1(\alpha (x))=0$. But this is not the case. The contradiction means that the formula $\lnot \text{ A}_2$ is realizable. Other cases are considered in the same way.

Thus we have an algorithm for finding a realizable member in the disjunction $\lnot \text{ A}_1\vee \lnot \text{ A}_2\vee \lnot \text{ A}_3$ if a realization of the premise of the formula (8.4) is given. This means that the formula (8.4) is realizable. As the realization does not depend on the sentences $\text{ A}_1,\text{ A}_2,\text{ A}_3$, the formula $\textbf{L}$ is uniformly realizable.