The Review of Symbolic Logic

Research Article

INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES

WAGNER DE CAMPOS SANZa1 c1 and THOMAS PIECHAa2 c2

a1 Faculdade de Filosofia, Universidade Federal de Goiás

a2 Wilhelm-Schickard-Institut, Universität Tübingen

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.

(Received December 01 2008)

Correspondence:

c1 FACULDADE DE FILOSOFIA, UNIVERSIDADE FEDERAL DE GOIÁS, CEP 74001-970, GOIÂNIA, GO, BRAZIL E-mail: sanz@fchf.ufg.br

c2 WILHELM-SCHICKARD-INSTITUT, UNIVERSITÄT TÜBINGEN, SAND 13, 72076 TÜBINGEN, GERMANY E-mail: piecha@informatik.uni-tuebingen.de