Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* Identity versus equality
@ 2020-05-05  8:47 Ansten Mørch Klev
  2020-05-06 16:02 ` [HoTT] " Joyal, André
  0 siblings, 1 reply; 61+ messages in thread
From: Ansten Mørch Klev @ 2020-05-05  8:47 UTC (permalink / raw)
  To: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 2204 bytes --]

The discussion yesterday provides a good occasion for me to pose a question
I have long wanted to put to this list: is there a convention generally
agreed upon in the HoTT-community for when (if ever) to use 'identity'
instead of 'equality'?

Here are some relevant data.

A Germanic equivalent for 'identity' is 'sameness'.
A Germanic equivalent for 'equality' is 'likeness'.

For Aristotle equality means sameness of quantity. This is how one must
understand 'equal' in Euclid's Elements, where a triangle may have all
sides equal (clearly, they cannot be identical). The axiom in the Elements
that has given rise to the term 'Euclidean relation' and which is appealed
to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.

In Diophantus's Arithmetica, on the other hand, the two terms of an
equation are said to be equal, not identical, and this would become the
standard terminology in algebra. For instance, the sign '=' was introduced
by Robert Recorde as a sign of equality, not as a sign of identity. The
explanation for this apparent discrepancy with the Aristotelian/Euclidean
terminology might be that when dealing with numbers, equality just is
identity, since for two numbers to be identical as to magnitude just is for
them to be the same number. Aristotle says as much in Metaphysics M.7.

Hilbert and Bernays might be one of the few logic books in the modern era
to distinguish equality from identity (volume I, chapter 5). 'Equality' is
there used for any equivalence relation and glossed as the obtaining of
"irgendeine Art von Übereinstimmung". Identity, by contrast, is
"Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility
within the given language.

Frege, by contrast, explicitly identifies (sic!) equality with identity,
and glosses the latter as sameness or coincidence, in the first footnote to
his paper on sense and reference.  Kleene and Church do the same in their
famous textbooks: if one looks under 'identity' in the index to any of
those books one is referred to 'equality'.

Clearly the two cannot be assumed to mean the same by analysts who speak of
two functions being identically equal!

[-- Attachment #2: Type: text/html, Size: 2519 bytes --]

^ permalink raw reply	[flat|nested] 61+ messages in thread

end of thread, other threads:[~2020-05-11 17:27 UTC | newest]

Thread overview: 61+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-05-05  8:47 Identity versus equality Ansten Mørch Klev
2020-05-06 16:02 ` [HoTT] " Joyal, André
2020-05-06 19:01   ` Steve Awodey
2020-05-06 19:18     ` Michael Shulman
2020-05-06 19:31       ` Steve Awodey
2020-05-06 20:30         ` Joyal, André
2020-05-06 22:52         ` Thorsten Altenkirch
2020-05-06 22:54       ` Thorsten Altenkirch
2020-05-06 23:29         ` Joyal, André
2020-05-07  6:11           ` Egbert Rijke
2020-05-07  6:58           ` Thorsten Altenkirch
2020-05-07  9:04             ` Ansten Mørch Klev
2020-05-07 10:09             ` Thomas Streicher
2020-05-07 16:13               ` Joyal, André
2020-05-07 21:41                 ` David Roberts
2020-05-07 23:43                   ` Joyal, André
2020-05-07 23:56                     ` David Roberts
2020-05-08  6:40                       ` Thomas Streicher
2020-05-08 21:06                         ` Joyal, André
2020-05-08 23:44                           ` Steve Awodey
2020-05-09  2:46                             ` Joyal, André
2020-05-09  3:09                               ` Jon Sterling
     [not found]                             ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
2020-05-09  2:50                               ` Steve Awodey
2020-05-09  8:28                           ` Thomas Streicher
2020-05-09 15:53                             ` Joyal, André
2020-05-09 18:43                               ` Thomas Streicher
2020-05-09 20:18                                 ` Joyal, André
2020-05-09 21:27                                   ` Jon Sterling
2020-05-10  2:19                                     ` Joyal, André
2020-05-10  3:04                                       ` Jon Sterling
2020-05-10  9:09                                         ` Thomas Streicher
2020-05-10 11:59                                           ` Thorsten Altenkirch
2020-05-10 11:46                                     ` Thorsten Altenkirch
2020-05-10 14:01                                       ` Michael Shulman
2020-05-10 14:20                                         ` Nicolai Kraus
2020-05-10 14:34                                           ` Michael Shulman
2020-05-10 14:52                                             ` Nicolai Kraus
2020-05-10 15:16                                               ` Michael Shulman
2020-05-10 15:23                                                 ` Nicolai Kraus
2020-05-10 16:13                                                   ` Nicolai Kraus
2020-05-10 16:28                                                     ` Michael Shulman
2020-05-10 18:18                                                       ` Nicolai Kraus
2020-05-10 19:15                                             ` Thorsten Altenkirch
2020-05-10 19:20                                         ` Thorsten Altenkirch
2020-05-10 12:53                                   ` Ulrik Buchholtz
2020-05-10 14:01                                     ` Michael Shulman
2020-05-10 14:27                                       ` Nicolai Kraus
2020-05-10 15:35                                         ` Ulrik Buchholtz
2020-05-10 16:30                                           ` Michael Shulman
2020-05-10 18:56                                           ` Nicolai Kraus
2020-05-10 18:04                                     ` Joyal, André
2020-05-11  7:33                                       ` Thomas Streicher
2020-05-11 14:54                                         ` Joyal, André
2020-05-11 16:37                                           ` stre...
2020-05-11 16:42                                             ` Michael Shulman
2020-05-11 17:27                                               ` Thomas Streicher
2020-05-10 16:51                                   ` Nicolai Kraus
2020-05-10 18:57                                     ` Michael Shulman
2020-05-10 19:18                                     ` Nicolai Kraus
2020-05-10 20:22                                       ` Michael Shulman
2020-05-10 22:08                                         ` Joyal, André

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).