The KIF vocabulary for set theory as defined in the KIF 3.0 specification.

**Last modified:***Monday, 13 December 1993***Source code: kif-ontology.lisp****List of other known theories**

**No theories were included by Kif-Sets.**

Kif-OntologyKif-MetaConfiguration-DesignVt-DesignSimple-BikesVt-DomainVt-ExampleKif-OntologyKif-RelationsFrame-OntologyVt-Domain...Configuration-Design...Physical-QuantitiesUnary-Scalar-FunctionsCmlThermodynamicsDmeThermodynamicsStandard-UnitsSimple-BikesCml...Vt-Design...Unary-Scalar-Functions...Scalar-QuantitiesVt-Design...Vector-QuantitiesAbstract-AlgebraPhysical-Quantities...Jat-GenericJob-Assignment-TaskGeneric-BibliographySlot-Constraint-SugarGeneric-BibliographyKif-Ontology

BoundedEmptyIndividualMutually-DisjointPairwise-DisjointSetSimple-SetProper-SetFinite-SetUnbounded

**Cardinality****Complement****Difference****Generalized-Intersection****Generalized-Union****Intersection****Setof****Union**

**Axiom-Of-Choice****Axiom-Of-Infinity****Axiom-Of-Regularity****Extensionality-Property-Of-Sets****Finite-Set-Axiom****Intersection-Axiom****Subset-Axiom****Union-Axiom**

**The following constants were used from theories not included:**

**Arity***defined as a***function***in theory***Frame-Ontology****Class***defined as a***class***in theory***Frame-Ontology****Defining-Axiom***defined as a***relation***in theory***Kif-Meta****Documentation***defined as a***relation***in theory***Frame-Ontology****Domain***defined as a***relation***in theory***Frame-Ontology****Double***defined as a***class***in theory***Kif-Lists****Exhaustive-Subclass-Partition***defined as a***relation***in theory***Frame-Ontology****Function***defined as a***class***in theory***Kif-Relations****Function***defined as a***class***in theory***Frame-Ontology****Integer***defined as a***class***in theory***Kif-Numbers****Item***defined as a***relation***in theory***Kif-Lists****Length***defined as a***function***in theory***Kif-Lists****Nth-Domain***defined as a***relation***in theory***Frame-Ontology****Range***defined as a***relation***in theory***Frame-Ontology****Relation***defined as a***class***in theory***Kif-Relations****Relation***defined as a***class***in theory***Frame-Ontology****Subclass-Of***defined as a***relation***in theory***Frame-Ontology****Subrelation-Of***defined as a***relation***in theory***Frame-Ontology****Undefined***defined as a***class***in theory***Kif-Relations**

**All constants that were mentioned were defined.**

A set is a collection of objects, both individuals and sets of various sorts. It is a KIF primitive.

**Exhaustive-Subclass-Partition:**{Simple-set, Proper-set}

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

Something that can be a member of a set.

**Axioms:**

(<=> (Bounded ?X) (Forall (?Bounded-Object) (Member ?X (Setofall ?Bounded-Object True)) ))

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

Something in the universe of discourse that can't be a member of a set. Paradoxical beasts go here.

**Axioms:**

(<=> (Unbounded ?X) (Not (Bounded ?X)))

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

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.

**Arity:**2**Domain:**Bounded**Range:**Set

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

SETOF is the set constructor function for KIF. It takes any finite number of arguments and denotes the set of those things.

**Range:**Set

**Axioms:**

(Undefined (Arity Setof))

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

Two sets are identical if and only if they have the same members.

**Instance-Of:**Sentence**Defining-Axiom:**'(=> (And (Set ?S1) (Set ?S2)) (<=> (Forall (?X) (<=> (Member ?X ?S1) (Member ?X ?S2))) (= ?S1 ?S2) ))

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

An individual is something that is not a set.

**Axioms:**

(<=> (Individual ?X) (Not (Set ?X)))

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

A simple set is a set that can be a member of another set.

**Subclass-Of:**Set

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

A proper set is a set that cannot be a member of another set.

**Subclass-Of:**Set

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

True of the empty set.

**Axioms:**

(<=> (Empty ?X) (= ?X (Setof)))

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

**Arity:**2**Domain:**Set**Range:**Integer

**Axioms:**

(<=> (Cardinality ?Set ?Integer) (And (Set ?Set) (Integer ?Integer) (Exists (@Elements) (And (= ?Set (Setof @Elements)) (Length (Listof @Elements) ?Integer) ))))

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

A set that has only finite elements

**Subclass-Of:**Set

**Axioms:**

(<=> (Finite-Set ?F-Set) (And (Set ?F-Set) (Exists (@Elements) (= ?F-Set (Setof @Elements))) ))

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

**Range:**Set

**Axioms:**

(Undefined (Arity Union)) (Undefined (Arity Union))

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

**Range:**Set

**Axioms:**

(Undefined (Arity Intersection)) (Undefined (Arity Intersection))

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

**Axioms:**

(Undefined (Arity Difference)) (Nth-Domain Difference 3 Set) (Nth-Domain Difference 1 Set) (Undefined (Arity Difference))

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

**Arity:**2**Domain:**Set**Range:**Set

**Axioms:**

(= (Complement ?S) (Setofall ?X (Not (Member ?X ?S))))

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

**Arity:**2**Domain:**Set**Range:**Set

**Axioms:**

(= (Generalized-Union ?Set-Of-Sets) (Setofall ?X (Exists (?S) (And (Member ?S ?Set-Of-Sets) (Member ?X ?S)) ))) (=> (Generalized-Union ?Set-Of-Sets ?Set) (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Set ?S))) )

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

**Arity:**2**Domain:**Set**Range:**Set

**Axioms:**

(= (Generalized-Intersection ?Set-Of-Sets) (Setofall ?X (Exists (?S) (=> (Member ?S ?Set-Of-Sets) (Member ?X ?S)) ))) (=> (Generalized-Intersection ?Set-Of-Sets ?Set) (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Set ?S))) )

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

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$.

**Arity:**2**Domain:**Set**Range:**Set

**Axioms:**

(<=> (Subset ?S1 ?S2) (And (Set ?S1) (Set ?S2) (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2))) ))

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

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.

**Arity:**2**Subrelation-Of:**Subset

**Axioms:**

(<=> (Proper-Subset ?S1 ?S2) (And (Subset ?S1 ?S2) (Not (Subset ?S2 ?S1))) )

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

Two sets are disjoint if and only if there is no object that is a member of both sets.

**Arity:**2

**Axioms:**

(<=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))

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

Sets are pairwise-disjoint if and only if every set is disjoint from every other set.

**Axioms:**

(Undefined (Arity Pairwise-Disjoint)) (<=> (Pairwise-Disjoint @Sets) (Forall (?S1 ?S2) (=> (Item ?S1 (Listof @Sets)) (Item ?S2 (Listof @Sets)) (Or (= ?S1 ?S2) (Disjoint ?S1 ?S2)) )))

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

Sets are mutually-disjoint if and only if there is no object that is a member of all of the sets.

**Axioms:**

(Undefined (Arity Mutually-Disjoint)) (<=> (Mutually-Disjoint @Sets) (Empty (Intersection @Sets)))

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

**Axioms:**

(Undefined (Arity Set-Partition)) (<=> (Set-Partition ?S @Sets) (And (= ?S (Union @Sets)) (Pairwise-Disjoint @Sets)) )

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

**Axioms:**

(Undefined (Arity Set-Cover)) (<=> (Set-Cover ?S @Sets) (Subset ?S (Union @Sets)))

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

every non-empty set has an element with which it has no members in common.

**Instance-Of:**Sentence**Defining-Axiom:**'(Forall (?S) (=> (Not (Empty ?S)) (Exists (?U) (And (Member ?U ?S) (Disjoint ?U ?S))) ))

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

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-ontology.lisp**

Any finite set of bounded sets is itself a bounded set.

**Instance-Of:**Sentence**Defining-Axiom:**'(=> (Finite-Set ?S) (Bounded ?S))

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

The set of all of subsets of a bounded set is also a bounded set.

**Instance-Of:**Sentence**Defining-Axiom:**'(=> (Bounded ?V) (Bounded (Setofall ?U (Subset ?U ?V))))

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

**Instance-Of:**Sentence**Defining-Axiom:**'(=> (And (Bounded ?U) (Forall (?X) (=> (Member ?X ?U) (Bounded ?X))) ) (Bounded (Generalized-Union ?U)) )

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

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.

**Instance-Of:**Sentence**Defining-Axiom:**'(=> (And (Bounded ?U) (Set ?S)) (Bounded (Intersection ?U ?S)))

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

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.

**Instance-Of:**Sentence**Defining-Axiom:**'(Exists (?U) (And (Bounded ?U) (Not (Empty ?U)) (Forall (?X) (=> (Member ?X ?U) (Exists (?Y) (And (Member ?Y ?U) (Proper-Subset ?X ?Y) ))))))

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

= 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.

**Arity:**2

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

/= means not equal. It is a KIF operator.

**Arity:**2

**Axioms:**

(<=> (/= ?X ?Y) (Not (= ?X ?Y)))

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

Formatting and translation code was written by