Herbrandization

Herbrandization

The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem (Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem (Herbrand 1930).

As with Skolemization, the resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is.

Let F be a formula in the language of first-order logic. We may assume that F contains no variable that is bound by two different quantifier occurrences, and that no variable occurs both bound and free. (That is, F could be relettered to insure these conditions, in such a way that the result is an equivalent formula).

The "Herbrandization" of F is then obtained as follows:

* First, replace any free variables in F by constant symbols.

* Second, delete all quantifiers on variables that are either (1) universally quantified and within an even number of negation signs, or (2) existentially quantified and within an odd number of negation signs.

* Finally, replace each such variable v with a function symbol f_v(x_1,dots,x_k), where x_1,dots,x_k are the variables that are still quantified, and whose quantifiers govern v.

For instance, consider the formula F := forall y exists x [R(y,x) wedge egexists z S(x,z)] . There are no free variables to replace. The variables y,z are the kind we consider for the second step, so we delete the quantifiers forall y and exists z. Finally, we then replace y with a constant c_y (since there were no other quantifiers governing y), and we replace z with a function symbol f_z(x):

: F^H = exists x [R(c_y,x) wedge eg S(x,f_z(x))] .

The "Skolemization" of a formula is obtained similarly, except that in the second step above, we would delete quantifiers on variables that are either (1) existentially quantified and within an even number of negations, or (2) universally quantified and within an odd number of negations. Thus, considering the same F from above, its Skolemization would be:

: F^S = forall y [R(y,f_x(y)) wedge egexists z S(f_x(y),z)] .

To understand the significance of these constructions, see Herbrand's theorem or the Löwenheim-Skolem theorem.

References

* Skolem, T. "Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: A simplified proof of a theorem by L. Löwenheim and generalizations of the theorem". In (van Heijenoort 1967), 252-63.

* Herbrand, J. "Investigations in proof theory: The properties of true propositions". In (van Heijenoort 1967), 525-81.

* van Heijenoort, J. "From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931". Harvard University Press, 1967.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Herbrand's theorem — is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). [J. Herbrand: Recherches sur la theorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et… …   Wikipedia

  • First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… …   Wikipedia

  • Prenex normal form — A formula of the predicate calculus is in prenex[1] normal form if it is written as a string of quantifiers followed by a quantifier free part (referred to as the matrix). Every formula in classical logic is equivalent to a formula in prenex… …   Wikipedia

  • Skolem normal form — A formula of first order logic is in Skolem normal form (named after Thoralf Skolem) if it is in conjunctive prenex normal form with only universal first order quantifiers. Every first order formula can be converted into Skolem normal form while… …   Wikipedia

  • List of mathematics articles (H) — NOTOC H H cobordism H derivative H index H infinity methods in control theory H relation H space H theorem H tree Haag s theorem Haagerup property Haaland equation Haar measure Haar wavelet Haboush s theorem Hackenbush Hadamard code Hadamard… …   Wikipedia

  • Davis–Putnam algorithm — The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first order logic formula using a resolution based decision procedure for propositional logic. Since the set of valid first order formulas… …   Wikipedia

  • DPLL algorithm — The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF SAT problem. It was introduced in …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”