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 On Monday, June 27, 2022 at 5:29:46 PM UTC+2 Roland Coghetto wrote: > 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 > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/08b93cda-2fc0-4cd3-b0b2-f34d0aa74ccan%40googlegroups.com.
