 In many sorted logic, the conclusion is easily obtained from these hypotheses by using a deductive calculus (see  section 2).  Therefore, the argument is formally correct, once we accept the problematic hypothesis \(\alpha\). In  section 2.4  we rewrite the argument to use theorem provers LEO-II and LEO-III.