Instantiation overflow. (English) Zbl 1403.03119
Summary: The well-known embedding of full intuitionistic propositional calculus into the atomic polymorphic system \(\mathbf{F}_{\mathbf{at}}\) is possible due to the intriguing phenomenon of instantiation overflow. Instantiation overflow ensures that (in \(\mathbf{F}_{\mathbf{at}}\) ) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in \(\mathbf{F}_{\mathbf{at}}\) were identified with such property: the types that result from the Prawitz translation of the propositional connectives (\(\bot\), \(\wedge\), \(\vee\)) into \(\mathbf{F}_{\mathbf{at}}\) (or Girard’s system \(\mathbf{F}\)). Are there other types in \(\mathbf{F}_{\mathbf{at}}\) with instantiation overflow? In this paper we show that the answer is yes and we isolate a class of formulas with such property.
MSC:
03F07 | Structure of proofs |
03F03 | Proof theory in general (including proof-theoretic semantics) |
03B20 | Subsystems of classical logic (including intuitionistic logic) |