Class INDVAR

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

Slots on this class:

Documentation:

An individual variable in a KIF expression. For every individual variable $nu$, there is an axiom asserting that it is indeed an individual variable. Each such axiom is a defining axiom for the {tt indvar} relation.

Instance-Of: Class

Subclass-Of: Variable

Other Related Axioms:

(Exhaustive-Subclass-Partition Variable (Setof Indvar Seqvar))

(Or (Exists (?T ?P)
            (And (Term ?T)
                 (Sentence ?P)
                 (= ?X (Listof (Quote The) ?T ?P))))
    (Exists (?T ?P)
            (And (Term ?T)
                 (Sentence ?P)
                 (= ?X (Listof (Quote Setofall) ?T ?P))))
    (Exists (?Vlist ?P)
            (And (List ?Vlist)
                 (Sentence ?P)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlistp) (Indvar ?V))
                 (= ?X (Listof (Quote Kappa) ?Vlistp ?P))))
    (Exists (?Vlist ?Sv ?P)
            (And (List ?Vlist)
                 (Seqvar ?Sv)
                 (Sentence ?P)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (= ?X
                    (Listof 'Kappa
                            (Append ?Vlist (Listof ?Sv))
                            ?P))))
    (Exists (?Vlist ?T)
            (And (List ?Vlist)
                 (Term ?T)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlistp) (Indvar ?V))
                 (= ?X (Listof (Quote Lambda) ?Vlistp ?T))))
    (Exists (?Vlist ?Sv ?T)
            (And (List ?Vlist)
                 (Seqvar ?Sv)
                 (Sentence ?T)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (= ?X
                    (Listof 'Lambda
                            (Append ?Vlist (Listof ?Sv))
                            ?T)))))

(<=> (Quanterm ?X)
     (Or (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote The) ?T ?P))))
         (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote Setofall) ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Kappa) ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?P)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append ?Vlist (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List ?Vlist)
                      (Term ?T)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Lambda) ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?T)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append ?Vlist (Listof ?Sv))
                                 ?T))))))

(Or (Exists (?V ?P)
            (And (Indvar ?V)
                 (Sentence ?P)
                 (Or (= ?X (Listof (Quote Forall) ?V ?P))
                     (= ?X (Listof (Quote Exists) ?V ?P)))))
    (Exists (?Vlist ?P)
            (And (List ?Vlist)
                 (Sentence ?P)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (Or (= ?X (Listof (Quote Forall) ?Vlist ?P))
                     (= ?X (Listof (Quote Exists) ?Vlist ?P))))))

(<=> (Quantsent ?X)
     (Or (Exists (?V ?P)
                 (And (Indvar ?V)
                      (Sentence ?P)
                      (Or (= ?X (Listof (Quote Forall) ?V ?P))
                          (= ?X (Listof (Quote Exists) ?V ?P)))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (Or (= ?X (Listof (Quote Forall) ?Vlist ?P))
                          (= ?X (Listof (Quote Exists) ?Vlist ?P)))))))