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 .

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 .

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

An intermediate logic is called solvable if there is an algorithm that, for any propositional formula , recognizes whether does or does not belong to . 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 is called disjunctive if implies that or . 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 (Craig's theorem) is that if a formula belongs to , then there is a formula containing only variables that are common to both and and such that or ; if and have no variables in common, then or . 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 is called expressible in formulas in an intermediate logic if can be obtained from using a finite number of replacements by equivalent (in ) formulas and a finite number of substitutions of formulas that have already been obtained for variables. A list of formulas is called functionally complete in if every formula in is expressible in . 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 is expressible in for a given formula and list — 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 of structures (models) on which a truth relation of a given propositional formula under a given valuation is defined. (A valuation is a mapping assigning some value in to the variables in a formula .) A formula that is true in under every valuation is called generally valid on (denoted by ). If , then the intermediate logic is the set of all formulas that are generally valid on every structure . For a given semantics the relation of semantic implication , where consists of formulas, is naturally defined. This relation means that for any structure , the relation for all implies . Two semantics and are called equivalent if the relations and coincide. The basic requirement on a semantics is its correctness: must imply . All semantics mentioned below are correct. Another important property of semantics is completeness. An intermediate logic is called complete relative to a semantics if .

An algebraic semantics consists of a pseudo-Boolean algebra, i.e. an algebra of the form

where is a unary operation, and , , are binary operations on , corresponding to the connectives , , , ; is a distributive lattice; and and are the least and the largest element of . The operations , satisfy: For any ,

Here, the relation means that takes in the value 1 under every valuation .

Every intermediate logic is complete relative to finitely-generated pseudo-Boolean algebras. If an intermediate logic 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 consists of a Kripke model (cf. Kripke models), having in this case the form , where is a partially ordered set, also called the frame, and where the values of the valuation form a subset of , where for it follows from and that . There is a close connection between the semantics and (cf. [5]); they are, however, not equivalent. In particular, there are intermediate logics that are not complete relative to (cf. [3]).

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

Predicate intermediate logics are defined analogously to propositional intermediate logics, i.e. it are extensions of intuitionistic predicate logic 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)