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. BPC is sound and complete for transitive Kripke frames and for the variety of weak Heyting algebras, and it is decidable, having the finite model property. The relation to IPC is exact rather than approximate: adding the single formula (A ∧ (A → B)) → B, which is what reflexivity of R validates, recovers intuitionistic logic, so BPC is IPC minus detachment and nothing else. The modal picture is the same one shifted: BPC stands to K4 as IPC stands to S4, and the Gödel-style translation lands in the transitive-but-not-reflexive logic, so the modal-companion apparatus applies below IPC as well as above it. Celani and Jansana gave weak Heyting algebras a Priestley-style duality, which places the subintuitionistic setting inside the same dual framework as Esakia's. The explicit fixed points that motivated the system are the sharpest result: for any φ(p) with p occurring only under →, an explicit ψ with ⊢ ψ ↔ φ(ψ) is constructed rather than merely proved to exist. Ardeshir and Vaezian (2012) related BPC to Sambin's basic logic, which shares the name and little 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 implication does not internalise its own detachment: modus ponens is available as a rule but (A ∧ (A → B)) → B is not a theorem, so any argument that must reason about a conditional from inside another conditional cannot use it, and there is no deduction theorem in the usual biconditional form. Conditionals therefore carry less information than they appear to — A → A is a theorem only vacuously, holding at every point precisely because a point does not see itself, and the same vacuity validates A → B at any R-terminal point whatever A and B are. Residuation is only partial, so weak Heyting algebras are not residuated lattices and the substructural machinery built on residuation does not apply. There is no Curry–Howard counterpart, since dropping detachment removes function application. And there is no classification of the subintuitionistic logics comparable to Jankov's for the intermediate ones, so BPC's position below IPC is a chosen weakening rather than a located point in a mapped lattice.

© 2026 Lingenic LLC