Identity Logic

Origin. Leibniz stated the two principles that bear his name — identicals are indiscernible, and (more contentiously) indiscernibles are identical. Frege gave identity its first formal treatment in the Begriffsschrift (1879), where he read it as sameness of content between signs, and revised that reading in "Über Sinn und Bedeutung" (1892) after seeing that the informativeness of a = b cannot be explained if identity relates signs. Whitehead and Russell's Principia defined identity second-order, by indiscernibility. Hilbert and Ackermann (1928) fixed the modern first-order treatment: identity as a distinguished binary predicate with its own axioms, part of the logic rather than of any theory.

Models. Identity is the one predicate whose interpretation is fixed in advance. In a normal model the symbol = denotes the actual diagonal — the relation each element bears to itself and to nothing else — so it is not a parameter that varies from structure to structure the way R or f do. The axioms do not force this. What they force is that = denote a congruence: an equivalence relation respected by every function and predicate of the signature. Models in which = denotes a proper congruence are the general (or non-normal) models, and each collapses onto a normal one by quotienting, which is what makes the axiomatization adequate.

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: Reflexivity, plus a substitution schema. φ[x/z] → (x = y → φ[y/z]) One instance for each formula φ: infinitely many axioms, finitely many schemata. Symmetry and transitivity are derivable from these.

Congruence conditions: x₁ = y₁ ∧ … ∧ xₙ = yₙ → f(x⃗) = f(y⃗). x₁ = y₁ ∧ … ∧ xₙ = yₙ → (R(x⃗) → R(y⃗)). The schema's instances for atomic φ; enough on their own.

Cardinality sentences: λₙ: ∃x₁…∃xₙ ⋀_{i<j} xᵢ ≠ xⱼ — "at least n elements." "Exactly n" is λₙ ∧ ¬λₙ₊₁. "Finitely many" is not expressible.

Normal vs general models: Normal: = denotes the diagonal. General: = denotes a congruence. Quotient by that congruence gives a normal model of the same sentences.

Identity elimination: Not definable: no formula of the =-free language denotes identity in every model. Eliminable for satisfiability: replace = by a fresh E, add the congruence axioms, and quotient. Standard in automated theorem proving. Second-order: definable outright as ∀P.(Px ↔ Py).

Symbols.

Metatheory. First-order logic with identity is sound and complete for normal models. Henkin's construction builds a term model in which = denotes a congruence rather than the diagonal, and the quotient by that congruence is a normal model of the same sentences — so the identity axioms are exactly what is needed, and compactness and the Löwenheim–Skolem theorems survive in the form "every satisfiable set has a normal model of the stated cardinality." Identity is not first-order definable: no formula of the =-free language denotes the diagonal in every structure, since indiscernible elements can always be adjoined. It is nevertheless eliminable for satisfiability, by replacing = with a fresh binary relation and adding the congruence axioms. Adding identity does not change undecidability, which is Church's and Turing's (1936); the pure identity language with no other predicates is decidable, every sentence being equivalent to a Boolean combination of the λₙ. Behmann (1922) proved monadic predicate logic with identity decidable. Second-order standard semantics defines identity outright as ∀P.(Px ↔ Py).

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

Limitations. Identity fixes no cardinality beyond the finite: λₙ says "at least n," but "finitely many" is not first-order expressible, and by compactness any theory with arbitrarily large finite models has an infinite one. So counting is available and finiteness is not. The identity of indiscernibles is not a theorem — it fails in any structure with an automorphism swapping two elements, and holds only where the language is rich enough to separate them, which makes it a claim about vocabulary rather than about objects. Substitutivity, the one uncontested principle, breaks in intensional position: modal, temporal, epistemic and quotational contexts all falsify φ[x/z] → (x = y → φ[y/z]), which is why quantified modal logic must either restrict the schema or restrict its terms to rigid designators. Free logic breaks it too, since a non-denoting term satisfies no atomic formula and t = t may fail.

© 2026 Lingenic LLC