Abstract
Prawitz proposed certain notions of proof-theoretic validity and conjectured that intuitionistic logic is complete for them [11, 12]. Considering propositional logic, we present a general framework of five abstract conditions which any proof-theoretic semantics should obey. Then we formulate several more specific conditions under which the intuitionistic propositional calculus (IPC) turns out to be semantically incomplete. Here a crucial role is played by the generalized disjunction principle. Turning to concrete semantics, we show that prominent proposals, including Prawitz’s, satisfy at least one of these conditions, thus rendering IPC semantically incomplete for them. Only for Goldfarb’s [1] proof-theoretic semantics, which deviates from standard approaches, IPC turns out to be complete. Overall, these results show that basic ideas of proof-theoretic semantics for propositional logic are not captured by IPC.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Goldfarb, W., On Dummett’s “Proof-theoretic Justifications of Logical Laws”, in T. Piecha and P. Schroeder-Heister [6], pp. 195–210.
Harrop, R., Concerning formulas of the types \(A \rightarrow B \vee C\), \(A \rightarrow (Ex)B(x)\) in intuitionistic formal systems, Journal of Symbolic Logic 25:27–32, 1960.
Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66:281–294, 2001.
Piecha, T., Completeness in proof-theoretic semantics, in T. Piecha and P. Schroeder-Heister [6], pp. 231–251.
Piecha, T., W. de Campos Sanz, and P. Schroeder-Heister, Failure of completeness in proof-theoretic semantics, Journal of Philosophical Logic 44:321–335, 2015. First published online August 1, 2014.
Piecha, T., and P. Schroeder-Heister, (eds.), Advances in Proof-Theoretic Semantics, vol. 43 of Trends in Logic, Springer, 2016.
Piecha, T., and P. Schroeder-Heister, Atomic systems in proof-theoretic semantics: two approaches, in J. Redmond, O. Pombo Martins, and Á. N. Fernández, (eds.), Epistemology, Knowledge and the Impact of Interaction, Springer, Cham, 2016, pp. 47–62.
Piecha, T., and P. Schroeder-Heister, The definitional view of atomic systems in proof-theoretic semantics, in P. Arazim, and T. Lávička, (eds.), The Logica Yearbook 2016, College Publications, London, 2017, pp. 185–200.
Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965. Reprinted by Dover Publications, Mineola, N.Y., 2006.
Prawitz, D., Ideas and results in proof theory, in J. E. Fenstad, (ed.), Proceedings of the Second Scandinavian Logic Symposium, vol. 63 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1971, pp. 235–307.
Prawitz, D., Towards a foundation of a general proof theory, in P. Suppes, et al., (eds.), Logic, Methodology and Philosophy of Science IV, North-Holland, Amsterdam, 1973, pp. 225–250.
Prawitz, D., An approach to general proof theory and a conjecture of a kind of completeness of intuitionistic logic revisited, in L. C. Pereira, E. H. Haeusler, and V. de Paiva, (eds.), Advances in Natural Deduction, vol. 39 of Trends in Logic, Springer, Berlin, 2014, pp. 269–279.
Acknowledgements
This work was carried out within the French-German ANR-DFG project “Beyond Logic: Hypothetical Reasoning in Philosophy of Science, Informatics, and Law”, DFG Grant Schr 275/17-1. We are grateful to two referees for their helpful comments and suggestions.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Piecha, T., Schroeder-Heister, P. Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-Theoretic Semantics. Stud Logica 107, 233–246 (2019). https://doi.org/10.1007/s11225-018-9823-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-018-9823-7