eigenvariable conditions, Henkin quantifiers, Inductive proofs, primitive recursive arithmetic, Proof Schema, tableau methods.