Visser's Basic Propositional Logic (BPC)

Origin. Albert Visser, "A propositional logic with explicit fixed points" (1981), where the system arose from the study of provability rather than from a philosophical programme. Developed by Ruitenburg, Ardeshir, Suarez, and Celani–Jansana. A subintuitionistic logic: strictly weaker than intuitionistic propositional calculus, obtained by dropping the reflexivity of the accessibility relation.

Models. Intuitionistic Kripke semantics with reflexivity removed. Implication is still evaluated by looking forward along R, but a point no longer sees itself, so a conditional asserted at a point says nothing about that point. What survives is a logic of implication-as-forward-looking without implication-as-detachable.

Formalism.

Frames: (W, R, ⊩) with R transitive. Not reflexive—this is the whole departure from IPC. Persistence: w ⊩ p and wRv implies v ⊩ p.

Implication: w ⊩ A → B iff ∀v (wRv and v ⊩ A implies v ⊩ B) The clause is IPC's; only the frame condition changed.

What survives: ⊢ A → A (vacuously, for all accessible v) ⊢ (A → B) ∧ (B → C) → (A → C) ⊢ (A → B) ∧ (A → C) → (A → B ∧ C)

What fails: ⊬ (A ∧ (A → B)) → B Modus ponens is not an axiom: w need not be R-accessible from w. Modus ponens survives as a rule, not as a formula.

Algebraic semantics: Weak Heyting algebras (Celani and Jansana): bounded distributive lattices with a binary → satisfying (a → b) ∧ (a → c) = a → (b ∧ c) (a → c) ∧ (b → c) = (a ∨ b) → c a → a = 1, (a → b) ∧ (b → c) ≤ a → c Residuation is weakened; Heyting algebras are the reflexive case.

Fixed points: The original motivation. BPC has explicit fixed points: for φ(p) with p under →, a formula ψ with ⊢ ψ ↔ φ(ψ), constructed rather than merely asserted.

Symbols.

Metatheory. Complete for transitive Kripke frames, and for the variety of weak Heyting algebras. Decidable, with the finite model property. BPC stands to K4 as intuitionistic logic stands to S4: the Gödel-style translation lands in the transitive-but-not-reflexive modal logic. Ardeshir and Vaezian (2012) unified it with Sambin's basic logic, which shares the name and nothing else.

Applies to. Provability interpretations where reflexivity fails. The subintuitionistic lattice below IPC. Explicit fixed-point constructions. The algebraic study of weakened residuation.

Limitations. The failure of modus ponens as an axiom is hard to motivate outside the provability reading that produced it, and the system is usually studied as an object rather than adopted. The name collides with Hájek's BL and Sambin's B. The subintuitionistic region is thinly mapped compared with the intermediate logics above IPC, and BPC's place in it depends on which weakening is taken as fundamental.

© 2026 Lingenic LLC