Failure of Completeness in Proof-Theoretic Semantics | Journal of Philosophical Logic Skip to main content
Springer Nature Link
Log in

Failure of Completeness in Proof-Theoretic Semantics

  • Published:
Journal of Philosophical Logic Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. Also known as Kreisel-Putnam rule (cf. [10]) or independence of premiss rule.

  2. Harrop’s rule was proposed as an example of a formula, which is admissible, but not derivable in intuitionistic logic (see [8]). It should be pointed out that admissibility is different from validity, although there are some similarities between these concepts (see [3]).

  3. See also Sandqvist [21], who proposed some sort of semantics for disjunction corresponding to the use of propositional quantification in atomic rules, for which completeness follows almost immediately.

References

  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.

    Article  Google Scholar 

  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.

  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.

    Article  Google Scholar 

  4. Dummett, M. (1991). The Logical Basis of Metaphysics. London: Duckworth.

    Google Scholar 

  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.

  6. Hallnäs, L. (1991). Partial inductive definitions. Theoretical Computer Science, 87, 115–142.

    Article  Google Scholar 

  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.

  8. Harrop, R. (1960). Concerning formulas of the types A → B ∨ C, A → (E x)B(x) in intuitionistic formal systems. Journal of Symbolic Logic, 25, 27–32.

    Article  Google Scholar 

  9. Kleene, S.C. (1971). Introduction to Metamathematics. Wolters-Noordhoff Publishing, Groningen and North-Holland Publishing Company: Amsterdam and London.

    Google Scholar 

  10. Kreisel, G., & Putnam, H. (1957). Eine Unableitbarkeitsbeweismethode fur den intuitionistischen Aussagenkalkül̈. Archiv für Mathematische Logik und Grundlagenforschung, 3, 74–78.

    Article  Google Scholar 

  11. Litland, J. (2012). Topics in Philosophical Logic. Ph.D. thesis, Cambridge: Department of Philosophy, Harvard University.

  12. Makinson, D. (2014). On an inferential semantics for classical logic. Logic Journal of the IGPL, 22(1), 147–154.

    Article  Google Scholar 

  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.

    Chapter  Google Scholar 

  14. Mints, G.E. (1976). Derivability of admissible rules. Journal of Mathematical Sciences, 6, 417–421.

    Google Scholar 

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

    Chapter  Google Scholar 

  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. Prawitz, D. (1974). On the idea of a general proof theory. Synthese, 27, 63–77.

    Article  Google Scholar 

  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.

    Chapter  Google Scholar 

  20. Sandqvist, T. (2009). Classical logic without bivalence. Analysis, 69, 211–217.

    Article  Google Scholar 

  21. Sandqvist, T. (2014). Basis-extension semantics for intuitionistic sentential logic. Submitted manuscript.

  22. Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49, 1284–1300.

    Article  Google Scholar 

  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.

  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. Schroeder-Heister, P. (2012). Proof-theoretic semantics. In E. Zalta (Ed.), The Stanford Encyclopedia of Philosophy (Winter 2012 Edition). http://plato.stanford.edu/archives/win2012/entries/proof-theoretic-semantics/.

  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 

Download references

Acknowledgments

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.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Tübingen, Sand 13, 72076, Tübingen, Germany

    Thomas Piecha & Peter Schroeder-Heister

  2. Faculdade de Filosofia, Campus II, Universidade Federal de Goiás, Goiânia, GO, 74001-970, Brasil

    Wagner de Campos Sanz

Authors
  1. Thomas Piecha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wagner de Campos Sanz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Schroeder-Heister
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Schroeder-Heister.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Piecha, T., de Campos Sanz, W. & Schroeder-Heister, P. Failure of Completeness in Proof-Theoretic Semantics. J Philos Logic 44, 321–335 (2015). https://doi.org/10.1007/s10992-014-9322-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10992-014-9322-x

Keywords

Mathematics Subject Classification (2000)

Search

Navigation