First Order Logic

Syntax

Symbols

We define the set C = {¬, ∧, ∨, →, ↔} of logical connectors (all different from each other), the set B = {‘(’, ‘)’, ‘,’} of opening and closing parentheses and comma (B is for brackets) disjoint from C, the set Q = {∀, ∃} of quantifiers disjoint from B and C, an infinite set U disjoint from B, C, and Q whose members are called constants, an infinite set V disjoint from B, C, Q, and U whose members are called variables, for all integer n > 0, an infinite set F_n disjoint from all other sets, whose members are called functions of arity n, and for all integer n ≥ 0, an infinite set P_n disjoint from all other sets, whose members are called predicates of arity n.

Symbols of FOL

The symbols of FOL are Sym_FOL = B ⋃ C ⋃ Q ⋃ U ⋃ V ⋃ (F₁ ⋃ F₂ ⋃ … ⋃ F_i ⋃ … ) ⋃ (P₀ ⋃ P₁ ⋃ … ⋃ P_i ⋃ … ).

Sometimes, predicates of arity 0 are distinguished as a separate set and are called propositions. Some other times, constants are presented as functions of arity 0.

As with propositions in propositional logic, we will write distinct constants, functions or predicates with distinct sequences of latin characters like so: Louis-XIV, motherOf, Person, etc.

Formulas

Defining formulas in FOL requires some additional definitions.

Terms

A term is either a constant or, if f is a function of arity n and t₁, … , t_n are terms, then f(t₁, … , t_n) is a term.

Formulas of FOL

Formulas are recursively built as the smallest set For_FOL such that:

• for all arity n, all p ∈ P_n, and all tuple of terms t₁, … , t_n, p(t₁, … , t_n) ∈ For_FOL;
• for all φ ∈ For_FOL, ¬φ ∈ For_FOL;
• for all φ, ψ ∈ For_FOL, (φ ∧ ψ) ∈ For_FOL;
• for all φ, ψ ∈ For_FOL, (φ ∨ ψ) ∈ For_FOL;
• for all φ, ψ ∈ For_FOL, (φ → ψ) ∈ For_FOL;
• for all φ, ψ ∈ For_FOL, (φ ↔ ψ) ∈ For_FOL;
• for all φ ∈ For_FOL and all x ∈ V, ∃x φ ∈ For_FOL;
• for all φ ∈ For_FOL and all x ∈ V, ∀x φ ∈ For_FOL.

Argument

In a term t = f(t₁, … , t_n) that consists of an n-ary function with n terms, t₁, … , t_n are called the arguments of t. In a formula φ = p(t₁, … , t_n) that consists of an n-ary predicate with n terms, t₁, … , t_n are called the arguments of φ.

Note that a predicate of arity 0 has an empty list of arguments.

Atom

An atom is a formula φ = p(t₁, … , t_n) that is reduced to a single predicate with its arguments.

Note that we use a light shading on formulas in order to clearly distinguish them from other syntactic constructs such as terms etc.

By convention, the following operator precedence is assumed: ∀ and ∃ has higher precedence than ¬; ¬ has higher precedence than ∧; ∧ has higher precedence than ∨; and ∨ has higher precedence than → and ↔. As a result, it is possible to write formulas by leaving parentheses implicit. Therefore, the following formulas are considered well formed:

∀z (∃x P(f(x),c) ∨ Q(y)) ∧ (R(z) ∨ ¬B) → D(y,z)
implicitly meaning ((∀z (∃x P(f(x),c) ∨ Q(y)) ∧ (R(z) ∨ ¬B)) → D(y,z))

∀x Airplane(x) → Vehicle(x) ∧ IsFlying(x)
implicitly meaning (∀x Airplane(x) → (Vehicle(x) ∧ IsFlying(x))), which is different in meaning from ∀x (Airplane(x) → (Vehicle(x) ∧ IsFlying(x)))

In addition to these usual definitions that apply to any logic, we introduce special syntactic forms that are generally useful for algorithms.

Literal

A literal L is a formula that is either an atom or the negation of an atom.

Prenex normal form (PNF)

A formula φ ∈ For_FOL is in prenex normal form (or PNF for short) if and only if φ = Q₁x₁ … Q_nx_n ψ for some n ∈ ℕ, some quantifiers Q₁, … , Q_n ∈ Q, some variables x₁, … , x_n ∈ V, and some formula ψ ∈ For_FOL where no quantifier appear in the quantifiers.

In a PNF Q₁x₁ … Q_nx_n ψ, the part Q₁x₁ … Q_nx_n is called the prefix and ψ is called the matrix.

Skolem normal form (SNF)

A formula φ ∈ For_FOL is in Skolem normal form (or SNF for short) if and only if φ is in PNF and its prefix only contains universal quantifiers.

Conjunctive normal form (CNF)

A formula φ ∈ For_FOL is in conjunctive normal form (or CNF for short) if and only if φ is in SNF and the matrix is a conjunction of disjunction of literals.

Free and bound variable occurrence

A variable x ∈ V occurs free or bound or both, or neither in a formula φ ∈ For_FOL according to the following recursive rules:

• if x does not occur in φ then it neither occurs free nor bound;
• if φ is a literal, x occurs free and not bound if and only if it occurs in φ;
• if φ = ¬ψ, x occurs free (respectively bound) if and only if it occurs free (respectively bound) in φ;
• if φ = (ψ₁ ∧ ψ₂) (or (ψ₁ ∨ ψ₂), or (ψ₁ → ψ₂), or (ψ₁ ↔ ψ₂)), then x occurs free (respectively bound) in φ if and only if it occurs free (respectively bound) in either ψ₁ or ψ₂.
• if φ = ∃y ψ (or ∀y ψ), then x occurs free in φ if and only if it occurs free in ψ and x is a different symbol than y; x occurs bound in φ if and only if x is y or it occurs bound in ψ.

Closed formula

A formula is closed if and only if no variable occurs free in it.

Semantics

Interpretations

Interpretations in FOL

An interpretation in FOL is a pair (Δ, 𝓘) such that:

• Δ is a non-empty set called the universe of the interpretation (or domain of discourse);

• 𝓘 is a function defined on the sets of constants, functions, and predicates such that:

  • for each c ∈ C, 𝓘(c) ∈ Δ;
  • for each n > 0 and each f ∈ F_n, 𝓘(f) : Δⁿ ⟶ Δ;
  • for each n ≥ 0 and each p ∈ P_n, 𝓘(p) : Δⁿ ⟶ {true, false}.

Satisfaction relation

Before defining the satisfaction relation, we need to introduce a new concept, namely assignment:

Variable assignment

Given an interpretation (Δ, 𝓘), a variable assignment (or simply assignment) is a mapping μ : V ⟶ Δ from variables to elements of the universe of interpretation.

For an interpretation (Δ, 𝓘), an assignment μ, a variable x ∈ V, and an element e ∈ Δ of the universe, we use the notation μ_x↦e to denote an assignment such that μ_x↦e(x) = e and for all y ∈ V\{x}, μ_x↦e(y) = μ(y).

Given an interpretation (Δ, 𝓘) and an assignment μ, we can define how every term and formula is interpreted with respect to the assignment as follows:

• for a constant c ∈ C, 𝓘[μ](c) = 𝓘(c);
• for a variable x ∈ V, 𝓘[μ](c) = μ(x);
• for n > 0, an n-ary function f ∈ F_n, and n terms t₁, … , t_n, 𝓘[μ](f(t₁, … , t_n)) = 𝓘(f)(𝓘[μ](t₁), … , 𝓘[μ](t_n));

• for all φ ∈ For_FOL, 𝓘[μ](φ) ∈ {true, false} and:

  • for n ≥ 0, an n-ary predicate p ∈ P_n, and n terms t₁, … , t_n, 𝓘[μ](p(t₁, … , t_n)) = 𝓘(p)(𝓘[μ](t₁), … , 𝓘[μ](t_n));
  • for φ ∈ For_FOL, 𝓘[μ](¬φ) = true if and only if 𝓘[μ](φ) = false;
  • for φ, ψ ∈ For_FOL, 𝓘[μ]((φ ∧ ψ)) = true if and only if 𝓘[μ](φ) = true and 𝓘[μ](ψ) = true;
  • for φ, ψ ∈ For_FOL, 𝓘[μ]((φ ∨ ψ)) = true if and only if 𝓘[μ](φ) = true or 𝓘[μ](ψ) = true (or both);
  • for φ, ψ ∈ For_FOL, 𝓘[μ]((φ → ψ)) = true if and only if 𝓘[μ](φ) = false or 𝓘[μ](ψ) = true (or both);
  • for φ, ψ ∈ For_FOL, 𝓘[μ]((φ ↔ ψ)) = true if and only if 𝓘[μ](φ) = 𝓘[μ](ψ);
  • for φ ∈ For_FOL and x ∈ V, 𝓘[μ](∃xφ) = true if and only if there is an element e ∈ Δ such that 𝓘[μ_x↦e](φ) = true;
  • for φ ∈ For_FOL and x ∈ V, 𝓘[μ](∀xφ) = true if and only if, for every element e ∈ Δ, 𝓘[μ_x↦e](φ) = true.

Given these definition, the Satisfaction relation is defined as follows:

Satisfaction relation in FOL

An interpretation (Δ, 𝓘) in FOL satisfies a formula φ (that is, ((Δ, 𝓘), φ) ∈ ⊨_FOL, or (Δ, 𝓘) ⊨_FOL φ) if and only if for any assignment μ : V ⟶ Δ, 𝓘[μ](φ) = true.

Properties of FOL

Complexity of FOL

FOL is semi-decidable.

Rewritability to CNF

Given any formula φ, there exists a formula ψ in CNF such that φ ⊨_FOL ψ and ψ ⊨_FOL φ.

Correspondence between the entailment problem and tautology

For any formulas φ, ψ ∈ For_FOL, φ ⊨_FOL ψ if and only if φ → ψ is a tautology.