Lukas' Notes

Search titles, aliases and note text. Use # for tags.

First-Order Logic

2 min read

Definition

First-Order Logic

First-Order Logic (FOL) is a formal system used to represent and reason about propositions involving objects and their relationships. It extends propositional logic by incorporating quantifiers and predicates.

Syntax

Definition

Syntax of First-Order Logic

The syntax of first-order logic is defined by the inductive formation rules for formulas and terms.

Link to original

Semantics

The meaning of FOL formulas is defined using:

  1. An interpretation .
  2. A variable assignment .
  3. The valuation function .

Satisfaction

A tuple is called a model of a formula (written ) if .

Terms vs. Formulas

Terms represent objects in the universe and are evaluated to elements of , whereas formulas represent statements and are evaluated to truth values .

Limitations

While First-Order Logic is highly expressive, it has fundamental limitations when used as a specification language for complex systems:

Finiteness of Formulas: Standard FOL only allows for formulas of finite length. This means that properties requiring an “infinite disjunction” or “infinite conjunction” cannot be expressed.

Expressing Loops and Recursion: A critical limitation in the context of program verification is the inability to express the weakest precondition of a loop (e.g., a while loop) as a single FOL formula.

To define the semantics of a loop, one typically needs to account for an unknown number of iterations. This results in an infinite disjunction:

where represents the condition that the loop terminates after exactly runs. Since FOL formulas must be finite, this “infinite formula” exists only at a meta-level and cannot be used within the logic itself.

Higher-Order Requirements: To reason about such properties (e.g., termination, reachability in graphs, or arbitrary recursion), one often requires Higher-Order Logic or fixed-point logics. These systems allow for quantification over sets, predicates, or functions, enabling the definition of recursive properties that are unreachable in standard First-Order Logic.

Backlinks