A Categorical Interpretation of the Intuitionistic, Typed, First Order Logic with Hilbert’s $${\varepsilon}$$ ε -Terms

Logica Universalis 10 (4):407-418 (2016)
  Copy   BIBTEX

Abstract

We introduce a typed version of the intuitionistic epsilon calculus. We give a categorical semantics of it introducing a class of categories which we call \-categories. We compare our results with earlier ones of Bell :323–337, 1993).

Categories

Keywords

Reprint years

DOI

10.1007/s11787-016-0155-y

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Hilbert’s varepsilon -operator in intuitionistic type theories.John L. Bell - 1993 - Mathematical Logic Quarterly 39 (1):323--337.
The "Relevance" of Intersection and Union Types.Mariangiola Dezani-Ciancaglini, Silvia Ghilezan & Betti Venneri - 1997 - Notre Dame Journal of Formal Logic 38 (2):246-269.
On proof terms and embeddings of classical substructural logics.Ken-Etsu Fujita - 1998 - Studia Logica 61 (2):199-221.
Intuitionistic ε- and τ-calculi.David Devidi - 1995 - Mathematical Logic Quarterly 41 (4):523-546.
On the semantics of the universal quantifier.Djordje Čubrić - 1997 - Annals of Pure and Applied Logic 87 (3):209-239.
Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
Lambda calculus and intuitionistic linear logic.Simona Ronchi della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
Term-Forming Operators in First Order Logic.David Michael Devidi - 1994 - Dissertation, The University of Western Ontario (Canada)
A Concrete Categorical Model for the Lambek Syntactic Calculus.Marcelo Da Silva Corrêa & Edward Hermann Haeusler - 1997 - Mathematical Logic Quarterly 43 (1):49-59.
Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
Intuitionistic completeness for first order classical logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
Epsilon Calculi.Barry Slater - 2006 - Logic Journal of the IGPL 14 (4):535-590.
A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
Negationless intuitionism.Enrico Martino - 1998 - Journal of Philosophical Logic 27 (2):165-177.
The judgement calculus for intuitionistic linear logic: Proof theory and semantics.Silvio Valentini - 1992 - Mathematical Logic Quarterly 38 (1):39-58.

Analytics

Added to PP
2016-10-03

Downloads
19 (#781,160)

6 months
7 (#418,426)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On a Generalization of Equilogical Spaces.Fabio Pasquali - 2018 - Logica Universalis 12 (1-2):129-140.

Add more citations

References found in this work

Epsilon substitution for first- and second-order predicate logic.Grigori Mints - 2013 - Annals of Pure and Applied Logic 164 (6):733-739.
Hilbert’s varepsilon -operator in intuitionistic type theories.John L. Bell - 1993 - Mathematical Logic Quarterly 39 (1):323--337.
Axiom of Choice and Complementation.Radu Diaconescu - 1975 - Proceedings of the American Mathematical Society 51 (1):176-178.

Add more references