Basic Logic (Sambin)

Origin. Sambin, Battilotti, and Faggian, "Basic logic: reflection, symmetry, visibility" (Journal of Symbolic Logic 65, 2000); roots in Sambin's formal topology and Battilotti's 1997 thesis. A sequent calculus B proposed as the base from which classical, intuitionistic, quantum, and non-modal linear logic are all obtained as extensions in a single framework, by adding structural rules while the operational rules stay fixed.

Models. A logic below linear logic. Where linear logic controls weakening and contraction, B adds a strict control of contexts: all active formulas in every rule are isolated. Three properties characterize it positively—reflection, symmetry, and visibility—and each of the familiar logics is recovered by relaxing one of them.

Formalism.

Reflection: A connective is characterized by an equation binding it to a metalinguistic link between assertions. Its inference rules are obtained by solving that equation. Every connective of B satisfies reflection; none is stipulated.

Visibility: No context on the active side of any rule. Active formulas are isolated: Γ ⊢ A, not Γ ⊢ A, Δ. This is the control B adds on top of linear logic's control of weakening and contraction.

Symmetry: Left and right rules mirror each other. Each connective has a dual; the calculus is self-dual under the exchange.

The cube of extensions: Add weakening and contraction → intuitionistic and classical. Drop visibility → linear. Drop symmetry on one side → intuitionistic-style single conclusion. Restrict to the additive fragment with an orthogonality → quantum (orthologic). Each corner is B plus structural rules only.

Connectives: Multiplicative and additive pairs, as in linear logic. Their rules are derived by reflection rather than posited.

Symbols.

Metatheory. Cut elimination holds for B and is inherited by every extension, since the extensions add structural rules only and leave the operational rules untouched. That inheritance is the framework's payoff: the differences between classical, intuitionistic, quantum, and linear logic are relocated into structure, and the proof theory is not recomputed at each corner. The mechanism is the definitional equation. A connective is not posited by its rules; one writes an equation identifying an assertion about the compound with a metalinguistic link between assertions about the components — Γ ⊢ A ⊗ B when Γ splits as Γ₁, Γ₂ with Γ₁ ⊢ A and Γ₂ ⊢ B — and the inference rules are read off by solving it, which is what "reflection" names. Visibility is what makes the quantum corner work: Faggian and Sambin (1998) obtained orthologic with cut elimination, which the usual two-sided presentations of quantum logic lack, because forbidding context on the active side blocks exactly the steps that break cut. Ardeshir and Vaezian (2012) gave a unification of the basic logics of Sambin and of Visser, distinct systems sharing a name.

Applies to. Foundational analysis of what a connective is. Comparison of logics within one calculus. Formal topology, where the programme originated. The proof-theoretic semantics literature on what justifies an inference rule.

Limitations. Small literature and few implementations. The name collides with two other systems: Hájek's BL, a fuzzy logic complete for continuous t-norms, and Visser's basic propositional logic. Whether visibility is a structural rule in Gentzen's sense, or a further constraint of a different kind, is arguable—and the claim that the extensions differ "only structurally" rests on that classification. Reflection is a criterion internal to the framework: that every connective of B satisfies it is a theorem about B, not an independent test of B's adequacy.

© 2026 Lingenic LLC