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) |
Intermediate logic. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Intermediate_logic&oldid=13595