Abstract
We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus (\(\mathbf {IPC}\)), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of \(\mathbf {IPC}\) into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of \(\mathbf {IPC}\) (presented in a recent paper co-authored with Fernando Ferreira) and answers a question then posed by Pierluigi Minari.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Dinis, B., and G. Ferreira, Instantiation overflow, Reports on Mathematical Logic 51:15–33, 2016.
Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35:1–8, 2006.
Ferreira, F., and G. Ferreira, Commuting conversions vs. the standard conversions of the “good” connectives, Studia Logica 92:63–84, 2009.
Ferreira, F., and G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78:260–274, 2013.
Ferreira, F., and G. Ferreira, The faithfulness of \({{\bf F}}_{{\bf at}}\): a proof-theoretic proof, Studia Logica 103(6):1303–1311, 2015.
Ferreira, G., Eta-conversions of \({\bf IPC} \) implemented in atomic \({\bf F}\), To appear in Logic Jnl IGPL, published online July 1, 2016. doi:10.1093/jigpal/jzw035.
Girard, J.-Y., Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, 1989.
Minari, P., and A. Wronski, The property (HD) in intermediate logics. A partial solution of a problem of H. Ono, Reports on Mathematical Logic 22:21–25, 1988.
Prawitz, D., Natural Deduction, Almkvist & Wiksell, Stockholm, 1965. Reprinted, with a new preface, in Dover Publications, 2006.
Reynolds, J. C., Towards a theory of type structure, in B. Robinet (ed.), Lecture Notes in Computer Science, vol. 19, Colloque sur la programmation, Springer, 1974, pp. 408–425.
Russell, B., Principles of Mathematics, 2nd edn., George Allen and Unwin, London, 1903 (1937).
Author information
Authors and Affiliations
Corresponding author
Additional information
Presented by Jacek Malinowski
Rights and permissions
About this article
Cite this article
Ferreira, G. Rasiowa–Harrop Disjunction Property. Stud Logica 105, 649–664 (2017). https://doi.org/10.1007/s11225-016-9704-x
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-016-9704-x