First-Order Logic

First-order logic extends propositional logic in several ways. Along with the propositional connectives ¬ (negation), ∧ (conjunction), ∨ (disjunction), ⇒ (implication), and ⇔ (equivalence), we find = (identitity), ∀ (universal quantification), and ∃ (existential quantification). Whereas propositional logic has only one type of expression: the formula, first-order logic has two types: the term and the formula. A term describes an object in the universe of discourse, and a formula is a statement regarding such objects.

Syntax

The language of first-order logic contains the following symbols:

infinitely many variables,
the connectives ¬, ∧, ∨, ⇒, ⇔, and the quantifiers ∀, and ∃,
parentheses (, ) and comma ,,
the identity symbol =,
constant symbols,
function symbols,
relation symbols (a.k.a. predicate symbols).

Each function and relation symbol has an arity property which tells us how many arguments the function or relation takes. It is assumed that different sets of symbols are pairwise disjoint, so for example, there is no symbol which is both a constant and a relation. Some authors simplify things by considering constants to be functions with arity zero. Note that first-order languages differ only in the sets of constant, function, and relation symbols (a.k.a. the non-logical symbols).

The set of first-order logic terms, T, is the smallest one satisfying

for all x such that x is a variable then x ∈ T,
for all c such that c is a constant symbol then c ∈ T,
for all f such that f is a function symbol with arity n (n-ary) and t₁, ..., t_n ∈ T, then f(t₁, ..., t_n) ∈ T.

The set of first-order logic formulas, F, is the smallest one satisfying

for all r such that r is a relation symbol with arity n (n-ary) and t₁, ..., t_n ∈ T, then r(t₁, ..., t_n) ∈ F.
for all φ and ψ, if φ and ψ ∈ F, then ¬φ ∈ F, φ∧ψ ∈ F, φ∨ψ ∈ F, φ⇒ψ ∈ F, and φ⇔ψ ∈ F,
for all φ such that φ ∈ F then (φ) ∈ F,
for all x, φ such that φ ∈ F and x a variable, then ∀xφ ∈ F, ∃xφ ∈ F,
for all t₁, t₂ such that t₁ and t₂∈ T, then t₁=t₂ ∈ F.

Semantics

To provide meaning for a first-order language we need interpretations for the non-logical symbols. If we have a language L which has constants from the set C, functions from the set F, and relations from the set R, then we can write L=C∪F∪R. A model for the language L is a structure comprising a universe of discourse and interpretations for all of the constants, functions, and relations. We can write M=(M,...,r,...,f,...,c,...) where M is the universe of discourse for M, and

for each c∈C we have a c∈M,
for each f∈F with arity n, we have a f:Mⁿ→M,
for each r∈R with arity n, we have a r∈Mⁿ,

Here c,f,r are the interpretations of c,f,r respectively. As a convention we will write M for the universe of discourse of model M, and c,f,r for the interpretations of c,f,r.

Example: Consider the axioms for an equivalence relation r

∀x rxx (reflexivity)
∀x∀y rxy ⇒ ryx (symmetry)
∀x∀y∀z (rxy ∧ ryz) ⇒ rxz (transitivity)

Now take the set of natural numbers, N, to be the universe of discourse, and if we take ≤ to the be interpretation of r, then we have a model (N, ≤) for the language of these axioms.

Truth is defined for sentences of a given language so we must deal with free variables. There are two ways to do so:

extend the language with a new constant for each memeber of the universe of discourse and replace variables with the new constants, or
assign elements of the universe of discourse to variables with the help of mappings.

The first option is given in Doets, and the second in Deransart and Maluszynski.

The Doets Method

If M is a model for the language L, then the M-language L_M is an extension of L by adding the elements of the universe of discourse as constant symbols. These new symbols are interpreted as themselves. The terms, formulas, and sentence of L_M are called M-terms, M-formulas, and M-sentences.

If M is a model and t is a ground M-term then the value of t, written t^M, is given by the following rules:

if t=c (a constant symbol) then t^M=c,
if t=c (a newly added constant symbol) then t^M=c,
if t=f(t₁,...,t_n) (a function application) then t^M=f(t₁^M,...,t_n^M).

If M is a model and φ is a M-sentence then the truth of φ in M, written M⊨φ, is given by the following rules:

if φ=r(t₁,...,t_n), then M⊨φ iff r(t₁^M,...,t_n^M)
if φ=t₁=t₂, then M⊨φ iff t₁^M=t₂^M
if φ=¬ψ, then M⊨φ iff M⊯ψ
if φ=ψ₁∧ψ₂, then M⊨φ iff M⊨ψ₁ and M⊨ψ₂. Similarly for the other logical connectives (∨, ⇒, ⇔)
if φ=∀xψ, then M⊨ψ iff for all v∈M, M⊨ψ{x/v}
if φ=∃xψ, then M⊨ψ iff for some v∈M, M⊨ψ{x/v}

Here ψ{x/v} means all free occurences of the variable x are replaced by the new constant v.

To turn a formula of the language L_M into a M-sentence we need a M-assignment which is just a mapping from the set of variables to the set of constant symbols. The set of free variables in the formula must be a subset of the domain of the M-assignment. When we apply a M-assignment, we replace each free variable by it's image. If α is a M-assignment, and φ a L_M formula, the φα is a M-sentence.

The M-assignment α satisfies the forumla φ in the model M if M⊨φα. A formula is said to be satisfiable if it can be satisfied by some assignment in some model.

The formula φ is valid or true in M, written, M if M⊨φ, if it is satisfied by every M-assignment in M.

If Φ is a set of formulas then M is a model of Φ if for all φ∈Φ, M⊨φ.

The formula φ is logically valid, written ⊨φ, if it is valid in every model.

If Φ is a set of formulas then φ is a logical consequence of Φ, or φ is follows logically from Φ, written Φ⊨φ, if φ is valid in every model of Φ.

If φ and ψ are formulas, then φ is logically equivalent to ψ, written φ~ψ if ⊨φ⇔ψ

The Deransart and Maluszynski Method

Here we assign elements of the universe of discourse to variables with the help of mappings called valuations.

If M is a model for the language L, t is a term, and ν is a valuation for the variables in t, then the value of t, written t^M,ν, is given by the following rules:

if t=c (a constant symbol) then t^M,ν=c,
if t=v (a variable symbol) then t^M,ν=ν(v),
if t=f(t₁,...,t_n) (a function application) then t^M,ν=f(t₁^M,ν,...,t_n^M,ν).

If M is a model and φ is a formula and ν is a valuation for the variables in φ, then the truth of φ in M and ν, written M,ν⊨φ, is given by the following rules:

if φ=r(t₁,...,t_n), then M,ν⊨φ iff r(t₁^M,ν,...,t_n^M,ν)
if φ=t₁=t₂, then M,ν⊨φ iff t₁^M,ν=t₂^M,ν
if φ=¬ψ, then M,ν⊨φ iff M,ν⊯ψ
if φ=ψ₁∧ψ₂, then M,ν⊨φ iff M,ν⊨ψ₁ and M,ν⊨ψ₂. Similarly for the other logical connectives (∨, ⇒, ⇔)
if φ=∀xψ, then M,ν⊨ψ iff for all v∈M, M,{x/v}ν⊨ψ
if φ=∃xψ, then M⊨ψ iff for some v∈M, M,{x/v}ν⊨ψ

Here {x/v}ν denotes the function ν' defined as ν'(y)=x if x=y, otherwise ν(y).

The valuation ν satisfies the forumla φ in the model M if M,ν⊨φ. A formula is said to be satisfiable if it can be satisfied by some valuation in some model.

The formula φ is valid or true in M, written, M if M⊨φ, if it is satisfied by every valuation in M.

If Φ is a set of formulas then M is a model of Φ if for all φ∈Φ, M⊨φ.

The formula φ is logically valid, written ⊨φ, if it is valid in every model.

If Φ is a set of formulas then φ is a logical consequence of Φ, or φ is follows logically from Φ, written Φ⊨φ, if φ is valid in every model of Φ.

If φ and ψ are formulas, then φ is logically equivalent to ψ, written φ~ψ if ⊨φ⇔ψ

References

Deransart, Pierre, Maluszynski, Jan. A Grammatical View of Logic Programming. MIT Press, 1993.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.