- English only

# Lab for Automated Reasoning and Analysis LARA

# 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: