Hostname: page-component-8448b6f56d-cfpbc Total loading time: 0 Render date: 2024-04-15T13:17:06.063Z Has data issue: false hasContentIssue false
  • English
  • Français

INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES

Published online by Cambridge University Press:  05 October 2009

WAGNER DE CAMPOS SANZ  and
THOMAS PIECHA
WAGNER DE CAMPOS SANZ*
Affiliation:
Faculdade de Filosofia, Universidade Federal de Goiás
THOMAS PIECHA*
Affiliation:
Wilhelm-Schickard-Institut, Universität Tübingen
*
*FACULDADE DE FILOSOFIA, UNIVERSIDADE FEDERAL DE GOIÁS, CEP 74001-970, GOIÂNIA, GO, BRAZIL E-mail:sanz@fchf.ufg.br
†WILHELM-SCHICKARD-INSTITUT, UNIVERSITÄT TÜBINGEN, SAND 13, 72076 TÜBINGEN, GERMANY E-mail:piecha@informatik.uni-tuebingen.de
Get access Rights & Permissions [Opens in a new window]

Abstract

The inversion principle for logical rules expresses a relationship between introduction and elimination rules for logical constants. Hallnäs & Schroeder-Heister (1990, 1991) proposed the principle of definitional reflection, which embodies basic ideas of inversion in the more general context of clausal definitions. For the context of admissibility statements, this has been further elaborated by Schroeder-Heister (2007). Using the framework of definitional reflection and its admissibility interpretation, we show that, in the sequent calculus of minimal propositional logic, the left introduction rules are admissible when the right introduction rules are taken as the definitions of the logical constants and vice versa. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 2 , Issue 3 , September 2009 , pp. 550 - 569
Copyright
Copyright © Association for Symbolic Logic 2009

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

Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431. English translation (1969) in Szabo, M. E., editor. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. Amsterdam, The Netherlands: North-Holland, pp. 68–131.CrossRefGoogle Scholar
Hallnäs, L., & Schroeder-Heister, P. (1990). A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation, 1, 261–283.CrossRefGoogle Scholar
Hallnäs, L., & Schroeder-Heister, P. (1991). A proof-theoretic approach to logic programming. II. Programs as definitions. Journal of Logic and Computation, 1, 635–660.CrossRefGoogle Scholar
Hallnäs, L. (1991). Partial inductive definitions. Theoretical Computer Science, 87, 115–142.CrossRefGoogle Scholar
Iemhoff, R. (2001). On the admissible rules of intuitionistic propositional logic. Journal of Symbolic Logic, 66, 281–294.CrossRefGoogle Scholar
Iemhoff, R. (2003). Towards a proof system for admissibility. In Baaz, M., and Makowsky, J. A., editors. Computer Science Logic 2003. Lecture Notes in Computer Science 2803. Berlin: Springer, pp. 255–270.Google Scholar
Iemhoff, R., & Metcalfe, G. (2009). Proof theory for admissible rules. Annals of Pure and Applied Logic, 159, 171–186.CrossRefGoogle Scholar
Jeřábek, E. (2008). Independent bases of admissible rules. Logic Journal of the IGPL, 16, 249–267.CrossRefGoogle Scholar
Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik (second edition 1969). Berlin: Springer.CrossRefGoogle Scholar
Moriconi, E., & Tesconi, L. (2008). On inversion principles. History and Philosophy of Logic, 29, 103–113.CrossRefGoogle Scholar
Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge, UK: Cambridge University Press.CrossRefGoogle Scholar
von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541–567.CrossRefGoogle Scholar
Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm, Sweden: Almqvist & Wiksell. Reprinted by Dover Publications, Mineola, NY (2006).Google 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. Dordrecht, The Netherlands: Reidel, pp. 25–40. Revised and extended German translation (1982): Beweise und die Bedeutung und Vollständigkeit der logischen Konstanten. Conceptus, XVI, 3–44.CrossRefGoogle Scholar
Rybakov, V. V. (1997). Admissibility of Logical Inference Rules. Studies in Logic and the Foundations of Mathematics 136. Amsterdam, The Netherlands: North-Holland.Google Scholar
Schroeder-Heister, P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49, 1284–1300.CrossRefGoogle Scholar
Schroeder-Heister, P. (1993). Rules of definitional reflection. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal June 19–23, 1993). Los Alamitos, CA: IEEE Computer Society, pp. 222–232.Google Scholar
Schroeder-Heister, P. (2007). Generalized definitional reflection and the inversion principle. Logica Universalis, 1, 355–376.CrossRefGoogle Scholar
Schroeder-Heister, P. (2008). Lorenzen’s operative justification of intuitionistic logic. In van Atten, M., Boldini, P., Bourdeau, M., and Heinzmann, G., editors. One Hundred Years of Intuitionism (1907-2007): The Cerisy Conference. Basel, Switzerland: Birkhäuser, pp. 214–240.CrossRefGoogle Scholar