Luiz Carlos Pereira: Atomic Polymorphism and schematic rules: a view from proof-theory

Abstract: 

(joint work with Edward Hermann Haeusler, PUC-Rio)

Translations have been put to many uses in logic. In the first half of last century, translations played an important role in foundational matters: the reduction of foundational questions to constructive settings. In the sixties translations became an autonomous topic: several general approaches to translations were proposed (proof-theoretical, algebraic). Another possible use of translation is related to schematic rules of inference. In 1978, Prawitz proposed an answer to the following interesting and natural questions: What’s an introduction rule for an operator φ? What’s an elimination rule for φ? Prawitz’ answer was given by means of schematic introduction and elimination rules. Prawitz also proposed a constructive version of the well-known classical truth-functional completeness: if the introduction and elimination rules for an operator φ are instances of the schematic introduction and elimination rules, then φ is intutionistically definable. Peter Schröder-Heister showed how to obtain this completeness result for higher-level schemata. These schematic introduction and elimination rules can also be used to show that logics whose operators satisfy the schematic rules and whose derivations satisfy the sub-formula principle can be translate into minimal implicational logic. Fernando Ferreira and Gilda Ferreira proposed still another use for translations: to use the Russell-Prawitz translation in order to study the proof-theory of intuitionistic propositional and first-order logic. This study is done in the atomically polymorphic system Fat. This system can be characterized as a second order propositional logic in the language {∀1, ∀2, →} such that ∀2-elimination is restricted to atomic instantiations. The aim of the present paper is to use atomic polymorphism to study the proof theory of schematic systems.