ABSTRACT

First of all, we are looking for normal forms, hence each formula should be equivalent to a formula in some (in an intuitionistic basic theory). Moreover, classically should neither be more nor less than n„, that is, classically n„ and <!>„ should be equivalent1. Natural closure conditions would increase the usability of our classes and hence are desirable. Finally, truth-predicates (in other word, universal or complete formulae) for which are itself in should exist.