Journal of Philosophical Logic

, Volume 44, Issue 3, pp 321–335 | Cite as

Failure of Completeness in Proof-Theoretic Semantics

  • Thomas Piecha
  • Wagner de Campos Sanz
  • Peter Schroeder-Heister


Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop’s rule is valid under substitution, which refutes the completeness conjecture for intuitionistic logic.


Proof-theoretic semantics Intuitionistic logic Mints’s rule Harrop’s rule Completeness 

Mathematics Subject Classification (2000)

03A05 03F03 03F55 



This work was supported by the French-German ANR-DFG project “Hypothetical Reasoning – Its Proof-Theoretic Analysis” (HYPOTHESES), DFG grant Schr 275/16-2 to T.P. and P.S.-H. and by grants CNPq 401882/2011-0 and CAPES/DAAD 1110-11-0 to W.d.C.S. We should like to thank the anonymous referees for very valuable detailed comments on earlier versions of this paper. We also thank Grigory Olkhovikov and Tor Sandqvist for helpful comments and suggestions.


  1. 1.
    de Campos Sanz, W., & Piecha, T. (2009). Inversion by definitional reflection and the admissibility of logical rules. Review of Symbolic Logic, 2(3), 550–569.CrossRefGoogle Scholar
  2. 2.
    de Campos Sanz,W., & Piecha, T. (2014). A critical remark on the BHK interpretation of implication. In P.E. Bour, G. Heinzmann,W. Hodges, P. Schroeder-Heister (Eds.), 14th CLMPS 2011 Proceedings, Philosophia Scientiae, Vol. 18(3). To appear.Google Scholar
  3. 3.
    de Campos Sanz, W., Piecha, T., Schroeder-Heister, P. (2014). Constructive semantics, admissibility of rules and the validity of Peirce’s law. Logic Journal of the IGPL, 22 (2), 297–308. First published online August 6, 2013.CrossRefGoogle Scholar
  4. 4.
    Dummett, M. (1991). The Logical Basis of Metaphysics. London: Duckworth.Google Scholar
  5. 5.
    Goldfarb, W. (2014). On Dummett’s “Proof-theoretic Justifications of Logical Laws”. In T. Piecha & P. Schroeder-Heister (Eds.), Advances in Proof-Theoretic Semantics. Trends in Logic. Dordrecht: Springer. Circulated manuscript, 1998.Google Scholar
  6. 6.
    Hallnäs, L. (1991). Partial inductive definitions. Theoretical Computer Science, 87, 115–142.CrossRefGoogle Scholar
  7. 7.
    Hallnäs, L. (2006). On the proof-theoretic foundation of general definition theory. In R. Kahle & P. Schroeder-Heister (Eds.), Proof-Theoretic Semantics. Special issue of Synthese (Vol. 148, pp. 589– 602). Berlin: Springer.Google Scholar
  8. 8.
    Harrop, R. (1960). Concerning formulas of the types ABC, A → (E x)B(x) in intuitionistic formal systems. Journal of Symbolic Logic, 25, 27–32.CrossRefGoogle Scholar
  9. 9.
    Kleene, S.C. (1971). Introduction to Metamathematics. Wolters-Noordhoff Publishing, Groningen and North-Holland Publishing Company: Amsterdam and London.Google Scholar
  10. 10.
    Kreisel, G., & Putnam, H. (1957). Eine Unableitbarkeitsbeweismethode fur den intuitionistischen Aussagenkalkül̈. Archiv für Mathematische Logik und Grundlagenforschung, 3, 74–78.CrossRefGoogle Scholar
  11. 11.
    Litland, J. (2012). Topics in Philosophical Logic. Ph.D. thesis, Cambridge: Department of Philosophy, Harvard University.Google Scholar
  12. 12.
    Makinson, D. (2014). On an inferential semantics for classical logic. Logic Journal of the IGPL, 22(1), 147–154.CrossRefGoogle Scholar
  13. 13.
    Martin-Löf, P. (1971). Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics (Vol. 63, pp. 179–216). Amsterdam: North-Holland.CrossRefGoogle Scholar
  14. 14.
    Mints, G.E. (1976). Derivability of admissible rules. Journal of Mathematical Sciences, 6, 417–421.Google Scholar
  15. 15.
    Olkhovikov, G.K., & Schroeder-Heister, P. (2014). Proof-theoretic harmony and the levels of rules: Generalised non-flattening results. In E. Moriconi & L. Tesconi (Eds.), Second Pisa Colloquium in Logic, Language and Epistemology. Pisa: ETS. To appear.Google Scholar
  16. 16.
    Prawitz, D. (1971). Ideas and results in proof theory. In J.E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics (Vol. 63, pp. 235–307). Amsterdam: North-Holland.CrossRefGoogle Scholar
  17. 17.
    Prawitz, D. (1973). Towards a foundation of a general proof theory. In P. Suppes, et al. (Eds.), Logic, Methodology and Philosophy of Science IV (pp. 225–250). Amsterdam: North-Holland.Google Scholar
  18. 18.
    Prawitz, D. (1974). On the idea of a general proof theory. Synthese, 27, 63–77.CrossRefGoogle Scholar
  19. 19.
    Prawitz, D. (2014). 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, V. de Paiva (Eds.), Advances in Natural Deduction, Trends in Logic (Vol. 39, pp. 269–279). Berlin: Springer.CrossRefGoogle Scholar
  20. 20.
    Sandqvist, T. (2009). Classical logic without bivalence. Analysis, 69, 211–217.CrossRefGoogle Scholar
  21. 21.
    Sandqvist, T. (2014). Basis-extension semantics for intuitionistic sentential logic. Submitted manuscript.Google Scholar
  22. 22.
    Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49, 1284–1300.CrossRefGoogle Scholar
  23. 23.
    Schroeder-Heister, P. (1993). Rules of definitional reflection. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal 1993) (pp. 222–232). Los Alamitos: IEEE Computer Society.Google Scholar
  24. 24.
    Schroeder-Heister, P. (2006). Validity concepts in proof-theoretic semantics. In R. Kahle & P. Schroeder-Heister (Eds.), Proof-Theoretic Semantics. Special issue of Synthese (Vol. 148, pp. 525–571). Berlin: Springer.Google Scholar
  25. 25.
    Schroeder-Heister, P. (2012). Proof-theoretic semantics. In E. Zalta (Ed.), The Stanford Encyclopedia of Philosophy (Winter 2012 Edition).
  26. 26.
    Schroeder-Heister, P. (2014). The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. In A. Indrzejczak (Ed.), Special issue, commemorating the 80th anniversary of Gentzens and Jaśkowski’s groundbreaking works on assumption based calculi, Studia Logica (Vol. 103). Berlin: Springer. To appear.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2014

Authors and Affiliations

  • Thomas Piecha
    • 1
  • Wagner de Campos Sanz
    • 2
  • Peter Schroeder-Heister
    • 1
  1. 1.Department of Computer ScienceUniversity of TübingenTübingenGermany
  2. 2.Faculdade de Filosofia, Campus IIUniversidade Federal de GoiásGoiâniaBrasil

Personalised recommendations