[CakeML] Set theory axioms

[Peter Vincent Homeier]

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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160629/8daaea28/attachment.html>