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: