[CakeML] Set theory axioms

[Konrad Slind]

Looks nice! Note that Michael has done an extensive development of the
ordinals in

  <holdir>/examples/set-theory/hol_sets

and transfinite induction is in there somewhere.

Konrad.


On Wed, Jun 29, 2016 at 5:09 PM, Peter Vincent Homeier <
palantir at trustworthytools.com> wrote:

> I've just made my first contribution to CakeML. This consists of two files
> within the subdirectory "flame/set-theory", which are modified versions of
> the corresponding files under "candle/set-theory".
>
> My primary reference for this work was "Set Theory, The Third Millennium
> Edition" by Thomas Jech, Springer, 2006.
>
> These files extend the existing specification of set theory to full ZFC.
> This includes two axioms that were previously omitted, the Axiom of
> Regularity and the Axiom Schema of Replacement:
>
> val regular_def = Define`
>   regular ^mem ⇔ ∀x. (∃y. mem y x) ⇒ ∃y. mem y x ∧ ∀z. ~(mem z x ∧ mem z
> y)`
>
> val is_functional_def = Define`
>   is_functional (R:'a -> 'b -> bool) ⇔ ∀x y z. R x y ∧ R x z ⇒ y = z`
>
> val replacement_def = Define`
>   replacement ^mem ⇔
>       ∀R. is_functional R ⇒
>           ∀d. ∃r. ∀y. mem y r ⇔ ∃x. mem x d ∧ R x y`
>
> val is_set_theory_def = Define`
>   is_set_theory ^mem ⇔
>     extensional mem ∧
>     (∃sub. is_separation mem sub) ∧
>     (∃power. is_power mem power) ∧
>     (∃union. is_union mem union) ∧
>     (∃upair. is_upair mem upair) ∧
>     regular mem ∧
>     replacement mem`
>
> In addition, I have modified the Axiom of Infinity,
>
> val is_infinite_def = Define`
>   is_infinite ^mem s = INFINITE {a | a <: s}`
>
> not really deleting it, but replacing it by the inductive property, taken
> from page 12 of "Set Theory, The Third Millennium Edition" by Thomas Jech,
> Springer, 2006, using the successor operator as defined (Definition 1.20)
> on page 19 of "Introduction to Set Theory" by J. Donald Monk, McGraw Hill,
> 1969.
>
> val suc_def = Define`
>   suc ^mem x = x ∪ Unit x`
>
> val _ = Parse.overload_on("Suc",``suc ^mem``)
>
> val is_inductive_def = Define`
>   is_inductive ^mem s ⇔
>       ∅ <: s ∧ ∀x. x <: s ⇒ Suc x <: s`
>
> val is_model_def = Define`
>   is_model ^s ⇔
>     is_set_theory mem ∧
>     is_inductive mem indset ∧
>     is_choice mem ch`
>
> There is included a proof that the inductive axiom implies the prior
> infinity axiom; this proof depends on the Axiom of Regularity.
>
>     inductive_set_infinite
>       |- is_set_theory mem ∧ is_inductive mem indset ⇒
>          is_infinite mem indset
>
> I also added several new set theory constants, such as binary
> intersection, inverse of a function, image of a function on a set,
> dependent function space, and dependent product space. The last three
> required the Axiom Schema of Replacement to define.
>
> I am hoping to stimulate some discussion and debate. It is necessary to
> extend the existing partial specification of set theory to support the
> construction of the set-theory model of HOL-Omega. Besides that, there will
> probably be other uses for ZFC set theory, and I felt we needed a more
> complete axiomatic basis.
>
> The next steps would presumably be the definition of the ordinals, with
> transfinite induction, and the cardinals.
>
> Enjoy, and please let me know what you think.
>
> Peter
>
>
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160629/4f602953/attachment.html>