Loading...
Publication
The faithfulness of Fat: a proof-theoretic proof
| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 238.9 KB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
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 established quite recently via a model-theoretic argument based in
Kripke structures. In this paper we present a purely proof-theoretic proof
of faithfulness. As an application, we give a purely proof-theoretic proof of
the disjunction property of the intuitionistic propositional logic in which
commuting conversions are not needed.
Description
Keywords
Predicative polymorphism Faithfulness Natural deduction Intuitionistic proposicional calculus Disjunction property Strong normalization