Technical Report: DCC-2004-01

The Formula-Tree Proof Method

Sabine Broda and Luís Damas

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {sbb,luis}
January 2004


We define an alternative representation for types in the simply typed $\lambda$-calculus or equivalently for formulas in the implicational fragment of intuitionist propositional logic, which gives us a better insight on the nature of a types structure and its relation to the structure of the set of its normal inhabitants. Based on this representation of a type $\varphi$, called its formula-tree, we define the notion of a valid proof-tree. Any such valid proof-tree represents a finite set of normal inhabitants of $\varphi$ and every normal inhabitant corresponds to exactly one valid proof-tree, constructable with the primitive parts in the formula-tree of $\varphi$. Precise algorithms are given to establish this relation. This method can be used to easily recognize and prove results concerning inhabitation/provability.