Rasiowa–Harrop Disjunction Property

Studia Logica 105 (3):649-664 (2017)
  Copy   BIBTEX

Abstract

We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus ), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of \ into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of \ and answers a question then posed by Pierluigi Minari.

Categories

Keywords

Reprint years

DOI

10.1007/s11225-016-9704-x

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,296

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

The Faithfulness of Fat: A Proof-Theoretic Proof.Fernando Ferreira & Gilda Ferreira - 2015 - Studia Logica 103 (6):1303-1311.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
A secondary semantics for Second Order Intuitionistic Propositional Logic.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2004 - Mathematical Logic Quarterly 50 (2):202-210.
On Harrop disjunction property in intermediate predicate logics.Katsumasa Ishii - 2023 - Archive for Mathematical Logic 63 (3):317-324.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A New Solution to a Problem of Hosoi and Ono.Michael Zakharyaschev - 1994 - Notre Dame Journal of Formal Logic 35 (3):450-457.
η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
A simple proof of second-order strong normalization with permutative conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
Commuting Conversions vs. the Standard Conversions of the “Good” Connectives.Fernando Ferreira & Gilda Ferreira - 2009 - Studia Logica 92 (1):63-84.

Analytics

Added to PP
2016-12-20

Downloads
28 (#589,033)

6 months
11 (#272,000)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Atomic polymorphism and the existence property.Gilda Ferreira - 2018 - Annals of Pure and Applied Logic 169 (12):1303-1316.

Add more citations

References found in this work

Comments on Predicative Logic.Fernando Ferreira - 2006 - Journal of Philosophical Logic 35 (1):1-8.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.

Add more references