Abstract Generated abstract
The paper studies superconstructive propositional calculi obtained by adding finitely many axioms to Heyting’s intuitionistic calculus, with modus ponens and substitution as rules. Using finite implicative structures, including Jaśkowski structures and related families constructed by cardinal products and ordinal addition, it gives necessary and sufficient semantic conditions for such calculi to coincide with four notable systems: classical logic, the weak law of excluded middle calculus, a calculus determined by axiom M, and their combination. The main results characterize derivability in these calculi by general validity on specified finite or infinite families of implicative structures, and derive equivalence criteria for arbitrary finitely axiomatized superconstructive calculi. The paper also notes that these criteria yield decision procedures in principle, though the resulting algorithms may be cumbersome.
Full Text
V. A. YANKOV
ON SOME SUPERCONSTRUCTIVE PROPOSITIONAL CALCULI
(Presented by Academician P. S. Novikov on 20 III 1963)
1. By a superconstructive propositional calculus (an sk-calculus) we shall mean any calculus that is constructed on the basis of the language of propositional logic in the following way: as the axioms of an sk-calculus one takes all the basic axioms of Heyting’s intuitionistic calculus and some finite set of additional axioms; as the rules of inference of an sk-calculus one takes modus ponens and the substitution rule (see (¹)).
We shall consider in particular the following four sk-calculi ($a$, $b$, $c$, $d$ will henceforth denote pairwise distinct propositional variables): a) the classical calculus $\mathfrak{K}$, in which the formula $K$: $\neg\neg a \supset a$ is taken as the additional axiom; b) the calculus of the weak law of excluded middle $\mathfrak{L}$, in which the formula $L$: $\neg\neg a \vee \neg a$ is taken as the additional axiom; c) the calculus $\mathfrak{M}$, in which the formula $M$: $(\neg\neg a \& (a \supset b) \& ((b \supset a) \supset a)) \supset b$ is taken as the additional axiom; d) the calculus $\mathfrak{N}$, in which there are two additional axioms, namely $L$ and $M$.
Two sk-calculi are called equivalent if every formula derivable in one of these calculi is also derivable in the other.
2. A finite implicative structure is a finite partially ordered set of constructive objects in which there exist least and greatest elements and in which three binary operations can be introduced: conjunction, disjunction, implication, and one unary operation: negation—so that the following conditions are satisfied.
The conjunction of elements $x$, $y$ (symbolically $x \cap y$) is equal to the greatest of those $z$ that are less than or equal to both $x$ and $y$. The disjunction of elements $x$, $y$ (symbolically $x \cup y$) is equal to the least of those $z$ that are greater than or equal to both $x$ and $y$. The implication of elements $x$, $y$ (symbolically $x \to y$) is equal to the greatest of those $z$ such that $x \cap z$ is less than or equal to $y$. The negation of an element $x$ (symbolically $-x$) is equal to the implication from $x$ to the least element (see (², ³)).
We shall need the following two operations, by means of which other implicative structures can be obtained from given implicative structures.
1) Cardinal product. In (²) it is defined for arbitrary partially ordered sets. It can be shown that the cardinal product of implicative structures is an implicative structure. The cardinal product of implicative structures $S_1, \ldots, S_l$ will be denoted by $S_1 \times \cdots \times S_l$, and in the case $S_1 = \cdots = S_l = S$ also by $S^l$.
2) Ordinal addition from above of a one-element structure. In (²) the ordinal sum of arbitrary partially ordered sets is defined. It can be shown that the ordinal sum of two implicative structures is an implicative structure. The result of applying to $S$ the ordinal addition from above of a one-element structure will be denoted by $\Gamma(S)$.
We shall need the following implicative structures.
a) The Jaśkowski structures \(I_k\) \((k=0,1,2,\ldots)\). Here \(I_0\) is a structure of two elements, one of which precedes the other, and
\[ I_{k+1}=\Gamma\left(I_k^{\,k+1}\right)\quad (k=0,1,\ldots). \]
b) The structures \(J_k\) \((k=1,2,\ldots)\). The implicative structure \(J_k\) is obtained from \(I_k\) in the following way: as elements one takes the least element \(I_k\), as well as all those elements whose negation is equal to the least element; among these elements their ordering in \(I_k\) is preserved.
c) The structures \(E_k\) \((k=1,2,\ldots)\). The implicative structure
\[ E_k=\Gamma\left(I_0^k\right) \]
(in particular \(E_1=I_1\)).
We shall denote the greatest element of an implicative structure \(S\) by zero. A formula \(F\) of propositional logic will be called generally valid on \(S\) if, when the operations \(&,\vee,\supset,\neg\) are replaced respectively by the operations \(\cap,\cup,\to,\sim\), and under any substitution of elements of \(S\) for the propositional variables of the formula \(F\), the formula takes the value \(0\) after the results of all operations have been computed in accordance with their definitions. If \(F\) is not generally valid on \(S\), then we shall say that \(F\) is refuted on \(S\).
- Theorem 1. a) In order that, in the sk-calculus \(P\), exactly those formulas be derivable which are generally valid on \(I_0\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on \(I_0\) and that at least one of them be refuted on
\[ I_1=\Gamma(I_0^1). \]
b) In order that, in the sk-calculus \(P\), exactly those formulas be derivable which are generally valid on every \(J_k\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on every \(J_k\) and that at least one of them be refuted on
\[ E_2=\Gamma(I_0^2). \]
c) In order that, in the sk-calculus \(P\), exactly those formulas be derivable which are generally valid on every \(E_k\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on every \(E_k\) and that at least one of these axioms be refuted on the structure
\[ \Gamma(I_1). \]
d) In order that, in the sk-calculus \(P\), exactly those formulas be derivable which are generally valid on \(I_1\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on \(I_1\), that at least one additional axiom be refuted on \(\Gamma(I_1)\), and that at least one be refuted on \(E_2\).
In Theorem 2, statement a) is a well-known fact and is given for the sake of symmetry of the formulations.
Theorem 2. a) In the sk-calculus \(\mathfrak K\), exactly those formulas are derivable which are generally valid on \(I_0\).
b) In the sk-calculus \(\mathfrak L\), exactly those formulas are derivable which are generally valid on all \(J_k\).
c) In the sk-calculus \(\mathfrak M\), exactly those formulas are derivable which are generally valid on all \(E_k\).
d) In the sk-calculus \(\mathfrak N\), exactly those formulas are derivable which are generally valid on \(I_1\).
From Theorems 1 and 2 it follows that
Theorem 3. a) In order that the sk-calculus \(P\) be equivalent to the classical calculus \(\mathfrak K\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on \(I_0\) and that at least one of them be refuted on \(I_1\).
b) In order that the sk-calculus \(P\) be equivalent to the calculus \(\mathfrak L\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on all \(J_k\) and that at least one of them be refuted on \(E_2\).
c) In order that the sk-calculus \(P\) be equivalent to the calculus \(\mathfrak M\), it is necessary and sufficient that all the additional axioms of \(P\) be generally valid on all \(E_k\) and that at least one of them be refuted on \(\Gamma(I_1)\).
d) In order that the sk-calculus \(P\) be equivalent to the calculus \(\mathfrak N\),
necessary and sufficient that all additional axioms of \(P\) be valid on \(I_1\), that at least one of them be refuted on \(\Gamma(I_1)\), and that at least one be refuted on \(E_2\).
In parts a) and г) of this theorem there is, in essence, already contained an algorithm for deciding whether a given sc-calculus \(P\) is equivalent to the calculus \(\mathfrak K\) or \(\mathfrak N\), respectively. To construct such an algorithm for the calculi \(\mathfrak L\) and \(\mathfrak M\), it is enough to learn how to decide whether a given formula \(F\) is valid on all \(J_k\) (on all \(E_k\)). This can be done on the basis of the following lemma, which is valid by virtue of the “Leningrad principle” \({}^{5}\):
Lemma. Every formula \(F\) is either derivable in \(\mathfrak L\) (in \(\mathfrak M\)), and then it is valid on all \(J_k\) (\(E_k\)), or it is refuted on some \(J_k\) (\(E_k\)).
Of course, in practice these algorithms will be cumbersome.
The definition of an sc-calculus was introduced by A. V. Kuznetsov in a talk at the seminar on mathematical logic at Moscow University. The set of formulas valid on \(I_1\) was studied by Ya. S. Smetanich \({}^{4}\). He also informed the author that, as the single additional axiom for obtaining an sc-calculus equivalent to \(\mathfrak N\), it suffices to take the formula
\[ (a \supset b)\vee(b \supset c)\vee(c \supset d). \]
The proofs of the theorem are constructive.
Mathematical Institute named after V. A. Steklov
Academy of Sciences of the USSR
Received
9 III 1963
CITED LITERATURE
\({}^{1}\) S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
\({}^{2}\) G. Birkhoff, Theory of Structures, Moscow, 1952.
\({}^{3}\) H. Sugg, Leçons de logique algébrique, Paris, 1952.
\({}^{4}\) Ya. S. Smetanich, Transactions of the Moscow Mathematical Society, 9, 357 (1960).
\({}^{5}\) A. A. Markov, Proceedings of the Third All-Union Mathematical Congress, 2, 146 (1956).