Published online by Cambridge University Press: 22 January 2016
This paper is a sequel to Motohashi [4]. In [4], a series of theorems named “elimination theorems of uniqueness conditions” was shown to hold in the classical predicate calculus LK. But, these results have the following two defects : one is that they do not hold in the intuitionistic predicate calculus LJ, and the other is that they give no nice axiomatizations of some sets of sentences concerned. In order to explain these facts more explicitly, let us introduce some necessary notations and definitions. Let L be a first order classical predicate calculus LK or a first order intuitionistic predicate calculus LJ. n-ary formulas in L are formulas F(ā) in L with a sequence ā of distinct free variables of length n such that every free variable in F occurs in ā.