Geometric Logic

Origin. Emerged from topos theory and categorical logic (1970s). Formulas preserved by geometric morphisms (topos maps). Characterizes constructively well-behaved theories. Important in algebraic geometry and classifying toposes. Related to regular and coherent logic.

Models. Logic preserved across toposes. Geometric formulas: built from atoms, ∧, ∨ (including infinite), ∃, ⊤, ⊥. No ¬, →, or ∀. These formulas are preserved by inverse images of geometric morphisms. Theories axiomatizable in geometric logic have classifying toposes.

Formalism.

Geometric formula: φ ::= ⊤ | ⊥ | R(t₁,...,tₙ) | φ ∧ ψ | ⋁ᵢ φᵢ | ∃x.φ

No implication, negation, or universal quantification.

Geometric sequent: φ ⊢ₓ ψ "In context x, if φ then ψ" (where φ, ψ geometric).

Geometric theory: Set of geometric sequents.

Hierarchy:

• Algebraic: only equations t = s
• Regular: atomic, ∧, ∃, ⊤
• Coherent: regular + finite ∨, ⊥
• Geometric: coherent + infinite ∨

Examples:

• Local rings: coherent (x + y = 1 ⊢ Inv(x) ∨ Inv(y))
• Fields: coherent (⊢ x = 0 ∨ ∃y.xy = 1)
• Torsion-free abelian groups: coherent, hence geometric — one sequent for each n ≥ 1, n·x = 0 ⊢ₓ x = 0
• Torsion abelian groups: geometric but not coherent — needs the infinite disjunction ⊤ ⊢ₓ ⋁_{n ≥ 1} n·x = 0
• Groups with trivial centre: not geometric — the antecedent needs ∀, ∀y (xy = yx) ⊢ₓ x = e

Torsion-freeness is the case worth dwelling on, because writing it as a single formula ∀n (n·x = 0 → x = 0) makes it look non-geometric and it is not. Two things are going on. The n is a metalanguage index, not an object variable — the language of groups has no sort for it, and n·x abbreviates x + ⋯ + x — so this is an axiom schema, one coherent sequent per n. And the implication sits at the turnstile, not inside a formula.

That is the general point: a geometric sequent φ ⊢ₓ ψ already carries an implication and a universal closure, so theories can express far more than the geometric formulas alone suggest. Implication and ∀ are barred only from the φ and ψ.

Classifying topos: For geometric theory T, there exists a topos Set[T] such that:

• Points of Set[T] = models of T in Set
• Models in any topos E = geometric morphisms E → Set[T]

Symbols.

Metatheory. Geometric logic is complete for topos semantics. Geometric morphisms preserve geometric truth. Classifying topos exists for every geometric theory. Deligne's theorem: coherent toposes have enough points. Barr's theorem: geometric consequences of geometric axioms hold classically iff intuitionistically.

Applies to. Algebraic geometry (scheme theory). Topos theory foundations. Constructive algebra. Classifying spaces (homotopy theory). Database theory (regular logic). Categorical model theory.

Limitations. No negation or implication — limited expressiveness. Many natural properties not geometric. Infinite disjunctions may be problematic computationally. Requires category theory fluency. Less intuitive than standard first-order logic. Specialized applications mainly in pure mathematics.

© 2026 Lingenic LLC