Extensionality ax-ext axext

[Roland Coghetto]

Hello,

by reading axext (hol.mm theorem - http://us.metamath.org/holuni/axext.html) and ax-ext (axiom set.mm - http://us.metamath.org/mpeuni/ax-ext.html),

ax-ext $a |- ( A. z ( z e. x <-> z e. y ) -> x = y ) $.

$d x y A $. $d x y B $. $d x y al $.
axext.1 $e |- A : ( al -> bool ) $.
axext.2 $e |- B : ( al -> bool ) $.
$( Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It
states that two sets are identical if they contain the same elements.
Axiom Ext of [BellMachover] p. 461. $)
axext $p |- T. |=
[ ( ! x : al . [ ( A x : al ) = ( B x : al ) ] ==> [ A = B ] $=

I have the impression that axext is not quite the HOL version of the extensionality axiom.

Indeed, for me alpha->star is not necessary a set but only a predicate. So alpha->star would not always be a set but it could be a class.

Also, ax-ext uses "=" and axext "<->". Is this difference important?

Most likely, I probably misunderstood one or more concepts.

Your help will be useful.

RC

[Benoit]

I'd be happy to hear from Mario on that, since he's the author of hol.mm.

As for the second question: if you want to use a biconditional, then you need to define it, similar to the definition of "=>" in df-im.  This would be something like

  <=> = \p \q [ p = q ]

and that would expand to the expression used in axext.  So it's not a significant difference.

As for the first question: it looks like one cannot exactly have ZF this way.  In set theory, you forget types.  For instance, ax-inf is stated for the type "ind" of individuals.  For various constructions, you "append a bool": as you saw, extensionality is proved for type (a -> bool) (so it does not apply to individuals? but maybe you can use the canonical embedding of a into ((a -> bool) -> bool) ?).  The power set axiom, starting from a set of type (a -> bool), yields one of type ((a-> bool) -> bool), the axiom of union decrements type, the axiom of replacement uses two different types.  Therefore, every "a" should be thought of as a chain "((ind -> bool) -> ......) -> bool)" ?  This is akin to the type hierarchy of Russell (which is actually the ancestor of hol).  But then, in ZF, you should be able to identify the "same" sets appearing at different levels...

This is a bit like a blind leading a blind... I hope better explanation can be given.

Benoît

[Mario Carneiro]

Note that axext in hol.mm is not an axiom, and also note that not all ZF axioms are present. HOL does not prove ZF, and these are only approximations of the corresponding ZF axioms.

The reason axext is stated with predicates ( al -> bool ) instead of functions ( al -> be ) is because it's supposed to be set extensionality and not function extensionality (which is a HOL axiom). It doesn't use individuals (type al) either because in type theory these don't have an extensionality property at all: they are atoms with no internal structure. At a minimum, we need to have functions in order to apply them in the hypothesis. In the ZF embedding of HOL, these (al -> bool) functions do actually correspond to subsets of the set [al], and function application becomes set membership. (Well, that's one possible translation. The other one maps bool to a two element set, and then these are plain functions. But they are still in bijection with the powerset of [al] in that case.)

Benoit already explained why the biconditional is not used: in HOL systems (maybe not all of them, but HOL light at least), the biconditional *is* the '=' relation at type bool. It just has notation to make it look more arrow-like. We could add a definition for it but it would not really make anything easier.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/08b93cda-2fc0-4cd3-b0b2-f34d0aa74ccan%40googlegroups.com.

[Roland Coghetto]

Thank you both for your response. 

I understand a little better.

RC