Axiom Axiom-Of-Choice

• Defined in ontology: Kif-sets
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/kif/../../all-ontologies/kif/kif-sets.lisp

Documentation@Ol%Frame-Ontology:

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.

Notes:

• Source: KIF Version 3.0 Specification

Defining axiom of Axiom-Of-Choice:

(Exists (?S)
        (And (Set ?S)
             (Forall (?X)
                     (=> (Member ?X ?S)
                         (Double@Ol-User%Kif-Lists ?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)))))))