MATHEMATICS

V. A. YANKOV

ON THE CONNECTION BETWEEN DERIVABILITY IN THE INTUITIONISTIC PROPOSITIONAL CALCULUS AND FINITE IMPLICATIVE STRUCTURES

(Presented by Academician P. S. Novikov on 20 III 1963)

On the intuitionistic propositional calculus used, on the use of the symbols (\&), (\vee) in many-place operations, and on the meaning of the derivability symbol (\vdash), see ((^1)).

By a matrix we shall mean a finite set of constructive objects (elements) with a nonempty subset of distinguished elements and with three binary operations (\cap), (\cup), (\to) and one unary operation (\sim) defined on it.

Let (F) be a formula of the propositional calculus in the variables (a_1,\ldots,a_k). A correspondence between the variables (a_1,\ldots,a_k) and the elements (x_1,\ldots,x_k) of a matrix (M),

[
a_1 \leftrightarrow x_1,\ldots,a_k \leftrightarrow x_k
]

will be called a refutation of (F) on (M), if, upon substituting in (F), for the variables (a_1,\ldots,a_k), respectively the elements (x_1,\ldots,x_k), and replacing the symbols (\&), (\vee), (\supset), (\neg) respectively by the operations (\cap), (\cup), (\to), (\sim), after computing the value of the expression obtained according to the definition of the operations (\cap), (\cup), (\to), (\sim), the resulting value (y) does not belong to the set of distinguished elements of (M); (y) is then called the value of this refutation. If the formula (F) has no refutation on (M), then (F) is called valid on (M).

A matrix (M) is called a finite implicative structure if: 1) all axioms of the intuitionistic propositional calculus ((^2)) are valid on (M); 2) whenever the elements (x) and (x \to y) are distinguished, then (y) also is a distinguished element; 3) whenever the elements (x \to y) and (y \to x) are distinguished, then the elements (x) and (y) coincide.

A finite implicative structure is called Gödelian if, whenever (a \cup b) is a distinguished element, then either (a) is a distinguished element or (b) is a distinguished element.

It can be proved that in finite implicative structures there exists only one distinguished element. If one sets aside the trivial one-element implicative structure, then the Gödelian structures are precisely those implicative structures in which there exists an element (\omega) with the following property: (\omega) is distinct from the distinguished element and, for every nondistinguished element (z), the element (z \to \omega) is distinguished.

We shall call such an element of a Gödelian implicative structure its (\omega)-element. It can be shown that it is unique.

We shall call formulas (F) and (G) distinguishable on a finite implicative structure (\alpha) if (F) is valid on (\alpha), while (G) is refutable on (\alpha) (i.e., has a refutation on (\alpha)). If (F) and (G) are distinguishable, then it is not the case that (F \vdash G).

Theorem 1. If propositional-calculus formulas (F) and (G) are distinguishable on some finite implicative structure, then they are also distinguishable on some Gödelian finite implicative structure.

To each Gödel implicative structure (\alpha) we shall assign the formula (X_\alpha) of the propositional calculus defined below, which we shall call the characteristic formula of (\alpha).

(X_\alpha) is

[
\bigwedge_{a,b\in\alpha} \bigl((t_a \& t_b)\equiv t_{a\cap b}\bigr)\ \&\
\bigwedge_{a,b\in\alpha} \bigl((t_a \vee t_b)\equiv t_{a\vee b}\bigr)\ \&\
\bigwedge_{a,b\in\alpha} \bigl((t_a \supset t_b)\equiv t_{a\to b}\bigr)\ \&
]

[
\bigwedge_{a\in\alpha} \bigl((\neg t_a\equiv t_{\sim a})\bigr)\supset t_\omega .
]

Here (a\equiv b) is used as an abbreviation for ((a\supset b)\&(b\supset a)); (\omega) is the (\omega)-element of (\alpha), and (x_a) ((a\in\alpha)) is a set of pairwise distinct variables corresponding to the elements of (\alpha).

Theorem 2. For any Gödel finite implicative structure (\alpha) and any formula (F) of the propositional calculus, the following conditions are equivalent:
1) (F\vdash X_\alpha); 2) (F) has a refutation on (\alpha).

We shall call a property (S) of formulas of the propositional calculus intuitionistic if it holds for the axioms of the intuitionistic propositional calculus and is preserved under substitution and modus ponens.

Theorem 3. For every Gödel finite implicative structure (\alpha) and every intuitionistic property (S), the following conditions are equivalent:
1) every formula possessing the property (S) is generally valid on (\alpha); 2) the formula (X_\alpha) does not possess the property (S).

In a finite implicative structure (\alpha), the elements (x_1,\ldots,x_k) form a basis if every element of (\alpha) is expressed through them by means of the operations (\cap,\ \cup,\ \to,\ \sim).

Theorem 4. If a Gödel finite implicative structure (\alpha) has a basis consisting of (k) elements, then one can construct a formula (\Phi_\alpha) on the basis of (k) distinct propositional variables such that (X_\alpha\vdash \Phi_\alpha) and (\Phi_\alpha\vdash X_\alpha).

Theorem 5. For any two Gödel finite implicative structures (\alpha,\beta), the following conditions are equivalent:
1) (X_\alpha\vdash X_\beta); 2) (X_\alpha) is refuted on (\beta); 3) every formula refutable on (\alpha) is also refutable on (\beta).

If (\alpha) and (\beta) are Gödel implicative structures and (X_\alpha) is refuted on (\beta) (one can always effectively determine whether this is the case), then we shall say that (\alpha) precedes (\beta) and denote this by (\alpha\preccurlyeq\beta).

Theorem 6. The relation (\preccurlyeq) between Gödel implicative structures is a quasi-ordering relation (\left({}^3\right)). If (\alpha\preccurlyeq\beta) and (\beta\preccurlyeq\alpha), then (\alpha) and (\beta) are isomorphic.

We shall say that (\alpha) strictly precedes (\beta) if (\alpha\preccurlyeq\beta) and (\alpha) and (\beta) are nonisomorphic.

Theorem 7. If the formulas (F) and (G) of the propositional calculus are distinguishable on a Gödel finite implicative structure (\alpha), and the value of some refutation of (G) on (\alpha) is not the (\omega)-element of (\alpha), then (F) and (G) are distinguishable on some Gödel finite implicative structure (\beta) such that (\beta) strictly precedes (\alpha).

Moscow State University
named after M. V. Lomonosov

Received
9 III 1963

REFERENCES

1. V. A. Yankov, DAN, 151, No. 5 (1963).
2. S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
3. G. Birkhoff, Theory of Structures, Moscow, 1952.