Rasiowa–Harrop disjunction property

We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus (IPC), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of IPC into an atomic...

Full description

Bibliographic Details
Main Author: Ferreira, Gilda (author)
Format: article
Language:eng
Published: 2018
Subjects:
Mathematical logic
Rasiowa–Harrop disjunction property
Intuitionistic propositional calculus
Predicative polymorphism
Natural deduction
Strong normalization
Online Access:http://hdl.handle.net/10400.2/7090
Country:Portugal
Oai:oai:repositorioaberto.uab.pt:10400.2/7090
Description
Summary:We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus (IPC), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of IPC into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of IPC (presented in a recent paper co-authored with Fernando Ferreira) and answers a question then posed by Pierluigi Minari.

Similar Items