Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Reports on Mathematical Logic

1 2016

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: instantiation overow

Sortuj według:

Ogranicz wyniki do:

Instantiation overflow

Dinis B., Ferreira G.

Reports on Mathematical Logic

2016

Vol. 51

15--33

The well-known embedding of full intuitionistic propositional calculus into the atomic polymorphic system Fat is possible due to the intriguing phenomenon of instantiation overow. Instantiation overow 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 overow ? In this paper we show that the answer is yes and we isolate a class of formulas with such property.