Seminários de Lógica Matemática 6 de Novembro 2008, 18h00 Abstract: The rules of elimination of the connectives "absurdum", "or" and "there exists" have been subjected to some criticism because they are not as natural and as well behaved as the other inferential rules. In fact, Jean-Yves Girard says that "the elimination rules [of these connectives] are very bad". Moreover, in order to have normal proofs with the subformula property, there is the need to add some ad hoc conversions: the commuting conversions. Girard adds that "the need to add these supplementary rules reveals an inadequacy of the syntax". We present an embedding of the intuitionistic predicate calculus into a second-order predicative system with no "bad" connectives. Moreover, in join work with Gilda Ferreira, we show that the redex and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions. | back |