A characterization of fragments of the intuitionistic propositional logic
Małgorzata Porębska, Andrzej Wroński · 1974
We shall use the symbols: →,↔, ∧, ∨, ¬ as the well-known connectives (implication, equivalence, conjunction, disjunction, negation). For every set of connectives Y ⊆ {→,↔, ∧, ∨, ¬} by FΨ we mean the set of formulas built up by means of propositional variables from an infinite set V and the connectives from Ψ (we shall write F instead of operation C in FΨ is called Ψ-consequence (see [1]) iff the following conditions hold for every X ⊆ FΨ, α, β ∈ FΨ: (→) if →∈ Ψ then C(X ∪ {β}) ⊆ C(X ∪ {α}) iff α→ β ∈ C(X), (↔) if ↔∈ Ψ then C(X ∪ {β}) = C(X ∪ {α}) iff α↔ β ∈ C(X), (∧) if ∧ ∈ Ψ then C({α, β}) = C({α ∧ β}), (∨) if ∨ ∈ Ψ then C(X ∪ {α}) ∩ C(X ∪ {β}) = C(X ∪ {α ∨ β}), (¬) if ¬ ∈ Ψ then C(X ∪ {α}) = FΨ iff ¬α ∈ C(X).