Function Projection

Arity: 3
Documentation:
The projection of an N-ary relation on column i is the class whose instances are the ith items of each tuple in the relation.
Instance-Of: Function, Relation, Set

Equivalence Axioms for Projection:

(<=> (Projection ?Relation ?Column)
     (And (Defined (Arity ?Relation))
          (Positive-Integer ?Column)
          (=< ?Column (Arity ?Relation))
          (Class ?Projection-Relation)
          (Forall (?Projection-Instance)
                  (<=> (Instance-Of ?Instance ?Projection-Relation)
                       (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (= (Nth ?Tuple ?Column)
                                       ?Instance)))))))


Axioms for Projection:

(Nth-Domain Projection 3 Class)

(Nth-Domain Projection 2 Positive-Integer)


Implication Axioms mentioning Projection:

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Forall (?Projection-Instance)
            (<=> (Instance-Of ?Instance ?Projection-Relation)
                 (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (= (Nth ?Tuple ?Column) ?Instance))))))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Class ?Projection-Relation))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (=< ?Column (Arity ?Relation)))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Positive-Integer ?Column))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Defined (Arity ?Relation)))