The First-Order Syntax of Variadic Functions

Samuel Alexander

We extend first-order logic to include variadic function symbols, and prove a substitution lemma. Two applications are given: one to bounded quantifier elimination and one to the d…