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 the extensions, since they add only structural rules. The framework's claim is uniformity: the operational meaning of each connective is fixed once, and the differences between classical, intuitionistic, quantum, and linear logic are relocated entirely into structure. Ardeshir and Vaezian (2012) gave a unification of the basic logics of Sambin and Visser, which are distinct systems that share 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