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.

Symbol	Unicode	Name	Meaning
∧	U+2227	Conjunction	And
∨	U+2228	Disjunction	Or (finite)
⋁	U+22C1	Big disjunction	Infinite or
∃	U+2203	Exists	Existential
⊤	U+22A4	True	Always
⊥	U+22A5	False	Never
⊢	U+22A2	Entails	Sequent
ₓ	U+2093	Subscript x	Context annotation on the turnstile, φ ⊢ₓ ψ
ᵢ	U+1D62	Subscript i	Index of a disjunct in ⋁ᵢ φᵢ
₁	U+2081	Subscript one	First argument in R(t₁,...,tₙ)
ₙ	U+2099	Subscript n	Last argument in R(t₁,...,tₙ); also the schema index
⋯	U+22EF	Midline ellipsis	Repetition in x + ⋯ + x
≥	U+2265	Greater than or equal	Range of the schema, n ≥ 1
·	U+00B7	Middle dot	Scalar repetition n·x in the group examples
¬	U+00AC	Negation	Excluded from geometric formulas
→	U+2192	Implication	Excluded from formulas; a geometric morphism arrow
∀	U+2200	For all	Excluded from formulas; implicit at the turnstile
φ, ψ	—	Formula metavariables	Geometric formulas in a sequent
::=	—	Grammar production	Formation rule for geometric formulas
R(t₁,...,tₙ)	—	Atomic formula	Relation applied to terms
Set[T]	—	Classifying topos	Topos whose points are the Set-models of T
Inv	—	Invertibility predicate	As in the coherent axiom for local rings

Metatheory. Every geometric theory over a small signature has a classifying topos Set[T], and conversely every Grothendieck topos classifies some geometric theory, so Grothendieck toposes and geometric theories are one subject presented twice. Two theories have equivalent classifying toposes exactly when they have equivalent categories of models in every topos, naturally in the topos — Morita equivalence — so the classifying topos is an invariant of the models rather than of the axioms. Completeness holds for the generic model: a geometric sequent is derivable iff it holds in the generic model of Set[T]. It does not hold for Set-models, because a Grothendieck topos may have no points at all; Deligne's theorem (SGA4) says coherent toposes do have enough points, which is exactly the completeness theorem for the finitary coherent fragment. Barr's theorem gives every Grothendieck topos a surjection from a Boolean one, so a geometric sequent derivable classically from geometric axioms is already derivable intuitionistically.

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

Limitations. Completeness for Set-models fails: a Grothendieck topos can have no points, so a consistent geometric theory need have no model in Sets, and only the finitary coherent fragment is rescued by Deligne's theorem. Infinitary disjunction costs compactness and the Löwenheim–Skolem theorems, and the proof system is infinitary — the disjunction rule takes one premise per disjunct — so derivations are not finite objects and there is no recursive complete calculus for geometric logic as there is for the coherent fragment. Classifying toposes require a small signature. The classifying topos determines a theory only up to Morita equivalence, so it cannot distinguish axiomatizations of the same models. Negation, implication and universal quantification are barred from formulas; the sequent supplies one of each at the turnstile, but properties whose antecedent genuinely needs ∀ inside it, such as having trivial centre, remain non-geometric.