ANTONINO SALIBRA The Abstract Variable-binding Calculus*
Don Pigozzi · 1995
The abstract variable binding calculus (VB-catculus) provides a formal frame- work encompassing such diverse variable-binding phenomena as lambda abstraction, Rie- mann integration, existential and universal quantification (in both classical and nonclas- sical logic), and various notions of generalized quantification that have been studied in abstract model theory. All axioms of the VB-calculus are in the form of equations, but like the lambda calculus it :is not a true equational theory since substitution of terms for variables is restricted. A similar problem with the standard formalism of the first-order predicate logic led to the development of the theory of cylindric and polyadic Boolean algebras. We take the same course here and introduce the variety of polyadic VB-algebras as a pure equational form of the VB-calculus. In one of the main results of the paper we show that every locally finite polyadic VB-algebra of infinite dimension is isomorphic to a functional polyadic VB-algebra that is obtained from a model of the VB-calcuhs by a natural coordinatization process. This theorem is a generalization of the functional rep- resentation theorem for polyadic Boolean algebras given by P. Halmos. As an application of this theorem we present a strong completeness theorem for the VB-calculus. More pre- cisely, we prove that, for every VB-theory T that is obtained by adjoining new equations to the axioms of the VB-calcutus, there exists a model D such that b- I- s = t iff ~D s = t. This result specializes to a completeness theorem for a number of familiar systems that can be formalized as VB-calculi. For example, the lambda calculus, the classical first-order predicate calculus, the theory of the generalized quantifier exists uncountably many and a fragment of Riemann integration.