Skolemization and Herbrand's theorem are powerful tools in first-order logic. They help simplify complex formulas by removing existential quantifiers and replacing them with functions or constants. This process makes automated theorem proving easier and more efficient.

These concepts are crucial for understanding how to manipulate and analyze first-order logic formulas. They provide a foundation for proving unsatisfiability and exploring the relationships between different logical statements in automated reasoning systems.

Skolemization: Process and Purpose

Eliminating Existential Quantifiers

• Skolemization is a process of eliminating existential quantifiers from a first-order logic formula by replacing existentially quantified variables with Skolem functions or Skolem constants
• Skolem functions are introduced to replace existentially quantified variables that are within the scope of universally quantified variables
  • The arity of a Skolem function is determined by the number of universally quantified variables in whose scope the existentially quantified variable appears
• Skolem constants are used to replace existentially quantified variables that are not within the scope of any universally quantified variables

Transforming Formulas for Automated Theorem Proving

• The purpose of Skolemization is to convert a formula into an equisatisfiable formula in prenex normal form with only universal quantifiers
  • Prenex normal form means that all quantifiers appear at the beginning of the formula, followed by a quantifier-free matrix
• Skolemized formulas are more suitable for automated theorem proving and other applications
• Skolemization preserves satisfiability
  • If the original formula is satisfiable, the Skolemized formula is also satisfiable
  • If the Skolemized formula is unsatisfiable, the original formula is also unsatisfiable

Eliminating Existential Quantifiers

Converting to Prenex Normal Form

• To apply Skolemization, first convert the formula to prenex normal form
  • Move all quantifiers to the beginning of the formula
  • Ensure the formula is followed by a quantifier-free matrix

Replacing Existentially Quantified Variables

• For each existentially quantified variable, determine if it is within the scope of any universally quantified variables
  • If it is, replace the existentially quantified variable with a Skolem function that takes the universally quantified variables as arguments
  • If it is not, replace the existentially quantified variable with a Skolem constant
• Remove the existential quantifiers from the formula, as the variables have been replaced by Skolem functions or constants

Resulting Skolem Normal Form

• The resulting formula is in Skolem normal form
  • Contains only universally quantified variables
  • Equisatisfiable with the original formula

Herbrand's Theorem: Statement and Implications

Unsatisfiability and Ground Instances

• Herbrand's theorem states that a set of clauses (disjunctions of literals) is unsatisfiable if and only if there exists a finite unsatisfiable set of ground instances of those clauses
• A ground instance of a clause is obtained by replacing all variables in the clause with terms from the Herbrand universe
  • The Herbrand universe is the set of all possible ground terms constructed from the function symbols and constants in the language

Implications for Automated Theorem Proving

• Herbrand's theorem provides a basis for proving the unsatisfiability of a set of clauses by showing that a finite set of ground instances is unsatisfiable
• The theorem implies that if a set of clauses is unsatisfiable, there must be a finite proof of its unsatisfiability
  • This is important for automated theorem proving

Relation to Completeness and Compactness

• Herbrand's theorem is closely related to the completeness of first-order logic
  • Completeness means that if a formula is logically valid, then it can be proven using a formal proof system
• The theorem is also related to the compactness theorem
  • Compactness states that if every finite subset of a set of formulas is satisfiable, then the entire set is satisfiable

Proving Unsatisfiability with Herbrand's Theorem

Skolemizing the Clauses

• To use Herbrand's theorem to prove the unsatisfiability of a set of clauses, first Skolemize the clauses to eliminate existential quantifiers
  • Replace existentially quantified variables with Skolem functions or constants

Generating Ground Instances

• Generate ground instances of the Skolemized clauses by replacing variables with terms from the Herbrand universe
  • The Herbrand universe is the set of all possible ground terms constructed from the function symbols and constants in the language

Searching for a Finite Unsatisfiable Set

• Search for a finite unsatisfiable set of ground instances
  • This can be done using various proof methods, such as resolution or tableau
• If a finite unsatisfiable set of ground instances is found, then by Herbrand's theorem, the original set of clauses is unsatisfiable

Herbrand's Procedure

• The process of generating ground instances and searching for a contradiction is called Herbrand's procedure or the Herbrand method
  • This procedure is a key component of many automated theorem proving systems