New Directions in Mechanical Theorem Proving

Abstract

The exclusive use of first-order logic in mechanical theorem proving systems effectively prevents the formulation of most interesting problems for input to them, while the use of higher-order logic would not. Yet if the higher-order notion of logical validity is construed, following Henkin. as “true under all interpretations, standard or not”, as is advocated here, then full omega-order logic still has a mechanical proof procedure. Furthermore, since Takeuti’s conjecture is now known to be correct, this procedure can be given the direct “semantic tableau” form. A version of this procedure is presented, based on SchUtte’s but exploiting Hilbert’s epsilon operator.