Studying provability in implicational intuitionistic logic: the formula tree approach

Sabine Broda and Luís Damas

Wollic 2002


We use an alternative graphical representation for formulas in implicational intuitionistic logic in order to obtain and demonstrate results concerning provability. We demonstrate the adequateness of the method in this area, showing that one can easily recognize and prove new results and simplify the proofs of others. As such, we extend a known class of formulas for which uniqueness of beta-eta-normal proofs. We also give a precise characterization of the set of provable monatomic formulas and obtain as a corollary a necessary condition for intuitionistic theorems in general.