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

- Primitive Equality
- _=_

For t,t':T:

- leib(t,t')
- forall P:T->bool. (P(t) implies P(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')

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.