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