Relation =

Slots on this relation:

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

Instance-Of: Relation
Arity: 2

Other Related Axioms:

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

(= ?X (Setof))

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

(=> (= (Union @Sets) ?Set) (=> (Item ?S (Listof @Sets)) (Set ?S)))

(=> (= (Intersection @Sets) ?Set)
    (=> (Item ?S (Listof @Sets)) (Set ?S)))

(=> (= (Difference ?Set @Sets) ?Diff-Set)
    (=> (Item ?S (Listof @Sets)) (Set ?S)))

(=> (= (Generalized-Union ?Set-Of-Sets) ?Set)
    (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set ?S))))

(=> (= (Generalized-Intersection ?Set-Of-Sets) ?Set)
    (Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set ?S))))

(Forall (?S1 ?S2)
        (=> (Item ?S1 (Listof @Sets))
            (Item ?S2 (Listof @Sets))
            (Or (= ?S1 ?S2) (Disjoint ?S1 ?S2))))

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

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

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

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

Notes: