The method of axiomatic rejection for the intuitionistic propositional logic

We prove that the intuitionistic sentential calculus is -decidable (decidable in the sense of ukasiewicz), i.e. the sets of theses of Int and of rejected formulas are disjoint and their union is equal to all formulas. A formula is rejected iff it is a sentential variable or is obtained from other formulas by means of three rejection rules. One of the rules is original, the remaining two are ukasiewicz's rejection rules: by detachement and by substitution. We extensively use the method of Beth's semantic tableaux.To the memory of Jerzy SupeckiTranslated from the Polish by Jan Zygmunt. Preparation of this paper was supported in part by C.P.B.P. 08-15.