Predicate Logic

Predicate Logic
Propositional logic can express simple ideas with no quantitative notions or qualifications, and is also good enough for describing digital logic circuits. For more complex ideas, propositional logic is not sufficient, as shown in the following example.

Example. Consider the following statements: Every time the car brake pedal is pressed by the driver of the car, the car stops within 8 seconds. Because Mercedes Benz E320 is a car, whenever the driver of the Mercedes Benz E320 presses its brake pedal, the Mercedes Benz E320 stops within 8 seconds.
P denotes “Every time the car brake pedal is pressed by the driver of the car, the car stops within 8 seconds.”
Q denotes “Mercedes Benz E320 is a car.”
R denotes “Whenever the driver of the Mercedes Benz E320 presses its brake pedal, the Mercedes Benz E320 stops within 8 seconds.”

However, R is not a logical consequence of P and Q in the framework of propositional logic.

To handle these statements, we introduce predicate logic, which has the concepts of terms, predicates, and quantifiers. First, we define functions and terms.
Function: A function is a mapping from a list of constants to a constant. Terms: Terms are defined inductively as follows:
1. Every constant or variable is a term.
2. If f is an n-place function symbol and x1, . . . , xn are terms, then f (x1, . . . , xn) is a term.
3. All terms are generated using the above rules.

Next, we define predicates and atoms.

Predicate: A predicate is a mapping from a list of constants to either T or F.

Atoms or Atomic Formulas: If P is an n-place predicate symbol and x1, . . . , xn are terms, then P(x1, . . . , xn) is an atom or atomic formula. The special symbol ∀ is the universal quantifier, and the special symbol ∃ is the existential quantifier. If x is a variable, then ∀x means “for all x,” (or “for every x”) and ∃x means “there exists an x.” We also need to define the notions of bound and free variables and variable occurrences.

Bound and Free Variable Occurrences: Given a formula, an occurrence of a variable x is a bound occurrence iff the occurrence is within the scope of a quantifier
over this variable or the occurrence immediately follows this quantifier, that is, x appears in a subformula of the form (∀x)F or (∃x)F. Given a formula, an occurrence of a variable is a free occurrence iff this occurrence is not bound.

Often we omit the parentheses surrounding the quantifier and the quantified variable. Bound and Free Variables: Given a formula, a variable is bound iff at least one occurrence of this variable is bound. Given a formula, a variable is free iff at least one occurrence of this variable is free. Now we are ready to define formulas in predicate logic.

Well-Formed Formulas: Well-formed formulas in predicate logic are defined recursively as follows:
1. An atom is a formula.
2. If F is a formula, then (¬F) is a formula.
3. If F and G are formulas, then (F op G) is a formula, where op is ∨,∧,→, or ↔.
4. If F is a formula and x is a free variable in F, then (∀x)F and (∃x)F are formulas.
5. All formulas are generated using a finite number of the above rules.

Example. Consider the above car example. Let BRAKE STOP signify “Every time the car brake pedal is pressed by the driver of the car, the car stops within 8 seconds.” We have the following predicate logic formulas:

(∀x)CAR(x) → BRAKE STOP(x))
CAR(MercedesBenzE320).

Since (∀x)(CAR(x) → BRAKE STOP(x)) is true for all x, replacing x by “MercedesBenzE320,” we have
(CAR(MercedesBenzE320) → BRAKE STOP(MercedesBenzE320)) is true.

This means that
¬(CAR(MercedesBenzE320) ∨ BRAKE STOP(MercedesBenzE320)) is true, but
¬(CAR(MercedesBenzE320)) is false since CAR(MercedesBenzE320) is true.

Therefore, BRAKE STOP(MercedesBenzE320) must be true.

In propositional logic, an interpretation of a formula is an assignment of truth values to the atoms. Since a predicate-logic formula may contain variables, in order to define an interpretation, we need to specify the domain and an assignment to constants, functions symbols, and predicate symbols in the formula.