TY - JOUR
TI - Instantiation overflow
AU - Dinis, Bruno
AU - Ferreira, Gilda
TI - Instantiation overflow
AB - 
	The well-known embedding of full intuition- istic propositional calculus into the atomic polymorphic system Fat is possible due to the intriguing phenomenon of instantiation overflow. Instantiation overflow ensures that (in Fat) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in Fat were identified with such property: the types that result from the Prawitz translation of the propositional connectives (?, ^, _) into Fat (or Girard's system F). Are there other types in Fat with instantiation overflow? In this paper we show that the answer is yes and we isolate a class of formulas with such property.
VL - 2016
IS - Number 51
PY - 2016
SN - 0137-2904
C1 - 2084-2589
SP - 15
EP - 33
DO - 10.4467/20842589RM.16.002.5279
UR - https://ejournals.eu/en/journal/reports-on-mathematical-logic/article/instantiation-overflow
KW - Instantiation overflow
KW - predicative polymorphism
KW - natural deduction