A Syntactic Embedding of Predicate Logic into Second-Order Propositional Logic

Notre Dame Journal of Formal Logic 51 (4):457-473 (2010)
  Copy   BIBTEX

Abstract

We give a syntactic translation from first-order intuitionistic predicate logic into second-order intuitionistic propositional logic IPC2. The translation covers the full set of logical connectives ∧, ∨, →, ⊥, ∀, and ∃, extending our previous work, which studied the significantly simpler case of the universal-implicational fragment of predicate logic. As corollaries of our approach, we obtain simple proofs of nondefinability of ∃ from the propositional connectives and nondefinability of ∀ from ∃ in the second-order intuitionistic propositional logic. We also show that the ∀-free fragment of IPC2 is undecidable

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

The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Logic: an introduction.Greg Restall - 2006 - New York: Routledge.
Undecidability and intuitionistic incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.

Analytics

Added to PP
2010-09-30

Downloads
44 (#316,309)

6 months
2 (#658,980)

Historical graph of downloads
How can I increase my downloads?