;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; If you load this file (with translation into the "KIF" implementation;;; -- the default ), then the definitions are saved on property lists;;; and can be used for online documentation and in cross-reference reports.(in-package "ONTOLINGUA-USER") ;inherits from the KIF package;all constants defined here are exported;from the KIF package.(define-theoryKIF-SETS() "The KIF vocabulary for set theory as defined in the KIF 3.0 specification." :issues ((:source "KIF Version 3.0 Specification"))) (in-theory 'kif-sets) (define-relationSET(?x) "A set is a collection of objects, both individuals and sets of various sorts. It is a KIF primitive." :issues ((:source "KIF Version 3.0 Specification"))) (define-relationINDIVIDUAL(?x) "An individual is something that is not a set." :iff-def (not (set ?x)) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationBOUNDED(?x) "Something is bounded if it can be a member of a set. This is a KIF primitive." :issues ((:source "KIF Version 3.0 Specification"))) (define-relationUNBOUNDED(?x) "Something in the universe of discourse that can't be a member of a set. Paradoxical beasts go here." :iff-def (not (bounded ?x)) :issues ((:source "KIF Version 3.0 Specification") "It would seem that the extension of this relation is empty, since there can exist no set containing any unbounded things.")) (define-classSIMPLE-SET(?x) "A simple set is a set that can be a member of another set." :iff-def (and (set ?x) (bounded ?x)) :constraints (thing ?x) :issues ("The constraint that simple-set is a subclass-of thing is specified as part of the definition of THING, but it needs to be here, too, for bootstrapping reasons." (:source "KIF Version 3.0 Specification"))) (define-classPROPER-SET(?x) "A proper set is a set that cannot be a member of another set." :def (set ?x) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationMEMBER(?element ?set) "The sentence {\tt (member $\tau_1$ $\tau_2$)} is true if and only if the object denoted by $\tau_1$ is contained in the set denoted by $\tau_2$. As mentioned above, an object can be a member of another object if and only if the former is bounded and the latter is a set." :def (and (bounded ?element) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionSETOF(@members) :-> ?set "SETOF is the set constructor function for KIF. It takes any finite number of arguments and denotes the set of those things." :def (simple-set ?set) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomEXTENSIONALITY-PROPERTY-OF-SETS"Two sets are identical if and only if they have the same members." := (=> (and (set ?s1) (set ?s2)) (<=>(forall (?x) (<=>(member ?x ?s1) (member ?x ?s2))) (= ?s1 ?s2))) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationEMPTY(?x) "True of the empty set." :iff-def (= ?x (setof)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionUNION(@sets) :-> ?set :lambda-body (setofall ?x (exists ?s (and (item ?s (listof @sets)) (member ?x ?s)))) :def (and (=> (item ?s (listof @sets)) (set ?s)) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionINTERSECTION(@sets) :-> ?set :lambda-body (setofall ?x (exists ?s (=> (item ?s (listof @sets)) (member ?x ?s)))) :def (and (=> (item ?s (listof @sets)) (set ?s)) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionDIFFERENCE(?set @sets) :-> ?diff-set :lambda-body (setofall ?x (and (member ?x ?set) (forall ?s (=> (item ?s (listof @sets)) (not (member ?x ?s)))))) :def (and (=> (item ?s (listof @sets)) (set ?s)) (set ?set) (set ?diff-set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionCOMPLEMENT(?s) :-> ?set :lambda-body (setofall ?x (not (member ?x ?s))) :def (and (set ?s) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionGENERALIZED-UNION(?set-of-sets) :-> ?set :lambda-body (setofall ?x (exists (?s) (and (member ?s ?set-of-sets) (member ?x ?s)))) :def (and (set ?set-of-sets) (forall (?s) (=> (member ?s ?set-of-sets) (simple-set ?s))) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-functionGENERALIZED-INTERSECTION(?set-of-sets) :-> ?set :lambda-body (setofall ?x (exists (?s) (=> (member ?s ?set-of-sets) (member ?x ?s)))) :def (and (set ?set-of-sets) (forall (?s) (=> (member ?s ?set-of-sets) (simple-set ?s))) (set ?set)) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationSUBSET(?s1 ?s2) "The sentence {\tt (subset $\tau_1$ $\tau_2$)} is true if and only if $\tau_1$ and $\tau_2$ are sets and the objects in the set denoted by $\tau_1$ are contained in the set denoted by $\tau_2$." :iff-def (and (set ?s1) (set ?s2) (forall ?x (=> (member ?x ?s1) (member ?x ?s2)))) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationPROPER-SUBSET(?s1 ?s2) "The sentence {\tt (proper-subset $\tau_1$ $\tau_2$)} is true if the set denoted by $\tau_1$ is a subset of the set denoted by $\tau_2$ but not vice-versa." :iff-def (and (subset ?s1 ?s2) (not (subset ?s2 ?s1))) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationDISJOINT(?s1 ?s2) "Two sets are disjoint if and only if there is no object that is a member of both sets." :iff-def (empty (intersection ?s1 ?s2)) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationPAIRWISE-DISJOINT(@sets) "Sets are pairwise-disjoint if and only if every set is disjoint from every other set." :iff-def (forall (?s1 ?s2) (=> (item ?s1 (listof @sets)) (item ?s2 (listof @sets)) (or (= ?s1 ?s2) (disjoint ?s1 ?s2)))) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationMUTUALLY-DISJOINT(@sets) "Sets are mutually-disjoint if and only if there is no object that is a member of all of the sets." :iff-def (empty (intersection @sets)) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationSET-PARTITION(?s @sets) :iff-def (and (= ?s (union @sets)) (pairwise-disjoint @sets)) :issues ((:source "KIF Version 3.0 Specification"))) (define-relationSET-COVER(?s @sets) :iff-def (subset ?s (union @sets)) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomAXIOM-OF-REGULARITY"every non-empty set has an element with which it has no members in common." := (forall (?s) (=> (not (empty ?s)) (exists (?u) (and (member ?u ?s) (disjoint ?u ?s))))) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomAXIOM-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." := (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))))))) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomFINITE-SET-AXIOM"Any finite set of bounded sets is itself a bounded set." := (=> (finite-set ?s) (bounded ?s)) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomSUBSET-AXIOM"The set of all of subsets of a bounded set is also a bounded set." := (=> (bounded ?v) (bounded (setofall ?u (subset ?u ?v)))) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomUNION-AXIOM:= (=> (and (bounded ?u) (forall (?x) (=> (member ?x ?u) (bounded ?x)))) (bounded (generalized-union ?u))) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomINTERSECTION-AXIOM"The intersection of a bounded set and any other set is a bounded set. So long as one of the sets defining the intersection is bounded, the resulting set is bounded." := (=> (and (bounded ?u) (set ?s)) (bounded (intersection ?u ?s))) :issues ((:source "KIF Version 3.0 Specification"))) (define-axiomAXIOM-OF-INFINITY"There is a bounded set containing a set, a set that properly contains that set, a third set that properly contains the second set, and so forth. In short, there is at least one bounded set of infinite cardinality." := (exists (?u) (and (bounded ?u) (not (empty ?u)) (forall (?x) (=> (member ?x ?u) (exists (?y) (and (member ?y ?u) (proper-subset ?x ?y))))))) :issues ((:source "KIF Version 3.0 Specification"))) (define-relation=(?x ?y) "= is the equality relation for KIF. It is defined as an operator, but is in practice like every other relation. Two things are = to each other if they are exactly the same thing. How these two things are denoted in some theory is an entirely different issue. = is an operator in KIF." :issues ((:source "KIF Version 3.0 Specification") "Equality is built in to KIF; = and /= are operators. However, it helps to have them be proper relations in the ontology. For instance, other relations may be subsumed by them in a taxonomy." (:see-also /=) "We put the equality relations in the SET ontology, because it is the most primitive ontology in KIF and equality is intrinsic to the definition of set membership.")) (define-relation/=(?x ?y) "/= means not equal. It is a KIF operator." :iff-def (not (= ?x ?y)) :issues ((:source "KIF Version 3.0 Specification") (:see-also =)))