Sentence AXIOM-OF-CHOICE

There is a set that associates every bounded set with a distinguished element of that set. In effect, it {it chooses} an element from every bounded set.

Instance-Of: Sentence

Defining-Axiom:

'(Exists (?S)
         (And (Set ?S)
              (Forall (?X) (=> (Member ?X ?S) (Double ?X)))
              (Forall (?X ?Y ?Z)
                      (=> (And (Member (Listof ?X ?Y) ?S)
                               (Member (Listof ?X ?Z) ?S))
                          (= ?Y ?Z)))
              (Forall (?U)
                      (=> (And (Bounded ?U) (Not (Empty ?U)))
                          (Exists (?V)
                                  (And (Member ?V ?U)
                                       (Member (Listof ?U ?V) ?S)))))))

• Defined in theory: Kif-sets
• Source code: kif-sets.lisp