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.
The language of first-order logic contains the following symbols:
¬
, ∧
, ∨
, ⇒
, ⇔
,
and the quantifiers ∀
, and ∃
,(
, )
and comma ,
,=
,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
x
such that x
is a variable then x
∈ T,c
such that c
is a constant symbol then c
∈ T,f
such that f
is a function symbol with arity n (n-ary)
and t_{1}, ..., t_{n}
∈ T, then f(t_{1}, ..., t_{n})
∈ T.The set of first-order logic formulas, F, is the smallest one satisfying
r
such that r
is a relation symbol with arity n (n-ary)
and t_{1}, ..., t_{n}
∈ T,
then r(t_{1}, ..., t_{n})
∈ F.φ
and ψ
, if φ
and ψ
∈ F, then
¬φ
∈ F,
φ∧ψ
∈ F,
φ∨ψ
∈ F,
φ⇒ψ
∈ F,
and φ⇔ψ
∈ F,φ
such that φ
∈ F then (φ)
∈ F,x
, φ
such that φ
∈ F and x
a variable,
then ∀xφ
∈ F, ∃xφ
∈ F,t_{1}
, t_{2}
such that
t_{1}
and t_{2}
∈ T,
then t_{1}=t_{2}
∈ F.
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
c∈C
we have a c∈M
,
f∈F
with arity n, we have a f:M^{n}→M
,
r∈R
with arity n, we have a r∈M^{n}
,
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:
The first option is given in Doets, and the second in Deransart and Maluszynski.
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:
t=c
(a constant symbol) then t^{M}=c
,
t=c
(a newly added constant symbol) then t^{M}=c
,
t=f(t_{1},...,t_{n})
(a function application)
then t^{M}=f(t_{1}^{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:
φ=r(t_{1},...,t_{n})
, then
M⊨φ
iff r(t_{1}^{M},...,t_{n}^{M})
φ=t_{1}=t_{2}
, then
M⊨φ
iff t_{1}^{M}=t_{2}^{M}
φ=¬ψ
, then
M⊨φ
iff M⊯ψ
φ=ψ_{1}∧ψ_{2}
, then
M⊨φ
iff M⊨ψ_{1}
and M⊨ψ_{2}
.
Similarly for the other logical connectives (∨, ⇒, ⇔
)
φ=∀xψ
, then
M⊨ψ
iff for all v∈M
, M⊨ψ{x/v}
φ=∃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 ⊨φ⇔ψ
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:
t=c
(a constant symbol) then t^{M,ν}=c
,
t=v
(a variable symbol) then t^{M,ν}=ν(v)
,
t=f(t_{1},...,t_{n})
(a function application)
then t^{M,ν}=f(t_{1}^{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:
φ=r(t_{1},...,t_{n})
, then
M,ν⊨φ
iff r(t_{1}^{M,ν},...,t_{n}^{M,ν})
φ=t_{1}=t_{2}
, then
M,ν⊨φ
iff t_{1}^{M,ν}=t_{2}^{M,ν}
φ=¬ψ
, then
M,ν⊨φ
iff M,ν⊯ψ
φ=ψ_{1}∧ψ_{2}
, then
M,ν⊨φ
iff M,ν⊨ψ_{1}
and M,ν⊨ψ_{2}
.
Similarly for the other logical connectives (∨, ⇒, ⇔
)
φ=∀xψ
, then
M,ν⊨ψ
iff for all v∈M
, M,{x/v}ν⊨ψ
φ=∃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 ⊨φ⇔ψ
Deransart, Pierre, Maluszynski, Jan. A Grammatical View of Logic Programming. MIT Press, 1993.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Copyright © 2015 Barry Watson. All rights reserved.