The First-Order Syntax of Variadic Functions

TL;DR

This paper extends first-order logic to include variadic functions, proving a substitution lemma and demonstrating applications in bounded quantifier elimination and Borel set definability.

Contribution

It introduces a formal framework for variadic functions in first-order logic and proves foundational lemmas for their use.

Findings

Established a substitution lemma for variadic functions

Applied the framework to bounded quantifier elimination

Demonstrated definability results for certain Borel sets

Abstract

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 definability of certain Borel sets.