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.
(<=> (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)))))) (<=> (Quantsent ?X) (Or (Exists (?V ?P) (And (Indvar ?V) (Sentence ?P) (Or (= ?X (Listof 'Forall ?V ?P)) (= ?X (Listof 'Exists ?V ?P))))) (Exists (?Vlist ?P) (And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1) (=> (Item ?V ?Vlist) (Indvar ?V)) (Or (= ?X (Listof 'Forall ?Vlist ?P)) (= ?X (Listof 'Exists ?Vlist ?P)))))))