Herbrand Universe

Herbrand Universe: It is a good exercise to determine for given formulae if they are satisfied/valid on specific L-structures, and to determine, if they exist, models for them. A good starting point in this task, and useful for a number of other reasons, is the Herbrand Universe for this set of formulae. Say that {F01 .. F0n} are the individual constants in the formulae [if there are no such constants, then introduce one, say, F0]. Say that {F1 .. Fm} are all the non 0-ary function symbols occurring in the formulae. Then the set of (constant) terms obtained starting from the individual constants using the non 0-ary functions, is called the Herbrand Universe for these formulae.
For example, given the formula (P x A) OR (Q y), its Herbrand Universe is just {A}. Given the formulae (P x (F y)) OR (Q A), its Herbrand Universe is {A (F A) (F (F A)) (F (F (F A))) ...}.

Reduction to Clausal Form: In the following we give an algorithm for deriving from a formula an equivalent clausal form through a series of truth preserving transformations. We can state an (unproven by us) theorem:
Theorem: Every formula is equivalent to a clausal form
We can thus, when we want, restrict our attention only to such forms.

Deduction
An Inference Rule is a rule for obtaining a new formula [the consequence] from a set of given formulae [the premises]. A most famous inference rule is Modus Ponens:

When we introduce inference rules we want them to be Sound, that is, we want the consequence of the rule to be a logical consequence of the premises of the rule. Modus Ponens is sound. But the following rule, called Abduction , is not:

is not. For example:

gives us a conclusion that is usually, but not always true [John takes a shower even when it is not raining].
A Logic or Deductive System is a language, plus a set of inference rules, plus a set of logical axioms [formulae that are valid].
A Deduction or Proof or Derivation in a deductive system D, given a set of formulae GAMMA, is a a sequence of formulae B1 B2 .. Bn such that:

• • for all i from 1 to n, Bi is either a logical axiom of D, or an element of GAMMA, or is obtained from a subset of {B1 B2 .. Bi-1} by using an inference rule of D.

In this case we say that Bn is Derived from GAMMA in D, and in the case that GAMMA is empty, we say that Bn is a Theorem of D.