Alpha-conversion, conditions on variables and categorical logic
Studia Logica 48 (3):319 - 360 (1989)
| Abstract | We present the paradigm of categories-as-syntax. We briefly recall the even stronger paradigm categories-as-machine-language which led from -calculus to categorical combinators viewed as basic instructions of the Categorical Abstract Machine. We extend the categorical combinators so as to describe the proof theory of first order logic and higher order logic. We do not prove new results: the use of indexed categories and the description of quantifiers as adjoints goes back to Lawvere and has been developed in detail in works of R. Seely. We rather propose a syntactic, equational presentation of those ideas. We sketch the (quasi-equational) categorical structures for dependent types, following ideas of J. Cartmell (contextual categories). All these theories of categorical combinators, together with the translations from -calculi into them, are introduced smoothly, thanks to the systematic use of– - an abstract variable-free notation for -calculus, going back to N. De Bruijn, – - a sequent formulation of the natural deduction. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesGeorge Voutsadakis (2003). Categorical Abstract Algebraic Logic: Equivalent Institutions. Studia Logica 74 (1-2):275 - 311.
Olivier Lessmann (2003). Categoricity and U-Rank in Excellent Classes. Journal of Symbolic Logic 68 (4):1317-1336.
Joel J. Kupperman (2002). A Messy Derivation of the Categorical Imperative. Philosophy 77 (4):485-502.
Walter Baur (1975). ℵ0-Categorical Modules. Journal of Symbolic Logic 40 (2):213 - 220.
Robert Schroer (2010). Is There More Than One Categorical Property? Philosophical Quarterly 60 (241):831-850.
Frances Howard-Snyder (2012). The Power of Logic. Mcgraw-Hill.
Olivier Lessmann (2005). Upward Categoricity From a Successor Cardinal for Tame Abstract Classes with Amalgamation. Journal of Symbolic Logic 70 (2):639 - 660.
Henning Peucker (2012). Husserl's Foundation of the Formal Sciences in His “Logical Investigations”. Axiomathes 22 (1):135-146.
R. A. G. Seely (1987). Categorical Semantics for Higher Order Polymorphic Lambda Calculus. Journal of Symbolic Logic 52 (4):969-989.
Michael Chris Laskowski (1988). Uncountable Theories That Are Categorical in a Higher Power. Journal of Symbolic Logic 53 (2):512-530.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #202,056 of 549,500 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
