On Herbrand Theorem

Alexander V. Lyaletski

1st-order classical logic (with functional symbols and without equality) is considered. A new formulation of Herbrand theorem is suggested in such a form that the forms A, B, and C [1] can be obtained as consequences of the one. For this, an original notion of admissible substitution [2] is generalized in case of a set of arbitrary formulas.

Let S be a finite set of formulas. Herbrand quasi-universe HQ(S) for S is the following minimal set of terms: (i) for any constant c from formulas belonging to S and for any variable x of a positive quantifier from formulas belonging to S it is true that c, x ∈ HQ(S); (ii) if t_{1}, ..., t_{m} ∈ S and a m-arity functional symbol f occurs in formulas from S, then f(t_{1},...,t_{m}) ∈ HQ(S).

THEOREM. A finite set S of formulas is unsatisfiable IFF there are a finite set S′ of variants F_{1},...,F_{n} of formulas from S and a substitution σ of terms from HQ(S′) for all variables bounded by negative quantifiers from formulas belonging to S′ such that: (1) formulas F_{i} and F_{j} have common bounded variables only if they are variants of a same formula from S and satisfy a certain condition;

(2) σ is an admissible substitution for S′; (3) a formula (M_{1} ∗ σ) & ... & (M_{n} ∗ σ) considered as a formula of the proposition calculus is false, where M_{1},...,M_{n} are obtained by elimination of all quantifiers in F_{1},...,F_{n}, respectively, and M_{i} ∗ σ denotes the result of application of σ to M_{i} (i = 1,...,n).

1. Herbrand, J.: Recherches sur la Theorie de la Demonstration. Travaux de la Societe des Sciences et de Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques, 1930, volume 33. 2. Lyaletski, A.V.: Variant of Herbrand Theorem for Formulas in Prefix Form (in Russian). Kibernetika, 1981, 1, 112–116.

Address: Cybernetics Department, Taras Shevchenko University of Kyiv, 6, Glushkov avenue, 03127 Kyiv, Ukraine

E-mail: lav@tc.unicyb.kiev.ua