Identity Logic

Origin. Frege (1879), Leibniz earlier. Identity as logical notion. Substitutivity. Indiscernibility of identicals. Foundation for quantified logic.

Models. Identity interpreted as actual equality. Leibniz's law: identicals share all properties. Normal models: = is true identity. General models allow non-standard.

Formalism.

Identity axioms: ∀x. x = x (reflexivity) ∀x∀y. (x = y → y = x) (symmetry) ∀x∀y∀z. (x = y ∧ y = z → x = z) (transitivity)

Leibniz's law (substitutivity): x = y → (φ[x/z] ↔ φ[y/z]) Identical objects satisfy same formulas.

Indiscernibility of identicals: x = y → ∀P.(Px ↔ Py) Second-order formulation.

Identity of indiscernibles: ∀P.(Px ↔ Py) → x = y Converse, philosophically disputed.

First-order identity: Finite axiom schema. φ[x/z] → (x = y → φ[y/z]) For each formula φ.

Normal vs general models: Normal: = is true equality. General: = any equivalence relation. Categoricity differences.

Identity elimination: Not eliminable in first-order. Higher-order: definable as ∀P.(Px ↔ Py).

Symbols.

Metatheory. Decidable with identity (finite models). Complete axiomatization. Normal models characterize arithmetic. Complexity same as FOL.

Applies to. Mathematics foundations. Database queries. Equality reasoning. Rewriting systems.

Limitations. Intensional contexts fail substitutivity. De re vs de dicto. Non-rigid designators. Opacity.

© 2026 Lingenic LLC