The faithfulness of atomic polymorphism

Ferreira, Fernando; Ferreira, Gilda

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

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
faithfulness.pdf		97.35 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Fernando

Ferreira, Gilda

Abstract(s)

It is known that the full intuitionistic propositional calculus can be embedded into the atomic polymorphic system Fat, a calculus with only two connectives: the conditional and the second-order universal quantifier. The embedding uses a translation of formulas due to Prawitz and relies on the so-called property of instantiation overflow. In this paper, we show that the previous embedding is faithful i.e., if a translated formula is derivable in Fat, then the original formula is already derivable in the propositional calculus.