Thank you both for your response. I understand a little better. RC
Le mercredi 29 juin 2022 à 01:28:22 UTC+2, [email protected] a écrit : > 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. > > On Tue, Jun 28, 2022 at 2:05 PM Benoit <[email protected]> wrote: > >> 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 >> >> <https://groups.google.com/d/msgid/metamath/08b93cda-2fc0-4cd3-b0b2-f34d0aa74ccan%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/c50bae1a-9f93-4d3b-8f58-0d3f9c7031b6n%40googlegroups.com.
