A sequence variable in a KIF expression. For every sequence variable $omega$, there is an axiom asserting that it is a sequence variable. Each such axiom is a defining axiom for the {tt seqvar} relation.
(<=> (Quanterm ?X)
(Or (Exists (?T ?P)
(And (Term ?T)
(Sentence ?P)
(= ?X (Listof 'The ?T ?P))))
(Exists (?T ?P)
(And (Term ?T)
(Sentence ?P)
(= ?X (Listof 'Setofall ?T ?P))))
(Exists (?Vlist ?P)
(And (List ?Vlist)
(Sentence ?P)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof '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 '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))))))