Notions of Leibniz and Extensional Equality

Leibniz Equality,: leib(_,_)
Extensional Equality: ext(_,_)

are special relations in higher-order logic that may differ from the usual

Primitive Equality: _=_

We can define them the following way:

For t,t':T:

leib(t,t'): forall P:T->bool. (P(t) implies P(t'))

For t,t':T->T':

ext(t,t'): forall x:T. (t(x)=t'(x))

From logically strongest to weakest we get:

t=t'
leib(t,t')
ext(t,t')

To get the last implication take P to be lambda z. forall x. (t(x)=z(x)).

If primitive equality is available in the signature and the comprehension, then leib(t,t') also implies t=t'. To get this take P to be lambda z. (t=z).

Note that the whole thing is actually far more complicated. If you really want to get confused, have a look at the wonderful paper "Higher Order Semantics and Extensionality" in Chris' publications.
For example, we have implicitly assumed here that the type bool is non-trivial and satisfies tertium non datur, i.e. that our logic is two-valued. This implies that leib(_,_) is symmetric: From leib(t,t') we get (setting P to not Q), forall Q. (not Q(t) implies not Q(t')) and then its contrapositive forall Q. (not not Q(t') implies not not Q(t)). But in general only in classical logic we get forall Q. (Q(t') implies Q(t)), which means leib(t',t).

This is file p/eq2.html on Claus-Peter Wirth's web site.
Last modified 2004/06/21/20.27.