First-Order Logic

logic

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

The syntax is constructed from a signature $(\mathcal{F},\mathcal{P})$ and a set of variables $\mathcal{V}$.

The set of first-order logic formulas $\mathcal{P}\mathcal{F}$ over a signature $\mathcal{F},\mathcal{P}$ is defined as the smallest set such that:

• $P(t_1,\dots ,t_n)\in \mathcal{P}\mathcal{F}⟺P/n\in \mathcal{P}$ and $t_i$ are terms.
• $\top ,\perp \in \mathcal{P}\mathcal{F}$
• $\neg F,(F\ast G)\in \mathcal{P}\mathcal{F}$ for logical operators.
• $\forall xF,\exists xF\in \mathcal{P}\mathcal{F}$ for $x\in \mathcal{V}$ and $F\in \mathcal{P}\mathcal{F}$.

Semantics

The meaning of FOL formulas is defined using:

1. An interpretation $I=(\mathcal{U},{\cdot }^I)$.
2. A variable assignment $\sigma :\mathcal{V}\to \mathcal{U}$.
3. The valuation function ${\mathrm{val}}_{I,\sigma }$.

Satisfaction

A tuple $(I,\sigma )$ is called a model of a formula $F$ (written $I,\sigma \models F$) if ${\mathrm{val}}_{I,\sigma }(F)=1$.

Terms vs. Formulas

Terms represent objects in the universe and are evaluated to elements of $\mathcal{U}$, whereas formulas represent statements and are evaluated to truth values $\{0,1\}$.

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:

$$\underset{i=0}{\overset{\infty }{\bigvee }}{F}_i$$

where $F_i$ represents the condition that the loop terminates after exactly $i$ 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.