Formal Methods 101: First-Order Logic (FOL)

Introduction:

  • First-Order Logic extends Zero-Order Logic (or Propositional Logic) to include variables and quantifiers.
  • First-Order Logic operators are used to form expressions over variables. These expressions over variables are known as ‘predicates’. Predicates are Boolean-valued functions that return either TRUE or FALSE depending on the value assignments of their variables.
  • First-Order Logic is made of up Logical Symbols (Negations, Binary Connectives, and Quantifiers) and Non-Logical Symbols (Predicate Symbols).

Non-Logical Symbols:

  • Predicate Variable (symbol):
    • Ex. 1 – Predicate Variable (symbol) with a valence of 0: A
    • Ex. 2 – Predicate Variable (symbol) with a valence of 2: A(b,d)
    • A predicate variable is a Boolean-valued variable that may take on the value of TRUE (1) or FALSE (0). Therefore, the Predicate variable A may be either TRUE or FALSE.
    • A predicate may have N-arguments and is said to have valence (or arity, i.e. number of arguments) of between 0 and N; depending on the number of arguments. The argument values determine the whether the predicate variable evaluates to TRUE or FALSE.
  • Function:
    • Ex. Function: f(b,v)
    • This is in line with the standard definition of a function that is not required to return a Boolean value.

Logical Symbols:

  • Negation (NOT): ¬
    • Ex. Predicate: ¬A
    • This negation relation, means the negation (opposite) of the assigned Boolean-valued variable A is TRUE. (If A is assigned TRUE, the predicate expression ¬A evaluates to FALSE. If A is assigned FALSE, the predicate expression ¬A evaluates to TRUE
  • Conjunction (AND): ∧
    • Ex. Predicate: A ∧ B
    • This conjunction operator means the predicate is TRUE if and only if (iff) predicate variables A AND B are assigned the value of TRUE.
  • Disjunction (OR): ∨
    • Ex. Predicate: A ∨”B”
    • This conjunction operator means the predicate is TRUE if and only if (iff) predicate variables A OR B are assigned the value of TRUE.
  • Material Implication: →
    • Ex. Predicate: A→B
    • This material implication operator means if predicate variable A is TRUE, then predicate variable B is TRUE. (Note: it gives not information about what B is if A is not TRUE.)
    • Note: This predicate may be TRUE or FALSE depending on if it breaks the rules of the material implication operations.
  • Material Bijection: ↔
    • Ex. Predicate: A↔B
    • This material bijection operator means, if A is TRUE, then B is TRUE, and if B is TRUE, then A is TRUE, if A is FALSE, then B is FALSE, and if B is FALSE, then A is FALSE. (In other words the Boolean value for both A and B is never different.)
    • Note: This operator is equivalent to implication both ways; in other words (A→ B) ∧ (B ← A).
    • Note: This predicate may TRUE or FALSE depending on if it breaks the rules of the material bijection operations.

Order of operations for FOL:

  1. ¬ is evaluated first
  2. ∧ is evaluated next
  3. ∨ is evaluated next
  4. ∀ & ∃ quantifiers are evaluated next
  5. → is evaluated last (thus so is ↔)

Example FOL Predicate:

  • ∀B∃A ( (C(x,y)∧¬D)→((A∧E(t,z))∨F) )
  • This is read for all B, there exist an A, such that, C and not D, implies A and E or F.
  • As seen, FOL is very expressive. This can be used to build extensive complex models of the domains of discourse.