The terminology 'extensionality' and 'extensional equality' seem to be a source of confusion:
| In logic: | extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. Wiki |
| In sets: | two sets are equal if they contain the same elements. |
So it seem that the term can be used for equality of either external properties or internal properties? Although perhaps we can construe all of these things as being external observations as opposed to being defined in an equal way.
Formal Systems
Often, formal systems for mathematics will include axioms designed to capture this principle.
Extensionality and Intensionality
- Extensionality - objects are considered to be equal if they have the same external properties.
- Intensionality - concerned with whether the internal definitions of objects are the same.
In some type theories:
- extension is taken to be the actual thing
- intension is more elusive and described as being the meaning.
This almost seem to reverse the above definitions. So this terminology around the realm of Type theory, logic and set theory seems very hard to tie down.
see
extensional type theory - nCat
intensional type theory - nCat
Extension (predicate logic)
The extension of a predicate – a truth-valued function – is the set of tuples of values that, used as arguments, satisfy the predicate. Such a set of tuples is a relation. - Wiki
Set theory - Axiom of Extensionality
two sets are equal if they contain the same elements.
the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. - Wiki
Function Extensionality
The principle of functional extensionality states that two functions are equal if their values are equal at every argument. - nLab
We now recall the principle of function extensionality in type theory:
Definition 2.1.5 (Function extensionality). The principle of function extensionality
That states is, that we two have functions a map:
f, g : Q
x:A B(x) are equal whenever they are pointwise equal.
Note that function extensionality is not derivable from the rules of standard Martin-Löf
type theory. However, it is derivable from the univalence axiom
