Intermediate logic

of propositions, propositional intermediate logic

An arbitrary consistent set of propositional formulas that is closed under the derivation rule modus ponens and the substitution rule, and that contains all axioms of intuitionistic propositional calculus $ I $.

The most natural way of specifying intermediate logics is by intermediate propositional calculi. Each such calculus is given by adding a certain number of classical generally-valid propositional formulas to the axioms of $ I $.

The set of all intermediate logics is a lattice under the inclusion relation $ \subseteq $, and the finitely-axiomatizable intermediate logics form a sublattice in it, in which every finite distributive lattice can be isomorphically imbedded.

An intermediate logic $ L $ is called solvable if there is an algorithm that, for any propositional formula $ A $, recognizes whether $ A $ does or does not belong to $ L $. Thus, classical and intuitionistic logic are both solvable. In general, any finitely-approximated (cf. below) finitely-axiomatizable intermediate logic is solvable. An example of a finitely-axiomatizable unsolvable intermediate logic has been constructed (cf. [7]).

An intermediate logic $ L $ is called disjunctive if $ ( A \lor B ) \in L $ implies that $ A \in L $ or $ B \in L $. Intuitionistic logic, e.g., has this property, but classical logic does not. There is an infinite number of disjunctive intermediate logics.

The interpolation property of an intermediate logic $ L $( Craig's theorem) is that if a formula $ A \supset B $ belongs to $ L $, then there is a formula $ C $ containing only variables that are common to both $ A $ and $ B $ and such that $ ( A \supset C ) \in L $ or $ ( C \supset B ) \in L $; if $ A $ and $ B $ have no variables in common, then $ \neg A \in L $ or $ B \in L $. It has been proved that there are exactly five intermediate logics (apart from the classical and intuitionistic logics) that have the interpolation property (cf. [6]).

A formula $ A $ is called expressible in formulas $ B _ {1} , B _ {2} \dots $ in an intermediate logic $ L $ if $ A $ can be obtained from $ B _ {1} , B _ {2} \dots $ using a finite number of replacements by equivalent (in $ L $) formulas and a finite number of substitutions of formulas that have already been obtained for variables. A list of formulas $ \Sigma = \{ B _ {1} , B _ {2} ,\dots \} $ is called functionally complete in $ L $ if every formula in $ L $ is expressible in $ \Sigma $. For intuitionistic logic and certain other intermediate logics the algorithmic problem of recognizing functional completeness of any list of formulas is solvable (cf. [3]). Another algorithmic problem — recognizing whether $ A $ is expressible in $ \Sigma $ for a given formula $ A $ and list $ \Sigma $— has been positively solved only for some intermediate logics; it remains open yet (1983) for intuitionistic logic.

Another way of specifying an intermediate logic is given by the so-called semantic approach. A semantics is, here, understood as a certain set $ S $ of structures (models) $ \mathfrak M $ on which a truth relation $ \mathfrak M \vDash _ \theta A $ of a given propositional formula $ A $ under a given valuation $ \theta $ is defined. (A valuation is a mapping assigning some value in $ \mathfrak M $ to the variables in a formula $ A $.) A formula $ A $ that is true in $ \mathfrak M $ under every valuation is called generally valid on $ \mathfrak M $( denoted by $ \mathfrak M \vDash A $). If $ S _ {1} \subseteq S $, then the intermediate logic $ L ( S _ {1} ) $ is the set of all formulas that are generally valid on every structure $ \mathfrak M \in S _ {1} $. For a given semantics $ S $ the relation of semantic implication $ \Gamma \vDash _ {S} A $, where $ \Gamma $ consists of formulas, is naturally defined. This relation means that for any structure $ \mathfrak M \in S $, the relation $ \mathfrak M \vDash B $ for all $ B \in \Gamma $ implies $ \mathfrak M \vDash A $. Two semantics $ S $ and $ S _ {1} $ are called equivalent if the relations $ \vDash _ {S} $ and $ \vDash _ {S _ {1} } $ coincide. The basic requirement on a semantics is its correctness: $ \Gamma \vdash _ {I} A $ must imply $ \Gamma \vDash _ {S} A $. All semantics mentioned below are correct. Another important property of semantics is completeness. An intermediate logic $ L $ is called complete relative to a semantics $ S $ if $ A \in L \iff L \vDash _ {S} A $.

An algebraic semantics $ S _ {A} $ consists of a pseudo-Boolean algebra, i.e. an algebra of the form

$$ \mathfrak M = ( M , \overline{\&}\; , \overline \lor \; ,\ \overline \supset \; , \overline \neg \; ; 1 , 0 ) , $$

where $ \overline \neg \; $ is a unary operation, and $ \overline{\&}\; $, $ \overline \lor \; $, $ \overline \supset \; $ are binary operations on $ M $, corresponding to the connectives $ \neg $, $ \& $, $ \lor $, $ \supset $; $ ( M , \overline{\&}\; , \overline \lor \; ) $ is a distributive lattice; and $ 0 $ and $ 1 $ are the least and the largest element of $ M $. The operations $ \overline \supset \; $, $ \overline \neg \; $ satisfy: For any $ a , b , c \in M $,

$$ a \leq ( b \overline \supset \; c ) \iff \ ( a \overline{\&}\; b ) \ \textrm{ and } \ \ \overline \neg \; a = ( a \overline \supset \; 0 ) . $$

Here, the relation $ \mathfrak M \vDash _ \theta A $ means that $ A $ takes in $ \mathfrak M $ the value 1 under every valuation $ \theta $.

Every intermediate logic is complete relative to finitely-generated pseudo-Boolean algebras. If an intermediate logic $ L $ is complete relative to a set of finite pseudo-Boolean algebras (relative to one finite pseudo-Boolean algebra), then it is called finitely approximated (respectively, tabular). The simplest tabular intermediate logic is classical logic. Disjunctive intermediate logics, in particular intuitionistic logic, are not tabular. There exists an example of a finitely-axiomatizable intermediate logic that is not finitely approximated (cf. [3]).

A Kripke semantics $ S _ {K} $ consists of a Kripke model (cf. Kripke models), having in this case the form $ ( \mathfrak M , \theta ) $, where $ \mathfrak M = ( M , \leq ) $ is a partially ordered set, also called the frame, and where the values of the valuation $ \theta $ form a subset of $ M $, where for $ \alpha , \beta \in M $ it follows from $ \alpha \in \theta ( p _ {i} ) $ and $ \alpha \leq \beta $ that $ \beta \in \theta ( p _ {i} ) $. There is a close connection between the semantics $ S _ {A} $ and $ S _ {K} $( cf. [5]); they are, however, not equivalent. In particular, there are intermediate logics that are not complete relative to $ S _ {K} $( cf. [3]).

The constructive semantics are the semantics $ S _ {R} $ of realizability (cf. [1]) and the semantics $ S _ {F} $ for finitary problems. These semantics are not complete even for intuitionistic logic; moreover, there are formulas that are generally valid in $ S _ {R} $ but not in $ S _ {K} $, and vice versa.

Predicate intermediate logics are defined analogously to propositional intermediate logics, i.e. it are extensions of intuitionistic predicate logic $ L I $ contained in classical predicate logic. As distinct from propositional intermediate logics, all predicate intermediate logics are unsolvable. The semantics of predicate intermediate logics are analogous to the corresponding semantics of propositional intermediate logics (cf. [2]).

References

[1]	P.S. Novikov, "Constructive mathematical logic from a classical point of view" , Moscow (1977) (In Russian)
[2]	A.G. Dragalin, "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc. (1988) (Translated from Russian)
[3]	A.V. Kuznetsov, "Means for detecting nonreducibility and inexpressibility" , Logical derivations , Moscow (1979) pp. 5–33 (In Russian)
[4]	A.V. Kuznetsov, "Superintuitionistic logics" Mat. Issled. , 10 : 2 (1975) pp. 150–158; 284–285 (In Russian)
[5]	L.L. Esakia, "On the theory of modal and superintuitionistic systems" , Logical derivations , Moscow (1979) pp. 147–172 (In Russian)
[6]	L.L. Maksimova, "Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras" Algebra and Logic , 16 (1977) pp. 427–455 Algebra i Logika , 16 (1977) pp. 643–681
[7]	V.B. [V.B. Shekhtman] Šehtman, "An undecidable superintuitionistic propositional calculus" Soviet Math. Dokl. , 19 : 3 (1978) pp. 656–660 Dokl. Akad. Nauk. SSSR , 240 : 3 (1978) pp. 549–552
[8]	T. Hosoi, H. Ono, "Intermediate propositional logics (a survey)" J. Tsuda College , 5 (1973) pp. 67–82

Comments

I.e. an intermediate logic is a propositional logic which is intermediate between intuitionistic and classical propositional logic.

For realizability see [a1], for Kripke semantics [a2] and for pseudo-Boolean algebras [a3].

References

[a1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[a2]	M.C. Fitting, "Intuitionistic logic, model theory and forcing" , North-Holland (1969)
[a3]	E. Rasiowa, R. Sikorski, "The mathematics of metamathematics" , Polska Akad. Nauk (1963)