Internal Logic

Origin. Lawvere, Kock, and others (1960s-1970s). Logic interpreted inside a category. Subobject classifier replaces truth values. Intuitionistic in general topoi. Foundation for categorical proof theory.

Models. Categories as universes of discourse. Objects as types, morphisms as functions. Subobjects as predicates. Power object for quantification. Ω (subobject classifier) for truth.

Formalism.

Subobject classifier: Ω: object of truth values. true: 1 → Ω (the "true" element). χ_m: A → Ω classifies subobject m: S ↣ A.

Propositions: Subobjects of 1 (global sections of Ω). In Set: Ω = {0,1}, two propositions. In general topos: richer Ω structure.

Connectives as operations on Ω: ∧: Ω × Ω → Ω (meet in Ω) ∨: Ω × Ω → Ω (join in Ω) ⇒: Ω × Ω → Ω (Heyting implication) ¬: Ω → Ω (¬p = p ⇒ ⊥)

Quantifiers: ∀_f: Ω^A → Ω^B (right adjoint to f*) ∃_f: Ω^A → Ω^B (left adjoint to f*) Along f: A → B.

Internal language: Mitchell-Bénabou language. Variables range over objects. Formulas interpreted as subobjects.

Topos validity: ⊨ φ iff φ interpreted as 1 ≅ {x | φ(x)}. Intuitionistic in general topoi.

Symbols.

Symbol	Unicode	Name	Meaning
Ω	U+03A9	Omega	Subobject classifier, the object of truth values
↣	U+21A3	Rightwards arrow with tail / Monomorphism	A subobject m : S ↣ A
χ	U+03C7	Small letter chi / Characteristic map	χ_m classifies the subobject m
⊨	U+22A8	True / Satisfies	Internal validity of a formula
⊩	U+22A9	Forces	Kripke–Joyal forcing at a stage
∧	U+2227	Logical and / Conjunction	Meet in the Heyting algebra Ω
∨	U+2228	Logical or / Disjunction	Join in Ω
⇒	U+21D2	Rightwards double arrow / Heyting implication	Relative pseudocomplement in Ω
¬	U+00AC	Not sign / Negation	Defined as p ⇒ ⊥; not involutive
⊥	U+22A5	Up tack / Falsum	Bottom of Ω
⊤	U+22A4	Down tack / Verum	Top of Ω, the image of true
∀	U+2200	For all / Universal quantifier	Right adjoint to pullback along f
∃	U+2203	There exists / Existential quantifier	Left adjoint to pullback along f
×	U+00D7	Multiplication sign / Product	Domain of the binary connectives, Ω × Ω
→	U+2192	Rightwards arrow	A morphism; also an exponential in Ω^A
≅	U+2245	Approximately equal to / Isomorphism	Validity is the terminal object being the extension of φ
φ	U+03C6	Small letter phi	A formula of the internal language
x	—	Variable	Bound by the comprehension {x \| φ(x)}
A, B, S	—	Objects	Types of the internal language; S ↣ A is a subobject
f	—	Morphism	f : A → B, along which ∀_f and ∃_f are taken
m	—	Mono	The subobject being classified
true	—	True	The map 1 → Ω picking the top element
Ω^A	—	Power object	Predicates on A; the site of quantification
f*	—	Pullback	Substitution functor along f : A → B
{ }	—	Comprehension	Extension of a formula, the subobject where φ holds
1	—	Terminal object	Propositions are subobjects of it
Sub(A)	—	Subobject lattice	A Heyting algebra for every object A
Sh(X)	—	Sheaf topos	Where Kripke–Joyal becomes forcing over open sets

Metatheory. Every elementary topos carries the Mitchell–Bénabou language: a typed higher-order language whose types are objects, whose terms are morphisms, and whose formulas are terms of type Ω, interpreted as subobjects. The interpretation is sound and complete for intuitionistic higher-order logic, and Lambek and Scott's Introduction to Higher Order Categorical Logic (1986) proves the correspondence is an equivalence: toposes with logical morphisms and higher-order intuitionistic type theories with translations are the same 2-category up to equivalence, with the syntactic topos of a theory as the generic model. Sub(A) is a Heyting algebra for every A, and it is Boolean for every A exactly when the topos is Boolean; by Diaconescu's theorem (1975) the internal axiom of choice forces this, so choice and non-classical internal logic are incompatible. Kripke–Joyal semantics gives the forcing clauses stage by stage over generalized elements, reducing to Kripke semantics in a presheaf topos and to sheaf forcing over the opens of a space in Sh(X).

Applies to. Topos theory. Synthetic differential geometry. Sheaf models. Type theory semantics. Categorical foundations.

Limitations. The internal logic is intuitionistic, and this is not a presentational choice: Sub(A) is Heyting rather than Boolean in almost every topos, and imposing Booleanness or internal choice collapses the interesting examples by Diaconescu's theorem. Internal validity means validity at every stage, so it does not agree with external truth — an internally provable existential need not have a global element as witness, and internal completeness, internal smallness and internal well-ordering all differ from their external counterparts. The Mitchell–Bénabou language is typed and higher-order but bounded: there is no untyped quantification, no global membership relation and no way to quantify over classes. Being a logic of subobjects it is proof-irrelevant, since Sub(A) is a poset and distinct derivations of a formula are identified. An elementary topos need not have a natural numbers object, so arithmetic is unavailable unless assumed, and Sub(1) may have many elements, so the logic need not be two-valued.