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 P and Q, and P enters into some true proposition, and the substitution of Q for P wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then P and Q 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 P and Q 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.
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. A=B⇔A=B). What’s a really early record of somebody making the symmetry of the equality-relation explicit?
1 to 11 of 11