On logic through relations without boundaries

October 22, 2017

On logic through relations without boundaries

HERBRAND LOGIC

Herbrand Logic is an alternative to Relational Logic, in which we can name infinitely many objects with a finite vocabulary.

· Function constants are similar to relation constants in that they are used in forming complex expressions by combining them with an appropriate number of arguments.

· Based on the number of arguments they take, function constants can be unary, binary, ternary, n-ary.

MATHEMATICAL FOUNDATIONS
OF HERBRAND LOGIC

Herbrand's Theorem

Herbrand's theorem is a fundamental result of mathematical logic obtained in 1930 by the young French mathematician Jacques Herbrand (1908-1931). In essence, it allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular.

is valid if and only if there exists a finite sequence of terms t_i,j, possibly in an expansion of the language, with

Informally: a formula A in prenex form containing existential quantifiers only is provable (valid) in first-order logic if and only if a disjunction composed of substitution instances of the quantifier-free subformula of A is a tautology (propositionally derivable).

Besides, the restriction to formulas in prenex form containing only existential quantifiers does not limit the generality of the theorem, because formulas can be converted to prenex form and their universal quantifiers can be removed by Herbrandization. Conversion to prenex form can be avoided, if structural Herbrandization is performed. Herbrandization can be avoided by imposing additional restrictions on the variable dependencies allowed in the Herbrand disjunction.

Generalizations of Herbrand's theorem

• Herbrand's theorem has been extended to higher‑order logic by using expansion-tree proofs. The deep representation of expansion-tree proofs corresponds to a Herbrand disjunction, when restricted to first-order logic.

• Herbrand disjunctions and expansion-tree proofs have been extended with a notion of cut. Due to the complexity of cut‑elimination, Herbrand disjunctions with cuts can be non‑elementarily smaller than a standard Herbrand disjunction.

• Herbrand disjunctions have been generalized to Herbrand sequents, allowing Herbrand's theorem to be stated for sequents: "a Skolemized sequent is derivable iff it has a Herbrand sequent".

PRENEX NORMAL FORM

A formula of the predicate calculus is in Prenex Normal Form (PNF), if it is written as a string of quantifiers (referred to as the prefix) followed by a quantifier-free part (referred to as the matrix).

Every formula in classical logic is equivalent to a formula in Prenex Normal Form (PNF). For instance, if ϕ(y),ψ(z),and ρ(x) are quantifier-free formulas with the free variables shown then