Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A late-night edit for entertainment – I’ll try to polish it up tomorrow when I am more awake:
I have added a translated original quote from Leibniz, as given by Gries & Schneider 1998:
Two terms are the same (eadem) if one can be substituted for the otherwithout altering the truth of any statement (salva veritate). If we have and , and enters into some true proposition, and the substitution of for wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then and are said to be the same;
Interestingly – and this is what I was searching for – Leibniz ends this paragraph with stating the converse:
conversely, if and are the same, they can be substituted for one another.
I was chasing for a historical reference on this “principle of substitution of equals” (or what do people call it?) since this is the logical seed of path induction.
I’d like to find a more canonical reference. But not tonight.
Sounds like the indiscernibility of identicals. Mike has some remarks here.
Yes, or “principle of substitution” or “substitutivity” seems to be used a lot. I am still looking for a good reference on what Leibniz actually said about this.
By the way, regarding that comment you point to:
Strictly speaking, it is “transport” which is “indiscernibility of identicals”, while path induction is the specialization of that to identifications-of-identifications.
This is why people find the J-rule un-intuitive: The J-rule is really just the intuitively clear Leibniz principle, but specialized to the (evident but) unfamiliar case of identifications-of-identifications!
added pointer to:
have extracted this page:
Interestingly, Leibniz went on to state the “first law of thought” (aka refl). Will add the pointer there, too.
have dug out the original Latin version, as reproduced in
and included a screenshot into the entry (here)
wouldn’t the topological version of identity of indiscernibles simply be the identity of indiscernibles after applying the shape modality in a cohesive homomtopy type theory?
Maybe the question in #7 is referring to the section “In topology”? (Notice that this was added in revision 8 by Daniel Luckhardt, March 2017. By the way, I like the idea of that paragraph, but it leaves some room for clarification and maybe examples.)
The standard shape modality does not capture the point-set-identification/distinction in this paragraph: under shape, all points in one connected component become “identified”.
Instead, if one wants to bring a modality into Daniel’s paragraph, it would be that of “T0-reflection” (Kolmogorov quotient).
Okay, I have added (here) a paragraph with more clarification on this example of “topological discernibility”.
(But I am not invested into this subsection, just adding this for completeness. One could probably say much more here in relation to the topological model of intuitionistic logic.)
I have:
made salva veritate a redirect to this entry
added pointer to
for prominent use of this (Leibniz’s original) term for the substitution principle
added pointer also
(where I found that Quine reference from – interestingly, this and the other Wikipedia entry on Identity of indiscernibles do not currently talk to each other)
Further on ancient history:
It looks like Leibniz’s ~1700 text fails to state the symmetry of his coincidentia (i.e. ). What’s a really early record of somebody making the symmetry of the equality-relation explicit?
1 to 11 of 11