Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-23T02:33:33.926Z Has data issue: false hasContentIssue false
  • English
  • Français

ON FLATTENING ELIMINATION RULES

Published online by Cambridge University Press:  23 January 2014

GRIGORY K. OLKHOVIKOV  and
PETER SCHROEDER-HEISTER
GRIGORY K. OLKHOVIKOV*
Affiliation:
Department of Philosophy, Ural Federal University
PETER SCHROEDER-HEISTER*
Affiliation:
Department of Computer Science, Universität Tübingen
*
*DEPARTMENT OF PHILOSOPHY URAL FEDERAL UNIVERSITY 51 LENIN AVENUE 620083 YEKATERINBURG, RUSSIA E-mail:[email protected]
†DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF TÜBINGEN SAND 13 72076 TÜBINGEN, GERMANY E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 7 , Issue 1 , March 2014 , pp. 60 - 72
Copyright
Copyright © Association for Symbolic Logic 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Dummett, M. (1991). The Logical Basis of Metaphysics. London: Duckworth.Google Scholar
Dyckhoff, R. (1988). Implementing a simple proof assistant. In Workshop on Programming for Logic Teaching (Leeds, 6-8 July 1987): Proceedings 23/1988 (pp. 49–59). University of Leeds, Centre for Theoretical Computer Science. Available from: http://rd.host.cs.st-andrews.ac.uk/publications/LeedsPaper.pdf.Google Scholar
Dyckhoff, R. (2009). Generalised Elimination Rules and Harmony. Manuscript, University of St. Andrews. Available from: http://rd.host.cs.st-andrews.ac.uk/talks/2009/GE.pdfGoogle Scholar
Francez, N., & Dyckhoff, R. (2012). A note on harmony. Journal of Philosophical Logic 41, 613–628.CrossRefGoogle Scholar
López-Escobar, E. G. K. (1999). Standardizing the N systems of Gentzen. In Caicedo, X., and Montenegro, C. H., editors. Models, Algebras and Proofs. Lecture Notes in Pure and Applied Mathematics, Vol. 203. New York, NY: Marcel Dekker, pp. 411–434.Google Scholar
Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: Springer.CrossRefGoogle Scholar
Olkhovikov, G. K. & Schroeder-Heister, P. (2014). Proof-theoretic harmony and the levels of rules: General non-flattening results. In Moriconi, E., and Tesconi, L., editors. Second Pisa Colloquium in Logic, Language and Epistemology. Pisa: ETS.Google Scholar
Pitts, A. M. (1992). On an interpretation of second order quantification in first order intuitionistic propositional logic. Journal of Symbolic Logic, 57, 33–52.Google Scholar
Plato, J. v. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541–567.CrossRefGoogle Scholar
Prawitz, D. (1979). Proofs and the meaning and completeness of the logical constants. In Hintikka, J., Niiniluoto, I., and Saarinen, E., editors. Essays on Mathematical and Philosophical Logic: Proceedings of the Fourth Scandinavian Logic Symposium and the First Soviet-Finnish Logic Conference, Jyväskylä, Finland, June 29 – July 6, 1976. Dordrecht, Netherlands: Kluwer, pp. 25–40[revised German translation ‘Beweise und die Bedeutung und Vollständigkeit der logischen Konstanten’, Conceptus, 16, 1982, 31–44].Google Scholar
Read, S. (2010). General-elimination harmony and the meaning of the logical constants. Journal of Philosophical Logic, 39, 557–576.Google Scholar
Read, S. (2014). General-elimination harmony and higher-level rules. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Heidelberg, Germany: Springer.Google Scholar
Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49, 1284–1300.CrossRefGoogle Scholar
Schroeder-Heister, P. (2012). Proof-theoretic semantics. In Zalta, E., editor. Stanford Encyclopedia of Philosophy. Stanford, CA: Stanford University. Available from: http://plato.stanford.edu.Google Scholar
Schroeder-Heister, P. (2013). Generalized elimination inferences, higher-level rules, and the implications-as-rules interpretation of the sequent calculus. In Pereira, L. C., Haeusler, E. H., and de Paiva, V., editors. Advances in Natural Deduction: A Celebration of Dag Prawitz’s Work. Heidelberg, Germany: Springer.Google Scholar
Schroeder-Heister, P. (2014a). The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. Studia Logica (Special issue, ed. Andrzej Indrzejczak: Gentzen’s and Jaśkowski’s heritage - 80 years of Natural Deduction and Sequent Calculi).CrossRefGoogle Scholar
Schroeder-Heister, P. (2014b). Harmony in proof-theoretic semantics: A reductive analysis. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Heidelberg, Germany: Springer.Google Scholar
Tennant, N. (1978). Natural Logic. Edinburgh, UK: Edinburgh University Press.Google Scholar
Tennant, N. (1992). Autologic. Edinburgh, UK: Edinburgh University Press.Google Scholar
von Kutschera, F. (1968). Die Vollständigkeit des Operatorensystems {¬,∧,∨,⊃} für dieintuitionistische Aussagenlogik im Rahmen der Gentzensemantik. Archiv für mathematische Logik und Grundlagenforschung, 11, 3–16.Google Scholar
Wansing, H. (1993). The Logic of Information Structures. Berlin: Springer (Springer Lecture Notes in Artificial Intelligence, Vol. 681).Google Scholar
Zucker, J.I., & Tragesser, R.S. (1978). The adequacy problem for inferential logic. Journal of Philosophical Logic, 7, 501–516.Google Scholar