Atomic polymorphism and the existence property

We present a purely proof-theoretic proof of the existence property for the full intuitionistic first-order predicate calculus, via natural deduction, in which commuting conversions are not needed. Such proof illustrates the potential of an atomic polymorphic system with only three generators of for...

Full description

Bibliographic Details
Main Author: Ferreira, Gilda (author)
Format: article
Language:eng
Published: 2020
Subjects:
Predicative polymorphism
Intuitionistic predicate calculus
Existence property
Natural deduction
Normalization
Faithfulness
ODS::04:Educação de Qualidade
Online Access:http://hdl.handle.net/10400.2/9416
Country:Portugal
Oai:oai:repositorioaberto.uab.pt:10400.2/9416
Description
Summary:We present a purely proof-theoretic proof of the existence property for the full intuitionistic first-order predicate calculus, via natural deduction, in which commuting conversions are not needed. Such proof illustrates the potential of an atomic polymorphic system with only three generators of formulas – conditional and first and second-order universal quantifiers – as a tool for proof-theoretical studies.

Similar Items