Rasiowa–Harrop disjunction property

Ferreira, Gilda

http://hdl.handle.net/10400.2/7090

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
RH-disjunction.pdf		343.85 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Gilda

Abstract(s)

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.

Keywords

Mathematical logic Rasiowa–Harrop disjunction property Intuitionistic propositional calculus Predicative polymorphism Natural deduction Strong normalization

URI

http://hdl.handle.net/10400.2/7090

Citation

Ferreira, Gilda - Rasiowa–Harrop disjunction property. "Stud Logica" [Em linha]. ISSN 0039-3215 (Print) 1572-8730 (Online). Vol. 105, nº 3 (2017), p. 649-664