;;; -*- 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-theory KIF-SETS ()
"The KIF vocabulary for set theory as defined in the KIF 3.0
specification.")
(in-theory 'kif-sets)
(define-relation SET (?x)
"A set is a collection of objects, both individuals and sets of
various sorts. It is a KIF primitive."
)
(define-relation INDIVIDUAL (?x)
"An individual is something that is not a set."
:iff-def (not (set ?x)))
(define-relation BOUNDED (?x)
"Something is bounded if it can be a member of a set.
This is a KIF primitive.")
(define-relation UNBOUNDED (?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 ("It would seem that the extension of this relation is empty,
since there can exist no set containing any unbounded things."))
(define-class SIMPLE-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."))
(define-class PROPER-SET (?x)
"A proper set is a set that cannot be a member of another set."
:def (set ?x))
(define-relation MEMBER (?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)))
(define-function SETOF (@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))
(define-axiom EXTENSIONALITY-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))))
(define-relation EMPTY (?x)
"True of the empty set."
:iff-def (= ?x (setof)))
(define-function UNION (@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)))
(define-function INTERSECTION (@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)))
(define-function DIFFERENCE (?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)))
(define-function COMPLEMENT (?s) :-> ?set
:lambda-body (setofall ?x (not (member ?x ?s)))
:def (and (set ?s) (set ?set)))
(define-function GENERALIZED-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)))
(define-function GENERALIZED-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)))
(define-relation SUBSET (?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)))))
(define-relation PROPER-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))))
(define-relation DISJOINT (?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)))
(define-relation PAIRWISE-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)))))
(define-relation MUTUALLY-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)))
(define-relation SET-PARTITION (?s @sets)
:iff-def (and (= ?s (union @sets))
(pairwise-disjoint @sets)))
(define-relation SET-COVER (?s @sets)
:iff-def (subset ?s (union @sets)))
(define-axiom AXIOM-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))))))
(define-axiom 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."
:= (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))))))))
(define-axiom FINITE-SET-AXIOM
"Any finite set of bounded sets is itself a bounded set."
:= (=> (finite-set ?s) (bounded ?s)))
(define-axiom SUBSET-AXIOM
"The set of all of subsets of a bounded set is also a bounded set."
:= (=> (bounded ?v) (bounded (setofall ?u (subset ?u ?v)))))
(define-axiom UNION-AXIOM
:= (=> (and (bounded ?u) (forall (?x) (=> (member ?x ?u) (bounded ?x))))
(bounded (generalized-union ?u))))
(define-axiom INTERSECTION-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))))
(define-axiom AXIOM-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))))))))
(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 ((:see-also /=)
"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."
"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 ((:see-also =)))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber