Intuitionistic Logic and Projective Beth Property

Larisa Maksimova

We consider the family E(Int) of all superintuitionistic logics. It is well known that there is a duality between E(Int) and the family of varieties of Heyting algebras.

Let x, q, q′ be disjoint lists of variables not containing y and z, Γ(x, q, y) a set of formulas. We say that a logic L has the projective Beth property PBP if Γ(x, q, y), Γ(x, q′, z) ⊢ _{L}y ↔ z implies Γ(x, q, y) ⊢_{L} y ↔ C(x) for some formula C(x); the Beth Property BP arises from PBP by deleting q and q′.

It is known [Maksimova 77] that there exist exactly 8 extensions of Int with Craig’s interpolation property CIP, and L ∈ E(Int) has CIP iff its associated variety V (L) has the Amalgamation Property AP. All extensions of Int have BP [Kreisel 60], and CIP implies PBP in E(Int).

We say that a variety V has the property SES if for any B in V and its subalgebra A, for any b ∈ B − A there exist C ∈ V and homomorphisms β : B → C and γ : B → C such that β(x) = γ(x) for all x ∈ A and β(b) ≠ γ(b).

Lemma 1. For each logic L in E(Int), L satisfies PBP iff V (L) has SES.

Proposition 2. Let L be any logic in E(Int).

(i) If L has CIP then L and Δ(L) have PBP.

(ii) If L has PBP then L + ¬p ∨ ¬¬p has PBP.

Here Δ(L) = Int + {p ∨ (p → A)|A ∈ L and p is not in A} [Hosoi 67]. By this proposition, at least 15 logics in E(Int) have PBP. These logics are finitely axiomatizable and have the finite model property.

Theorem 3. There exist exactly 16 logics with PBP in E(Int). Their list contains eight logics with CIP and, moreover, five logics of the form Δ(L) and two logics of the form Δ(L) + ¬p ∨ ¬¬p, where L has CIP, and one more logic which is characterized by four-element linearly ordered Heyting algebra.

It follows that there are exactly 16 varieties of Heyting algebras with SES.

Theorem 4. (i) There exist an algorithm which for any extension of Int by finitely many axiom schemes decides whether this extension possesses PBP or not.

(ii) SES is base-decidable on the family of varieties of Heyting algebras.

Address: Institute of Mathematics, Siberian Branch of Russian Academy of Sciences, 630090 Novosibirsk, Russia

E-mail: lmaksi@math.nsc.ru