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: geometric theory
Fields: coherent (x = 0 ∨ ∃y.xy = 1)
Torsion-free groups: not geometric (∀n.nx = 0 → x = 0 uses →)

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

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.