nLab identity of indiscernibles

Idea

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 $A$ and $B$, and $A$ enters into some true proposition, and the substitution of $B$ for $A$ wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then $A$ and $B$ 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 $P$ and $Q$ are the same, they can be substituted for one another.

The paragraph ends with the assertion that

$A$ and $A$ 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 homotopy type theory

In type theories with identity types (homotopy type theory), identity of indiscernibles holds trivially because of haecceities?; but 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_0$-separation axiom, hence that it is a Kolmogorov space. Generally, one could regard the $T_0$-reflection as the modality under which identity becomes indiscernibility, in this sense.

Related entries

• first law of thought

• transport

References

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) [archive.org]

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:

• Wikipedia, Identity of indiscernibles

• Wikipedia, Salva veritate

• Standord Encyclopedia of Philosophy, The Identity of Indiscernibles

Formalization in homotopy type theory is in

• Univalent Foundations Project, section 1.12 of Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Favonia, appendix B of Higher-Dimensional Types in the Mechanization of Homotopy Theory, PhD thesis 2017, (pdf)

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

• James Ladyman, Stuart Presnell, §6.3 of: Identity in Homotopy Type Theory, Part I: The Justification of Path Induction, Philosophia Mathematica 23 3 (2015) 386–406 [doi:10.1093/philmat/nkv014, pdf]

• Benedikt Ahrens, Paige Randall North, §3.1 in: Univalent foundations and the equivalence principle, in: Reflections on the Foundations of Mathematics, Synthese Library 407 Springer (2019) [arXiv:2202.01892, doi:10.1007/978-3-030-15655-8]

See also:

• Ladyman & Presnell (2016)