On a generalization of Herbrand's theorem

Candidate: Policriti,Alberto

Abstract

In this thesis we prove a generalized version of Herbrand's theorem. Our result guarantees the existence of a semi-decision procedure a la Herbrand for testing unsatisfiability with respect to a give theory T, in which the decision procedure used at the ground level depends upon T. This is opposed to the classical case in which procedure used at the ground level is simply a test for propositional satisfiability. The problem of finding suitable analogues for the general case of the exhaustive search procedures is also tackled, and one such generalization is proposed. The underlying motivation for this study was to find theoretical results that could provide the basis for a set-theoretic proof checker. Thus, the case of set theory is considered in more detail. In particular, decidability and undecidability results for classes of set-theoretic, purely universal formulae are proved.