Theory KIF-SETS

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

No theories were included by Kif-Sets.

Theories that include Kif-Sets:

    Kif-Ontology
    Kif-Meta
       Configuration-Design
          Vt-Design
             Simple-Bikes
             Vt-Domain
                Vt-Example
       Kif-Ontology
    Kif-Relations
       Frame-Ontology
          Vt-Domain ...
          Configuration-Design ...
          Physical-Quantities
             Unary-Scalar-Functions
                Cml
                   Thermodynamics
                   Dme
                      Thermodynamics
             Standard-Units
                Simple-Bikes
                Cml ...
                Vt-Design ...
                Unary-Scalar-Functions ...
             Scalar-Quantities
                Vt-Design ...
                Vector-Quantities
          Abstract-Algebra
             Physical-Quantities ...
          Jat-Generic
             Job-Assignment-Task
          Generic-Bibliography
          Slot-Constraint-Sugar
             Generic-Bibliography
       Kif-Ontology

10 classes defined:

    Bounded
    Empty
    Individual
    Mutually-Disjoint
    Pairwise-Disjoint
    Set
       Simple-Set
       Proper-Set
       Finite-Set
    Unbounded

8 relations defined:

8 functions defined:

8 instances defined:

The following constants were used from theories not included:

All constants that were mentioned were defined.

Class SET

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}

Class BOUNDED

Something that can be a member of a set.
Axioms:
(<=> (Bounded ?X) 
     (Forall (?Bounded-Object) 
             (Member ?X (Setofall ?Bounded-Object True)) ))

Class UNBOUNDED

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)))

Relation MEMBER

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

Function SETOF

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))

Sentence EXTENSIONALITY-PROPERTY-OF-SETS

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) ))

Class INDIVIDUAL

An individual is something that is not a set.
Axioms:
(<=> (Individual ?X) (Not (Set ?X)))

Class SIMPLE-SET

A simple set is a set that can be a member of another set.
Subclass-Of: Set

Class PROPER-SET

A proper set is a set that cannot be a member of another set.
Subclass-Of: Set

Class EMPTY

True of the empty set.
Axioms:
(<=> (Empty ?X) (= ?X (Setof)))

Function CARDINALITY

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) ))))

Class FINITE-SET

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))) ))

Function UNION

Range: Set
Axioms:
(Undefined (Arity Union)) 

(Undefined (Arity Union))

Function INTERSECTION

Range: Set
Axioms:
(Undefined (Arity Intersection)) 

(Undefined (Arity Intersection))

Function DIFFERENCE

Axioms:
(Undefined (Arity Difference)) 

(Nth-Domain Difference 3 Set) 

(Nth-Domain Difference 1 Set) 

(Undefined (Arity Difference))

Function COMPLEMENT

Arity: 2
Domain: Set
Range: Set
Axioms:
(= (Complement ?S) (Setofall ?X (Not (Member ?X ?S))))

Function GENERALIZED-UNION

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))) )

Function GENERALIZED-INTERSECTION

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))) )

Relation SUBSET

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))) ))

Relation PROPER-SUBSET

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))) )

Relation DISJOINT

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)))

Relation PAIRWISE-DISJOINT

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)) )))

Relation MUTUALLY-DISJOINT

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)))

Relation SET-PARTITION

Axioms:
(Undefined (Arity Set-Partition)) 

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

Relation SET-COVER

Axioms:
(Undefined (Arity Set-Cover)) 

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

Sentence AXIOM-OF-REGULARITY

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))) ))

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) ))))))

Sentence FINITE-SET-AXIOM

Any finite set of bounded sets is itself a bounded set.
Instance-Of: Sentence
Defining-Axiom: 
'(=> (Finite-Set ?S) (Bounded ?S))

Sentence SUBSET-AXIOM

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))))

Sentence UNION-AXIOM

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

Sentence 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.
Instance-Of: Sentence
Defining-Axiom: 
'(=> (And (Bounded ?U) (Set ?S)) (Bounded (Intersection ?U ?S)))

Sentence 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.
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) ))))))

Relation =

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

Arity: 2

Relation /=

/= means not equal. It is a KIF operator.
Arity: 2
Axioms:
(<=> (/= ?X ?Y) (Not (= ?X ?Y)))

This document was generated using Ontolingua.
Formatting and translation code was written by
François Gerbaux and Tom Gruber