David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 55 (1):129 - 179 (1995)
Theabstract variable binding calculus (VB-calculus) provides a formal frame-work encompassing such diverse variable-binding phenomena as lambda abstraction, Riemann integration, existential and universal quantification (in both classical and nonclassical 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-calculus by a natural coordinatization process. This theorem is a generalization of the functional representation 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 precisely, we prove that, for every VB-theory T that is obtained by adjoining new equations to the axioms of the VB-calculus, there exists a model D such that T 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 quantifierexists uncountably many and a fragment of Riemann integration.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Helena Rasiowa (1974). An Algebraic Approach to Non-Classical Logics. Warszawa,Pwn - Polish Scientific Publishers.
Helena Rasiowa (1963). The Mathematics of Metamathematics. Warszawa, Państwowe Wydawn. Naukowe.
Jerzy Kotas & August Pieczkowski (1966). On a Generalized Cylindrical Algebra and Intuitionistic Logic. Studia Logica 18 (1):73 - 81.
W. J. Blok & Don Pigozzi (1989). Algebraizable Logics. Monograph Collection (Matt - Pseudo).
Citations of this work BETA
No citations found.
Similar books and articles
M. W. Bunder (1979). Variable Binding Term Operators in $\Lambda $-Calculus. Notre Dame Journal of Formal Logic 20 (4):876-878.
Steve Awodey (2000). Topological Representation of the Lambda-Calculus. Mathematical Structures in Computer Science 10 (1):81-96.
H. P. Barendregt (1984). The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co..
Luca Alberucci & Alessandro Facchini (2009). On Modal Μ -Calculus and Gödel-Löb Logic. Studia Logica 91 (2):145 - 169.
Chris Hankin (1994). Lambda Calculi: A Guide for the Perplexed. Oxford University Press.
Dexter Kozen (1988). A Finite Model Theorem for the Propositional Μ-Calculus. Studia Logica 47 (3):233 - 241.
Georg Moser & Richard Zach (2006). The Epsilon Calculus and Herbrand Complexity. Studia Logica 82 (1):133 - 155.
Edward N. Zalta (1997). The Modal Object Calculus and its Interpretation. In M. de Rijke (ed.), Advances in Intensional Logic. Kluwer 249--279.
René David & Walter Py (2001). -Calculus and Böhm's Theorem. Journal of Symbolic Logic 66 (1):407-413.
Added to index2009-01-28
Total downloads21 ( #222,398 of 1,940,981 )
Recent downloads (6 months)5 ( #197,910 of 1,940,981 )
How can I increase my downloads?