Editing Extensionality

{{short description|Logic principle}}
{{no footnotes|date=February 2024}}
In [[logic]], '''extensionality''', or '''extensional equality''', refers to principles that judge objects to be [[equality (mathematics)|equal]] if they have the same external properties. It stands in contrast to the concept of [[intensionality]], which is concerned with whether the internal definitions of objects are the same.
==In mathematics==
The extensional definition of function equality, discussed above, is commonly used in mathematics.
A similar extensional definition is usually employed for [[relation (mathematics)|relations]]: two relations are said to be equal if they have the same [[Extension (predicate logic)|extensions]].

In [[set theory]], the [[axiom of extensionality]] states that two [[set (mathematics)|sets]] are equal if and only if they contain the same elements.  In mathematics formalized in set theory, it is common to identify relations&mdash;and, most importantly, [[function (mathematics)|functions]]&mdash;with their extension as stated above, so that it is impossible for two relations or functions with the same extension to be distinguished.

Other mathematical objects are also constructed in such a way that the intuitive notion of "equality" agrees with set-level extensional equality; thus, equal [[ordered pair]]s have equal elements, and elements of a set which are related by an [[equivalence relation]] belong to the same [[equivalence class]].

[[Type theory|Type-theoretical]] foundations of mathematics are generally ''not'' extensional in this sense, and [[setoid]]s are commonly used to maintain a difference between intensional equality and a more general equivalence relation (which generally has poor [[constructivism (mathematics)|constructibility]] or [[Decidability (logic)|decidability]] properties).

==Extensionality principles==
There are various extensionality principles in mathematics. 
* '''Propositional extensionality''' of predicates <math>P,Q</math>: if <math>P\iff Q</math> then <math>P = Q</math>
* '''Functional extensionality''' of functions <math>f,g</math>: if <math>\forall x, f x = g x</math> then <math>f = g</math>
* '''Univalence''' of types <math>A</math>, <math>B</math>:<ref name=HoTTBook>{{cite book | url=https://books.google.com/books?id=LkDUKMv3yp0C | title=Homotopy Type Theory: Univalent Foundations of Mathematics | author=The Univalent Foundations Program | publisher=[[Institute for Advanced Study]] | location=Princeton, NJ | year=2013 | mr=3204653}} </ref>{{rp|2.10}} if  <math>A\simeq B</math> then <math>A = B</math>, where <math>\simeq</math> denotes homotopy equivalence. 
Depending on the chosen foundation, some extensionality principles may imply another. For example it is well known that in [[univalent foundations]], the univalence axiom implies both propositional and functional extensionality. Extensionality principles are usually assumed as axioms, especially in type theories where computational content must be preserved. However, in set theory and other extensional foundations, functional extensionality can be proven to hold by default.

==Example==

Consider the two [[function (mathematics)|functions]] ''f'' and ''g'' mapping from and to [[natural number]]s, defined as follows:
* To find ''f''(''n''), first add 5 to ''n'', then multiply by 2.
* To find ''g''(''n''), first multiply ''n'' by  2, then add 10. 

These functions are extensionally equal; given the same input, both functions always produce the same value. But the definitions of the functions are not equal, and in that intensional sense the functions are not the same. 

Similarly, in natural language there are many predicates (relations) that are intensionally different but are extensionally identical. For example, suppose that a village has just one person named Joe, who is also the oldest person in the village. Then, the two predicates "being called Joe", and "being the oldest person" are intensionally distinct, but extensionally equal for the (current) population of this village.

==See also==
*[[Identity of indiscernibles]]
*[[Univalence axiom]]
*[[Type theory]]

== Notes ==
{{reflist}}
==References==
* {{Cite journal |last=Marcus |first=Ruth Barcan |author-link=Ruth Barcan Marcus |date=January 1960 |title=Extensionality |url=https://www.jstor.org/stable/2251588 |jstor=2251588|journal=[[Mind (journal)|Mind]] |volume=69 |issue=273 |pages=55–62 |doi=10.1093/mind/LXIX.273.55 |issn=0026-4423 }}
* {{Cite journal |last=Sagi |first=Gil |date=29 May 2017 |title=Extensionality and logicality |url=https://link.springer.com/article/10.1007/s11229-017-1447-3 |journal=[[Synthese]] |language=en |volume=198 |issue=5 |pages=1095–1119 |doi=10.1007/s11229-017-1447-3 |issn=1573-0964 |archive-url=https://epub.ub.uni-muenchen.de/41348/ |archive-date=6 Dec 2017}}
* {{Cite book |last=Carnap |first=Rudolf |url=https://archive.org/details/bwb_T2-DWG-016 |title=Formalization of Logic |publisher=[[Harvard University Press]] |year=1943 |series=Studies in Semantics |volume=II}}
* [https://plato.stanford.edu/entries/logic-intensional/ Intensional Logic (Stanford Encyclopedia of Philosophy)]
* [[nlab:equality|equality]] in [[nLab]]

{{Mathematical logic}}

[[Category:Set theory]]
[[Category:Concepts in logic]]
[[Category:Equivalence (mathematics)]]