Studia Logica

, Volume 107, Issue 1, pp 233–246

# Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-Theoretic Semantics

• Thomas Piecha
• Peter Schroeder-Heister
Article

## 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.

## Keywords

General proof theory Proof-theoretic semantics Intuitionistic logic Prawitz’s conjecture Incompleteness Logical constants Kripke semantics

## Notes

### 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.

## References

1. 1.
Goldfarb, W., On Dummett’s “Proof-theoretic Justifications of Logical Laws”, in T. Piecha and P. Schroeder-Heister [6], pp. 195–210.Google Scholar
2. 2.
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.
3. 3.
Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66:281–294, 2001.
4. 4.
Piecha, T., Completeness in proof-theoretic semantics, in T. Piecha and P. Schroeder-Heister [6], pp. 231–251.Google Scholar
5. 5.
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.Google Scholar
6. 6.
Piecha, T., and P. Schroeder-Heister, (eds.), Advances in Proof-Theoretic Semantics, vol. 43 of Trends in Logic, Springer, 2016.Google Scholar
7. 7.
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.Google Scholar
8. 8.
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.Google Scholar
9. 9.
Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965. Reprinted by Dover Publications, Mineola, N.Y., 2006.Google Scholar
10. 10.
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.Google Scholar
11. 11.
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.Google Scholar
12. 12.
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.