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