nLab identity of indiscernibles




The principle of identity of indiscernibles states that two objects are identical if they have all the same properties.

This is also known as “Leibniz’s Law”, in honor of Gottfried Leibniz (not to be confused with his product rule, also so-called).

G. W. Leibniz around 1700, from Gerhard 1890, p. 288

Concretely, Leibniz wrote the following, (in translation from Lewis 1918, p. 373 with original Latin terms in parenthesis; see also Cartwright 1971, p. 119 and Gries & Schneider 1998):

Two terms are the same (eadem) if one can be substituted for the other without altering the truth of any statement (salva veritate). If we have AA and BB, and AA enters into some true proposition, and the substitution of BB for AA wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then AA and BB are said to be the same; …

This sentence of Leibniz in fact closes with a statement of the converse, often known as the “principle of substitutivity” but which may deserve to be called the indiscernibility of identicals:

… conversely, if PP and QQ are the same, they can be substituted for one another.

The paragraph ends with the assertion that

AA and AA are, of course, said to be the same

This is what Fichte 1794 later called the “first, absolutely unconditioned principle” and Hegel 1812- called the “first law of thought”.

From the perspective of homotopy type theory, the “first law of thought” is the term introduction-rule for identity types, and “indiscernability of identicals” is the transport-rule, which together with “identiy of indiscernible” is implied by the induction-rule of the identity type (the “J-rule”). For more on this see below.

In set theory with power sets, the inference rule for the identity of indiscernables is given by

ΓAsetΓ,xA,yA(P𝒫(A).P(x)P(y))x= Aytrue\frac{\Gamma \vdash A \; \mathrm{set}}{\Gamma, x \in A, y \in A \vdash \left(\forall P \in \mathcal{P}(A).P(x) \iff P(y)\right) \implies x =_A y \; \mathrm{true}}

In dependent type theory

Leibniz’s identity of indiscernibles

In dependent type theory, a direct translation of Leibniz’s identity of indiscernibles requires a way to quantify over all propositions and predicates. The only way this is possible is if the dependent type theory comes with a type of all propositions and thus power sets, the latter of which are the type of all predicates on a type. In addition, unlike with set theory, one cannot simply say that there is a dependent function

idOfInd A: x:A y:A( P:𝒫(A)P(x)P(y))(x= Ay)\mathrm{idOfInd}_A:\prod_{x:A} \prod_{y:A} \left(\prod_{P:\mathcal{P}(A)} P(x) \simeq P(y)\right) \to (x =_A y)

This is because the identity type has more than one element, and thus indiscernibles could be identified in more than one way. Instead, the identity of indiscenibles for type AA is given by the dependent function

idOfInd A: x:A y:A(x= Ay)( P:𝒫(A)P(x)P(y))\mathrm{idOfInd}_A:\prod_{x:A} \prod_{y:A} (x =_A y) \simeq \left(\prod_{P:\mathcal{P}(A)} P(x) \simeq P(y)\right)

More concretely, for all x:Ax:A and y:Ay:A, the principle of substitution is always true because by induction on reflexivity, one could define a function

idToInd A(x,y):(x= Ay)( P:𝒫(A)P(x)P(y))\mathrm{idToInd}_A(x, y):(x =_A y) \to \left(\prod_{P:\mathcal{P}(A)} P(x) \simeq P(y)\right)

The identity of indiscernibles is simply the statement that idToInd A(x,y)\mathrm{idToInd}_A(x, y) is an equivalence of types. This is the same concept that motivates the definition of partial orders, Kolmogorov topological spaces, and skeletal categories in terms of equivalences between identity types and a binary endorelation.

If we define the local membership relation x APx \in_A P as x APP(x)x \in_A P \coloneqq P(x), then Leibniz’s identity of indiscenibles becomes

idOfInd A: x:A y:A(x= Ay)( P:𝒫(A)(x AP)(y AP))\mathrm{idOfInd}_A:\prod_{x:A} \prod_{y:A} (x =_A y) \simeq \left(\prod_{P:\mathcal{P}(A)} (x \in_A P) \simeq (y \in_A P)\right)

This is similar to but not identical to the axiom of extensionality: the axiom of extensionality is given by

extax A: P:𝒫(A) Q:𝒫(A)(P= 𝒫(A)Q)( x:A(x AP)(x AQ))\mathrm{extax}_A:\prod_{P:\mathcal{P}(A)} \prod_{Q:\mathcal{P}(A)} (P =_{\mathcal{P}(A)} Q) \simeq \left(\prod_{x:A} (x \in_A P) \simeq (x \in_A Q)\right)

If Leibniz’s identity of indiscenibles is true for AA, then AA is a set, because the type

P:𝒫(A)P(x)P(y)\prod_{P:\mathcal{P}(A)} P(x) \simeq P(y)

is always a proposition, in the context of weak function extensionality, and thus by the equivalence of types, x= Ayx =_A y is also a proposition for all x:Ax:A and y:Ay:A, which means that AA is a set. Thus, if Leibniz’s identity of indiscernibles is true for all types AA, the dependent type theory becomes a set-level type theory with Leibniz’s identity of indiscernibles as an axiom of set truncation.

On the other hand, one does not necessarily need Leibniz’s identity of indiscernibles to be true for all types AA, because the type family

x:A,y:Aind A(x,y) P:𝒫(A)P(x)P(y)x:A, y:A \vdash \mathrm{ind}_A(x, y) \coloneqq \prod_{P:\mathcal{P}(A)} P(x) \simeq P(y)

is always an equivalence relation, and thus one could construct the quotient set

A/ind AA/\mathrm{ind}_A

as the type

A/ind A Q:𝒫(A)[ x:A y:AQ(x)ind A(x,y)]A/\mathrm{ind}_A \coloneqq \sum_{Q:\mathcal{P}(A)} \left[\sum_{x:A} \prod_{y:A} Q(x) \simeq \mathrm{ind}_A(x, y)\right]

In topological terms, this means that every type AA with its power set 𝒫(A)\mathcal{P}(A) is an R0-space and the quotient A/ind AA/\mathrm{ind}_A is a T1-space.

Type-theoretic identity of indiscernibles

For a version of the identity of indiscernibles which applies to not just sets, but other non-set types, one would have to go from quantifying over predicates to quantifying over type families: For this, one has to use a type universe UU, upon which the identity of indiscenibles for type AA is given by the dependent function

idOfInd U: x:A y:A(x= Ay)( P:AUP(x)P(y))\mathrm{idOfInd}_U:\prod_{x:A} \prod_{y:A} (x =_A y) \simeq \left(\prod_{P:A \to U} P(x) \simeq P(y)\right)

The type-theoretic identity of indiscernibles is similar to but not identical to the univalence axiom for Tarski universes: univalence for Tarski universe (U,T)(U, T) quantifies over UU-small types and fixes the type reflector type family A:UT(A)A:U \vdash T(A) for Tarski universes, while the identity of indiscernables for type AA quantifies over UU-small type families and fixes the type AA.

Other versions

In addition, extensionality principles like function extensionality, propositional extensionality, and univalence (“typal extensionality”) are naturally regarded as a stronger form of identity of indiscernibles. In particular, the consistency of univalence means that in Martin-Löf type theory without univalence, one cannot define any predicate that provably distinguishes equivalent types; thus equivalent types are “externally indiscernible”, and univalence incarnates that principle internally by making them identical.

“There are several ways to think about the axiom of univalence. One can see it as a sophisticated updating of Leibniz’s principle of the identity of indiscernibles.” –John Baez nCafé

On the other hand, the converse substitution/substitutivity principle of “indiscernibility of identicals” is expressd by transport in homotopy type theory.

In point-set topology

A topological or geometrical version of the idea of identity of indiscernibles is separation: if two points are distinct, then they are separated in some sense. This means in turn that if two points in a space subject to a given separation axiom can not be separated by any admissible separation condition then they are identical.

More in detail:

Given a topological space one might declare that “topological observations” about the space are questions of the form: “Which points are contained in a given open subset?”, and hence that two points are “discernible”, namely “topologically distinct”, if there exists an open subset that contains one but not the other. With this convention, the condition that “indiscernibles be identical” is equivalently the condition that the topological space satisfies the T 0T_0-separation axiom, hence that it is a Kolmogorov space. Generally, one could regard the T 0T_0-reflection as the modality under which identity becomes indiscernibility, in this sense.

In dependent type theory, given a dominance ΣΩ\Sigma \subseteq \Omega, let 𝒪(A)\mathcal{O}(A) denote the type of Σ\Sigma-open sets of the type AA, the type of functions AΣA \to \Sigma. The T 1T_1-separation axiom for type AA is given by the dependent function

T 0: x:A y:A(x= Ay)( P:𝒪(A)P(x)P(y))T_0:\prod_{x:A} \prod_{y:A} (x =_A y) \simeq \left(\prod_{P:\mathcal{O}(A)} P(x) \simeq P(y)\right)

Leibniz’s identity of indiscernibles is simply the T 1T_1-separation axiom where the type of all propositions Ω\Omega is the dominance and where the predicates/subsets are the Ω\Omega-open sets.

In addition, given an type universe UU, Leibniz’s identity of indiscernibles for UU is simply the T 1T_1-separation axiom where the type of UU-small propositions Prop U A:UisProp(A)\mathrm{Prop}_U \coloneqq \sum_{A:U} \mathrm{isProp}(A) is the dominance, and where the UU-small predicates/subsets are the Prop U\mathrm{Prop}_U-open sets


Leibniz’s original paragraph (from an unpublished manuscript probably written after 1683) is reproduced in the Latin Original in

  • K. Gerhard (ed.), Section XIX, p. 228 in: Die philosophischen Schriften von Gottfried Wilhelm Leibniz, Siebenter Band, Weidmannsche Buchhandlung (1890) []

and in English translation in:

  • Clarence I. Lewis, Appendix (p. 373) of: A Survey of Symbolic Logic, University of California (1918) [pdf]

and further discussed in:

  • Richard Cartwright, Identity and Substitutivity, p. 119-133 of: Milton Munitz (ed.) Identity and Individuation, New York University Press (1971) [pdf]

  • David Gries, Fred Schneider, Formalizations Of Substitution Of Equals For Equals (1998) [pdf, ecommons:1813/7340

Leibniz’s original terminology “salva veritate” for the substitution principle is prominently used in:

  • W. V. O. Quine, §3 of Two Dogmas of Empiricism and Three grades of modal involvement, as reprinted in: Roger F. Gibson (ed.) Quintessence – Basic readings from the philosophy of W. V. Quine, The Belknap Press of Harvard University Press (2004) [ISBN:9780674027558]

See also:

Formalization in homotopy type theory is in

The understanding of “indiscernibility of identicals” as transport in homotopy type theory is made explicit in:

See also:

Last revised on July 16, 2023 at 21:00:58. See the history of this page for a list of all contributions to it.