Schematic rules and atomic polymorphism (2015)
(Luiz Carlos Pereira, PUC-Rio, BR)

What ́s an introduction rule for an operator φ? What ́s an elimination rule for 1978 Dag Prawitz proposed an answer to these questions 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 intuitionistically definable. It can be shown that a weak‐completeness result holds for a flat variant of Prawitz’ schemata and that full completeness holds for the generalized schemata introduced by Peter Schröder‐Heister. 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 subformula principle can be translated into minimal implicational logic. In 2013 Fernando and Gilda Ferreira introduced the system for atomic polymorphism. This system can be characterized as a second‐order propositional logic in the language {∀, →} such that ∀‐elimination is restricted to atomic instantiations. The aim of the present paper is twofold: [1] to use atomic polymorphism to study the proof theory of schematic systems and [2] to produce high‐level translations for a large class of logics.

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

Due to technical difficulties, the lecture had to be split into two parts and some minutes of the talk may be missing.
​Below is a playlist: