From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a02:58c3:: with SMTP id f186mr2502603jab.120.1588668493818; Tue, 05 May 2020 01:48:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6602:1494:: with SMTP id a20ls538882iow.5.gmail; Tue, 05 May 2020 01:48:12 -0700 (PDT) X-Received: by 2002:a6b:8ecf:: with SMTP id q198mr2239847iod.207.1588668492526; Tue, 05 May 2020 01:48:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588668492; cv=none; d=google.com; s=arc-20160816; b=adrKBY2CJuTR7v2U1ihRiC9yriXnAGTYi2oN71cenuaj+UCiZ7lSK5okN8rXUBNe0t No8su71tqYT5+pmoduq8kub6fSSuAa/bA74rWY5Y0b5cDDE28UXxCUsKjXbkF9mzjklR qnfYJu+6bcD7mLnHM9c5m38u9kUjRiclW1nBW29Z/cdwS6dxiXSnsrdW7+Kz3aKLKM41 O3iGtmHML6+C/tEX5k12R3aOXEm/c1Z+Y3iUVpDWRWaSt12032NTwA0huWsmM/enYQOI E8wSBvGhtcQaw70SVddetXVzWWyf9YgX1X78Wju7ON1BFNMktJhUeI+U7AXn992lZJ+o SZDg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=2A5PP+nZK/Xx6nIpOsd36O64aU3scsFyi393gnRfBnQ=; b=W+TeGdhGXAq1tDR5L3G2hPc6manBkNZ9I+pSgZJYzw2BjQJ96ETpxgi8LX2mpxLUDZ XuxP6bY46B0yb68zRPDFwjmR4lPBuH56ShQtubD7zPmzsznCTKdT6hNdIEF1U8pz2iUt gvoYlVR7ZR4imR/NQawS9EfBjdBLzTtubUQy5j7+9lRRqw4DCnbGd/wEQFoASxWkWI8T 02rLm4SHKfFQbn/dze+5QpGp4F5ChQy4jo+2TY3TaMcyhkOdkg2aImatRgRInectIS04 Jnr3K4WLodPSwSNzngS9+TJIEdGmo3dOkZOIVmJxQ8KK7HlF7IXN+cJDNOWF9eZj+Lgk 1D7w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=mngiVMcU; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::d2c as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-io1-xd2c.google.com (mail-io1-xd2c.google.com. [2607:f8b0:4864:20::d2c]) by gmr-mx.google.com with ESMTPS id k13si119604ioq.3.2020.05.05.01.48.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 05 May 2020 01:48:12 -0700 (PDT) Received-SPF: pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::d2c as permitted sender) client-ip=2607:f8b0:4864:20::d2c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=mngiVMcU; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:4864:20::d2c as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-io1-xd2c.google.com with SMTP id w11so551877iov.8 for ; Tue, 05 May 2020 01:48:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=2A5PP+nZK/Xx6nIpOsd36O64aU3scsFyi393gnRfBnQ=; b=mngiVMcUNZLpocvV8vrgf/hHcRTmVx74xmgH35tJ/9gdNZqpCb4nY57Ced3EqoPnp7 8GzGTM/KtnPc7uMHIfuG/CUilXlj1zJ+m/ZLOCSOHceLGS5yKhd7UYODzfmVP8akka+d C6q+9l22CGSuFdZG+swqmtPWMpBH8zMyb/GEbCMYFilBpCHGd3JooCzo6eBrTjsC6k3b +Eo8FlWESWOn/ugUHvv5i+MC5g6sAHW4MpcmXdAumGTMPTGt+6TURlZjXW0fUE5lFZGp nsG437oTEnq+6QJJyuW5exlZgG/nRQa4Lc70x+xXKjHh+ju0q5NM3YcwFxbOjmqsuGD5 IgUQ== X-Gm-Message-State: AGi0PuabBAqJuqAZtmzeC/amf5eYn6jRaIQKHtkfa7zKZ0zdN9tWZhdu sIhtsrenNZu0T+mLX2RhSMH5X8AsVG0d2xqQYJaXB+MR X-Received: by 2002:a02:23c1:: with SMTP id u184mr2364840jau.11.1588668492030; Tue, 05 May 2020 01:48:12 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?Q?Ansten_M=C3=B8rch_Klev?= Date: Tue, 5 May 2020 10:47:46 +0200 Message-ID: Subject: Identity versus equality To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000022283a05a4e2b52d" --00000000000022283a05a4e2b52d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 '=3D' was introduce= d 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 =C3=9Cbereinstimmung". Identity, by contrast, is "=C3=9Cbereinstimmung 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! --00000000000022283a05a4e2b52d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The discussion yesterday provides a good occasion=C2=A0for= me=C2=A0to pose a question I have long wanted to put to this list: is ther= e a convention generally agreed upon in the HoTT-community for when (if eve= r) to use 'identity' instead of 'equality'?

=
Here are some relevant data.

A Germanic equiv= alent for 'identity' is 'sameness'.
A Germanic eq= uivalent for 'equality' is 'likeness'.

=
For Aristotle equality means sameness of quantity. This is how one mus= t 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'.=C2=A0

In Diophan= tus'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 termino= logy in algebra. For instance, the sign '=3D' was introduced by Rob= ert Recorde as a sign of equality, not as a sign of identity. The explanati= on for this apparent=C2=A0discrepancy with the Aristotelian/Euclidean termi= nology 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 b= e the same number. Aristotle says as much in Metaphysics M.7.=C2=A0

Hilbert and Bernays might be one of the few logic books i= n the modern era to distinguish equality from identity (volume I, chapter 5= ). 'Equality' is there used for any equivalence relation and glosse= d as the obtaining of "irgendeine Art von =C3=9Cbereinstimmung". = Identity, by contrast, is "=C3=9Cbereinstimmung in jeder Hinsicht"= ;, as expressed by indiscernibility within the given language.=C2=A0
<= div>
Frege, by contrast, explicitly identifies (sic!) equalit= y with identity, and glosses the latter as sameness or coincidence, in the = first footnote to his paper on sense and reference.=C2=A0 Kleene and Church= do the same in their famous textbooks: if one looks under 'identity= 9; in the index to any of those books one is referred to 'equality'= .=C2=A0=C2=A0

Clearly the two cannot be assumed to= mean the same by analysts who speak of two functions being identically equ= al!
--00000000000022283a05a4e2b52d--