On the semantics of the universal quantifier

Annals of Pure and Applied Logic 87 (3):209-239 (1997)
  Copy   BIBTEX

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 calculus.

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(96)00051-6

Links

PhilArchive



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

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

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.
Quantifier Elimination for a Class of Intuitionistic Theories.Ben Ellison, Jonathan Fleischmann, Dan McGinn & Wim Ruitenburg - 2008 - Notre Dame Journal of Formal Logic 49 (3):281-293.
Presuppositions of quantified sentences: experimental data. [REVIEW]Emmanuel Chemla - 2009 - Natural Language Semantics 17 (4):299-340.
Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
Decidability of ∀*∀‐Sentences in Membership Theories.Eugenio G. Omodeo, Franco Parlamento & Alberto Policriti - 1996 - Mathematical Logic Quarterly 42 (1):41-58.
Three quantifier sentences.Harvey Friedman - manuscript
Herbrand semantics, the potential infinite, and ontology-free logic.Theodore Hailperin - 1992 - History and Philosophy of Logic 13 (1):69-90.
‘Ought’ and Resolution Semantics.Fabrizio Cariani - 2011 - Noûs 47 (3):534-558.
Expanding the universe of universal logic.James Trafford - 2014 - Theoria: Revista de Teoría, Historia y Fundamentos de la Ciencia 29 (3):325-343.
Completeness and incompleteness for intuitionistic logic.Charles Mccarty - 2008 - Journal of Symbolic Logic 73 (4):1315-1327.
On second order intuitionistic propositional logic without a universal quantifier.Konrad Zdanowski - 2009 - Journal of Symbolic Logic 74 (1):157-167.
Scope and the grammar of choice.Donka F. Farkas & Adrian Brasoveanu - unknown
Typed logics with states.J. van Eijck - 1997 - Logic Journal of the IGPL 5 (5):623-645.
Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.

Analytics

Added to PP
2017-02-19

Downloads
18 (#785,610)

6 months
6 (#431,022)

Historical graph of downloads
How can I increase my 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.

Add more citations

References found in this work

Adjointness in Foundations.F. William Lawvere - 1969 - Dialectica 23 (3‐4):281-296.
Locally cartesian closed categories and type theory.R. A. G. Seely - 1984 - Mathematical Proceedings of the Cambridge Philosophical Society 95 (1):33.
Hyperdoctrines, Natural Deduction and the Beck Condition.Robert A. G. Seely - 1983 - Mathematical Logic Quarterly 29 (10):505-542.

View all 6 references / Add more references