equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
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).
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 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.
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.
Leibniz’s original paragraph (from an unpublished manuscript probably written after 1683) is reproduced in the Latin Original in
and in English translation in:
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:
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:
Last revised on September 25, 2022 at 08:48:47. See the history of this page for a list of all contributions to it.