Instantiation overflow

• Autorzy: Dinis B. , Ferreira G.

Identyfikatory

DOI

10.4467/20842589RM.16.002.5279

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

instantiation overow; predicative polymorphism; natural deduction

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2016
• Tom: Vol. 51
• Strony: 15--33
• Opis fizyczny: Bibliogr. 7 poz., rys.

Twórcy

autor

Dinis B.

• Departamento de Matemática Faculdade de Ciéncias da Universidade de Lisboa Campo Grande, Ed. C6 1749-016 Lisboa Portugal

autor

Ferreira G.

• Departamento de Matemática Faculdade de Ciéncias da Universidade de Lisboa Campo Grande, Ed. C6 1749-016 Lisboa Portugal
• Departamento de Matemática Universidade Lusófona de Humanidades e Tecnologias Av. do Campo Grande, 376 1749-024 Lisboa Portugal

Bibliografia

• [1] F. Ferreira, Comments on Predicative Logic, Journal of Philosophical Logic 35 (2006), 1-8.
• [2] F. Ferreira and G. Ferreira, Commuting conversions vs. the standard conversions of the \good" connectives, Studia Logica 92 (2009), 63-84.
• [3] F. Ferreira and G. Ferreira, Atomic Polymorphism, Journal of Symbolic Logic 78:1 (2013), 260-274.
• [4] F. Ferreira and G. Ferreira, The faithfulness of atomic polymorphism, Trends in Logic XIII, A. Indrzejczak, J. Kaczmarek, M. Zawidzki (eds.), Łódź University Press, pp. 55-64, 2014.
• [5] F. Ferreira and G. Ferreira, The faithfulness of Fat: a proof-theoretic proof, Studia Logica 103:6 (2015), 1303-1311.
• [6] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press, 1989.
• [7] D. Prawitz, Natural Deduction, Almkvist & Wiskell, Stockholm, 1965. Reprinted in Dover Publications, 2006.

Uwagi

PL

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę.