First-Order Logic Semantics
(Recall First-Order Logic Syntax and Propositional Logic Semantics as well as Predicate Logic Informally.)
An interpretation for first-order logic language is the pair
where
is a nonempty set, called the domain of interpretation, and
is the interpretation function, which assigns
- to each first-order variable
, an element
- to each relation symbol
with arity
, a relation
- to each function symbol
with arity
, a function
If we denote
by
and
by
.
Because terms denote values from domain and formulas denote truth values from
, we define two semantic evaluation functions:
We evaluate terms by recursion on the structure of :
We evaluate formulas by recursion on the structure of :
How do we evaluate quantifiers?
We generalize this notion as follows: if is an interpretation and
is a set of first-order formulas, we write
iff for every
we have
(set is treated as infinite conjunction). This is a generalization because
.
A terminological note: in algebra, an interpretation is often called a structure. Instead of using mapping language
to interpretation of its symbols, the structure is denoted by a tuple
. For example, an interpretation with domain
, with one binary operation whose interpretation is
and one binary relation whose interpretation is
can be written as
. This way we avoid writing
all the time, but it becomes more cumbersome to describe correspondence between structures.
Examples
Example with Finite Domain
Consider language where
is a unary function symbol (
) and
is a binary relation symbol (
). Let
be given by
Let us evaluate the truth value of these formulas:
Example with Infinite Domain
Consider language where
is a unary function symbol (
) and
is a binary relation symbol (
). Let
where
. Let
be defined as the “strictly divides” relation:
What is the truth value of this formula
What is the truth value of this formula
Domain Non-Emptiness
Let be an arbitrary interpretation. Consider formula
What is its truth value in ? Which condition on definition of
did we use?
This formula is true with the assumption that is not empty.
With an empty domain, this formula would be false. There are other problems, for instance “how to evaluate a variable?”.
Satisfiability, Validity, and Semantic Consequence
Definition (satisfiability of set): If is a set of formulas, a model of
is an interpretation such that
. A set
of first-order formulas is satisfiable if there exists a model for
. A set
is unsatisfiable (contradictory) iff it is not satisfiable (it has no model).
Note: taking we obtain notion of satisfiability for formulas.
Definition (semantic consequence): We say that a set of formulas is a semantic consequence of a set of formulas
and write
, iff every model of
is also a model of
.
Definition: Formula is valid, denoted iff
.
Lemma: iff for every interpretation
we have
.
Lemma: A set of formulas is unsatisfiable iff
.
Lemma: Let be a set of formulas and
a formula. Then
iff the set
is contradictory.
One of the central questions is the study of whether a set of formulas is contradictory, many basic questions reduce to this problem.
Consequence Set
Definition: The set of all consequences of :
Note is equivalent to
.
Lemma: The following properties hold: