Loading...
Publication
Instantiation overflow
Authors
Advisor(s)
Abstract(s)
The well-known embedding of full intuitionistic 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 identi ed
with such property: the types that result from the Prawitz translation of the
propositional connectives (\bot,\wedge, \vee) 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.
Description
Keywords
Instantiation overflow Predicative polymorphism Natural deduction