Relation MEMBER

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

Slots on this relation:

Documentation:

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.

Instance-Of: Relation

Arity: 2

Domain: Bounded

Range: Set

Other Related Axioms:

(=> (Member $X $Y) (Set $Y))

(=> (Member $X $Y) (Bounded $X))

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

(<- (Union @Sets)
    (Setofall ?X
              (Exists (?S)
                      (And (Item ?S (Listof @Sets)) (Member ?X ?S)))))

(<- (Intersection @Sets)
    (Setofall ?X
              (Exists (?S)
                      (=> (Item ?S (Listof @Sets)) (Member ?X ?S)))))

(<- (Difference ?Set @Sets)
    (Setofall ?X
              (And (Member ?X ?Set)
                   (Forall (?S)
                           (=> (Item ?S (Listof @Sets))
                               (Not (Member ?X ?S)))))))

(<- (Complement ?S) (Setofall ?X (Not (Member ?X ?S))))

(<- (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) (Simple-Set ?S))))

(<- (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) (Simple-Set ?S))))

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

(Forall (?S)
        (=> (Not (Empty ?S))
            (Exists (?U) (And (Member ?U ?S) (Disjoint ?U ?S)))))

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

(=> (And (Bounded ?U) (Forall (?X) (=> (Member ?X ?U) (Bounded ?X))))
    (Bounded (Generalized-Union ?U)))

(Exists (?U)
        (And (Bounded ?U)
             (Not (Empty ?U))
             (Forall (?X)
                     (=> (Member ?X ?U)
                         (Exists (?Y)
                                 (And (Member ?Y ?U)
                                      (Proper-Subset ?X ?Y)))))))

Notes:

• Source: KIF Version 3.0 Specification