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.