Towards Automated Reasoning in Herbrand Structures

Herbrand structures have the advantage, computationally speaking, of being guided by the definability of all elements in them. A salient feature of the logics induced by them is that they internally

exhibit the induction scheme, thus providing a congenial, computationally-oriented framework for

formal inductive reasoning. Nonetheless, their enhanced expressivity renders any effective proof

system for them incomplete. Furthermore, the fact that they are not compact poses yet another prooftheoretic challenge. This paper offers several layers for coping with the inherent incompleteness and

non-compactness of these logics. First, two types of infinitary proof system are introduced—one

of infinite width and one of infinite height—which manipulate infinite sequents and are sound and

complete for the intended semantics. The restriction of these systems to finite sequents induces a

completeness result for finite entailments. Then, in search of effectiveness, two finite approximations

of these systems are presented and explored. Interestingly, the approximation of the infinite-width

system via an explicit induction scheme turns out to be weaker than the effective cyclic fragment of the

infinite-height system.