- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
On the semantics of the universal quantifier
Annals of Pure and Applied Logic 87 (3):209-239 (1997)
Abstract
We investigate the universal fragment of intuitionistic logic focussing on equality of proofs. We give categorical models for that and prove several completeness results. One of them is a generalization of the well known Yoneda lemma and the other is an extension of Harvey Friedman's completeness result for typed lambda calculusOther Versions
No versions found
My notes
Similar books and articles
On the semantics of the universal quantifier.Djordje Ubri - 1997 - Annals of Pure and Applied Logic 87 (3):209-239.
A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
Continuation-passing style models complete for intuitionistic logic.Danko Ilik - 2013 - Annals of Pure and Applied Logic 164 (6):651-662.
Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms.Yuta Takahashi & Ryo Takemura - 2019 - Journal of Philosophical Logic 48 (3):553-570.
The intuitionistic fragment of computability logic at the propositional level.Giorgi Japaridze - 2007 - Annals of Pure and Applied Logic 147 (3):187-227.
Generalising canonical extension to the categorical setting.Dion Coumans - 2012 - Annals of Pure and Applied Logic 163 (12):1940-1961.
On the Meaning of Logical Completeness.Michele Basaldella & Kazushige Terui - 2010 - Logical Methods in Computer Science 6 (4:11):1–35.
Analytics
Added to PP
2014-01-16
Downloads
26 (#892,543)
6 months
7 (#469,699)
2014-01-16
Downloads
26 (#892,543)
6 months
7 (#469,699)
Historical graph of downloads
Citations of this work
Coherence in linear predicate logic.Kosta Došen & Zoran Petrić - 2009 - Annals of Pure and Applied Logic 158 (1-2):125-153.
References found in this work
Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Fibered categories and the foundations of naive category theory.Jean Bénabou - 1985 - Journal of Symbolic Logic 50 (1):10-37.
Hyperdoctrines, Natural Deduction and the Beck Condition.Robert A. G. Seely - 1983 - Mathematical Logic Quarterly 29 (10):505-542.
The fibrational formulation of intuitionistic predicate logic ${\rm I}$: completeness according to Gödel, Kripke, and Läuchli. I.M. Makkai - 1993 - Notre Dame Journal of Formal Logic 34 (3):334-377.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-8d48cdbf4-jdnsr uwo