The faithfulness of Fat: a proof-theoretic proof

It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system Fat, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was esta...

Full description

Bibliographic Details
Main Author: Ferreira, Fernando (author)
Other Authors: Ferreira, Gilda (author)
Format: article
Language:eng
Published: 2021
Subjects:
Predicative polymorphism
Faithfulness
Natural deduction
Intuitionistic proposicional calculus
Disjunction property
Strong normalization
Online Access:http://hdl.handle.net/10400.2/10490
Country:Portugal
Oai:oai:repositorioaberto.uab.pt:10400.2/10490

Internet

http://hdl.handle.net/10400.2/10490

Similar Items