Intuitionistic completeness of first-order logic

Annals of Pure and Applied Logic 165 (1):164-198 (2014)
  Copy   BIBTEX

Abstract

We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the Nuprl proof assistant.Our result demonstrates the value of uniform validity as a semantic notion for studying logical theories, and it provides new techniques for showing that formulas are not intuitionistically provable. Here we demonstrate its value for minimal and intuitionistic first-order logic

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

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

Through your library

Similar books and articles

Intuitionistic completeness for first order classical logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
Reverse Mathematics and Completeness Theorems for Intuitionistic Logic.Takeshi Yamazaki - 2001 - Notre Dame Journal of Formal Logic 42 (3):143-148.
Negationless intuitionism.Enrico Martino - 1998 - Journal of Philosophical Logic 27 (2):165-177.
Undecidability and intuitionistic incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
Completeness and incompleteness for intuitionistic logic.Charles Mccarty - 2008 - Journal of Symbolic Logic 73 (4):1315-1327.
Intuitionistic Completeness and Classical Logic.D. C. McCarty - 2002 - Notre Dame Journal of Formal Logic 43 (4):243-248.
The Semantic Completeness of a Global Intuitionistic Logic.Hiroshi Aoyama - 1998 - Mathematical Logic Quarterly 44 (2):167-175.
Reflexive Intermediate Propositional Logics.Nathan C. Carter - 2006 - Notre Dame Journal of Formal Logic 47 (1):39-62.
Basic Predicate Calculus.Wim Ruitenburg - 1998 - Notre Dame Journal of Formal Logic 39 (1):18-46.
Towards intuitionistic dynamic logic.J. W. Degen & J. M. Werner - 2006 - Logic and Logical Philosophy 15 (4):305-324.

Analytics

Added to PP
2014-01-16

Downloads
29 (#472,004)

6 months
2 (#658,848)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Elements of Intuitionism.Michael Dummett - 1977 - New York: Oxford University Press. Edited by Roberto Minio.
The Calculi of Lambda-conversion.Alonzo Church - 1985 - Princeton, NJ, USA: Princeton University Press.
Type-theoretical Grammar.Aarne Ranta - 1994 - Oxford, England: Oxford University Press on Demand.
Proofs and types.Jean-Yves Girard - 1989 - New York: Cambridge University Press.
On the interpretation of intuitionistic number theory.S. C. Kleene - 1945 - Journal of Symbolic Logic 10 (4):109-124.

View all 27 references / Add more references