Bruno Dinis
Universidade de Lisboa

Abstract: Instantiation overflow ensures that, in the atomic polymorphism system Fat, we can instantiate universal formulas by any formula of the system, not necessarily atomic. In a recent paper [1] the notion of Prawitz formula was introduced in order to study the phenomenon of instantiation overflow. It was shown that all formulas of level 0 and 1 have instantiation overflow and that there exists a Prawitz formula of level n with the same property, for each natural number n. It was however left open if all Prawitz formulas have instantiation overflow. In this talk I will present this problem and present new ideas on this matter.

[1] B. Dinis and G. Ferreira - Instantiation overflow, to appear in Reports on Mathematical Logic.

This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.