Completeness and Cut-elimination in the Intuitionistic Theory of Types-Part 2

摘要

This article aims to extend some results in [3], using some new proof-theoretic tools, as well as to modify an erroneous construction in one of the cases of the proof of the main theorem. Our work also establishes some new correlations between formal properties of the sequent calculus of the intuitionistic theory of types and tableaux.