Extensionality elimination

[gebner]

The principle of function extensionality states that pointwise equal functions are equal, that is, they can be used interchangeably. This can simplify proofs considerably since we do not need to prove congruence with regard to the extensional equality.

∀f ∀g (∀x (f x = g x) → f = g)

A similar principle is propositional extensionality: two equivalent propositions (values of type o) are equal, that is, ∀p ∀q ((p ↔ q) → p = q).

However neither propositional nor function extensionality is provable in pure higher-order logic (say, LK with higher-order quantifier rules). Fortunately, we can eliminate both propositional and function extensionality from proofs of second-order statements. The general idea is that we equip every type with a (partial) equivalence relation that expresses the appropriate (extensional) equality for that type. In the literature, this is sometimes called a setoid model [1].

This partial equivalence relation ≈ is defined by recursion on the type, where i is a base type:

p ≈{o} q  :=  p ↔ q
x ≈{i} y  :=  x = y
f ≈{?a>?b} g  :=  ∀x ∀y (x ≈{?a} y  →  f x ≈{?b} g y)

Basic properties:

1. ≈ is a partial equivalence relation (that is, transitive and symmetric).
2. x ≈ x is valid for first-order functions and predicates as well as propositional connectives.

We can now define a expression translation as follows (the other cases just recurse):

〖∀x φ〗  :=  ∀x (x ≈ x → 〖φ〗)
〖∃x φ〗  :=  ∃x (x ≈ x ∧ 〖φ〗)
〖x = y〗 :=  x ≈ y

The main property here is that whenever funext, ..., funext, propext ⊢ φ is provable, then f ≈ f, ..., x ≈ x ⊢ 〖φ〗 is already provable, where f ≈ f, ..., x ≈ x ranges over all constants and free variables in φ. If φ is second-order, then from some basic properties of ≈ we get that ⊢ φ is provable.

• We can simplify the translation and drop the x ≈ x bound for second-order quantifiers.
• Similarily, we can drop the f ≈ f assumption in the translated proof for (at most) second-order functions f.
• This approach also works for subtypes, quotients, and subquotients.

[1] T. Altenkirch, Extensional equality in intensional type theory, LICS 1999.

[gebner]

See also M. Hofmann's thesis [2], which attributes a similar extensionality elimination to Gandy [3].

[2] M. Hofmann, Extensional concepts in intensional type theory (1995).
[3] R. Gandy. On the axiom of extensionality I, Journal of Symbolic Logic 21 (1956), 36-48.

[gebner]

Further references: Kohlenbach [4, Section 10.4] also describes this translation, and additionally references an exposition by Luckhardt [5, Chapter 2], who in turn additionally cites Takeuti [6] and Schütte [7]

[4] U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics (2008)
[5] H. Luckhardt, Extensional Gödel functional interpretation (1973)
[6] G. Takeuti, On a generalized logic calculus, Japanese Journal of Mathematics 23 (1953), 39-96.
[7] K. Schütte, Grundlagen der Analysis im Rahmen einer einfachen Typenlogik (1966).

[gebner]

Jeremy told me in Oxford that such an elimination was already described in the first version of the Principia Mathematica, but I could not find it after a quick look.