Abstract

The original decision criterion and method of the combined calculus, presented by D. Hilbert and W. Ackermann, and applied by later logicians, are illuminating, but also go seriously awry and lead the universality and preciseness of the combined calculus to be damaged. The main error is that they confuse the two levels of the combined calculus in the course of calculating. This paper aims to resolve the problem through dividing the levels of the combined calculus, introducing a mixed operation mode, and therefore finding a normal-form decision method approximated by that in sentential logic. Finally, this paper provides a more precise proof of Hauber’s theorem by using the normal-form decision method of the combined calculus.