A first order theory (FOT) \(T\) is defined by two main components:

• A signature \(\Sigma \) of a set of constant, function, and predicate symbols
• A set of axioms \(\mathcal A\) consisting of closed (i.e. no free variables) formulas over the signature \(\Sigma \)

We say that a formula constructed from only from the contents of the signature \(\Sigma \) is a \(\Sigma \)-formula.

Consider a theory withthe following signature:

And the axiom:

Are the following legal \(\Sigma _H\)-formulas?

1. \( \exists x.\ \forall y.\ (\texttt {taller}(x, z) \land \texttt {taller}(y, w)) \)
2. \( \exists x.\ \forall z.\ \texttt {taller}(x, z) \land \texttt {taller}(\text {joe}, \text {tom}) \)

A structure which we denote as:

Is a model of a theory \(T\) (or \(T\)-model) iff:

where:

• \(U\) is the universe or more commonly the domain
• \(I\) is the interpretation which assigns some meaning to our formula

consider a structure consisting of a universe \(U\) and interpretation \(I\) as follows:

Are the following models of the theory \(T\) or not:

1. Is \(\langle U, I\rangle \) a model of \(T\)
2. If we change the interpretation to \[ I = \{\texttt {taller} \mapsto \{\langle A, B\rangle \}\} \] is the structure now a model of \(T\)?
3. If we add the following axiom \[ \forall x, y, z.\ (\texttt {taller}(x, y) \land \texttt {taller}(y, z) \to \texttt {taller}(x, z)) \] and we change the interpretation to \[ I = \{\texttt {taller} \mapsto \{\langle A, B \rangle , \langle B, C \rangle \}\} \] then is the structure a model of \(T\)?

We say that a formula \(F\) is satisfiable modulo \(T\) iff there exists a \(T\)-model \(M\) and a variable assignment \(\sigma \) such that:

We say that a formula \(F\) is valid modulo \(T\) iff forall \(T\)-models \(M\) and all variable assignments \(\sigma \) we have:

We can compare the two notions by understanding validity in modulo \(T\) as a restriction of validity in FOL to only those models that are \(T\)-models. So the implication of that is that if a formula is valid (true in all models), then its clearly also valid in the subset/restriction to only \(T\)-models. However, the other way around does not hold, since a formula can be true in all \(T\)-models, but false in some non-\(T\)-model. Hence we have the following:

But the other way around does not hold in general:

Consider some arbitrary first order theory \(T\)

1. If a formula is valid in FOL, then is it also valid in modulo \(T\)?
2. If a formula is valid modulo \(T\), then is it also valid in FOL?

The theory of equality \(T_=\) is a first order theory over the signature \(\Sigma _=\) which contains:

Where \(=\) is a binary relation symbol and \(s\) is any constant function or predicate symbol. The axioms of the theory of equality are:

Consider the universe:

which of the following interpetations of \(=\) are allowd by the axioms of \(T_=\):

1. \(I(=) \triangleq \{\langle \alpha , \beta \rangle , \langle \beta \alpha \rangle \}\)
2. \(I(=) \triangleq \{\langle \alpha , \alpha \rangle , \langle \beta , \beta \rangle \}\)
3. \(I(=) \triangleq \{\langle \alpha , \alpha \rangle , \langle \alpha , \beta \rangle , \langle \beta , \alpha \rangle , \langle \beta , \beta \rangle \}\)

In the most general sense we say that a relation \(R\) over a set \(A\) is a congruence with respect to a function \(f : A^n \to A\) if for all \(a_1, \ldots , a_n, b_1, \ldots , b_n \in A\) such that \(a_i\ R\ b_i\) for all \(1 \leq i \leq n\) we have:

if we denote \(\overline x\) as a vector of elements \(x_1, \ldots , x_n\) we can rewrite this more succinctly as:

In the case of first order theories we can then instantiate \(R\) with things like equality or other relations defined in the theory. Additionally we can \(f\) represent a function or predicate symbol from the signature of the theory. In the case of binary functions or predicates we can also define left and right congruence as follows:

1. A relation \(R\) is a left congruence with respect to a binary function or predicate \(f : A \times A \to A\) if for all \(a, b, c \in A\) such that \(a\ R\ b\) we have:
\[ f(a, c)\ R\ f(b, c) \]
2. A relation \(R\) is a right congruence with respect to a binary function or predicate \(f : A \times A \to A\) if for all \(a, b, c \in A\) such that \(a\ R\ b\) we have:
\[ f(c, a)\ R\ f(c, b) \]

Consider the universe:

and the interpretation:

1. Does the interpetation \(I(=)\) satisfy the axioms of equality?
2. Which interpretations for a function \(f\) satisfy the axioms of congruence?
   1. \(I(f) \triangleq \{b \to a, a \to c, c \to c\}\)
   2. \(I(f) \triangleq \{b \to b, a \to b, c \to b\}\)
   3. \(I(f) \triangleq \{b \to a, a \to b, c \to c\}\)

Peano Arithmetic (PA) is a first order theory over the signature \(\Sigma _{PA}\) which contains:

Where \(0\) is a constant symbol representing zero, \(S\) is a unary function symbol representing the successor function, \(+\) and \(\times \) are binary function symbols representing addition and multiplication respectively, and \(=\) is a binary relation symbol representing equality. The axioms of Peano Arithmetic are:

Are the following well-formed \(T_{\text {PA}} formulae?\)

1. \(x + y = 1 \land f(x) = 1 + 1\)
2. \(\forall x.\ \exists y.\ \exists z.\ x + y = 1\land z \times x = 1 + 1\)
3. \(2x = y\)

The theory of rationals \(T_{\mathbb {Q}}\) is a first-order theory over the signature \(\Sigma _{\mathbb {Q}}\) which contains:

(Axioms ommitted for brevity.)

Some important properties of \(T_{\mathbb {Q}}\) are:

• Full theory is decidable but doubly exponential.
• Conjunctive quantifier-free fragment is efficiently decidable (polynomial time).
• \(T_{\mathbb {Q}}\) is the basis for arithemtic reasoning in SMT solvers such as Z3.
• In practice the simplex algorithm is used.

Presburger Arithmetic (PA) is a first order theory over the signature \(\Sigma _{\mathbb {N}}\) which contains:

Where \(0\) and \(1\) are constant symbols representing zero and one respectively, \(+\) is a binary function symbol representing addition, and \(=\) is a binary relation symbol representing equality. The axioms of Presburger Arithmetic are:

Some important properties of \(T_{\mathbb {N}} are\):

• Validity in quantifer-free Presburger Arithmetic is decidable.
• Validity in full Presburger Arithmetic is decidable.
• Validity in Presburger Arithmetic has a super exponential complexity \(O(2^{2^n})\)
• \(T_{\mathbb {N}}\) is complete, i.e. \[ \forall F.\ T_{\mathbb {N}} \models F \lor T_{\mathbb {N}} \models \neg F \]

Consider the following formula:

1. Is this formula valid in \(T_{\mathbb {Q}}\)
2. Is this formula valid in \(T_{\mathbb {Z}}\)

The theory of arrays is a first-order theory that models arrays as functions from indices to values. Its signature includes:

where:

• \(-[ - ]\): read operation, which takes an array and an index and returns the value at that index.
• \(\langle - \triangleleft - \rangle \): write operation, which takes an array, an index, and a value, and returns a new array with the value at the specified index updated.
• \(=\): equality relation, which checks if two arrays are identical.

The axioms of the theory of arrays are:

Which of the following formula is valid/satisfiable/unsatisfiable ?

1. \(a[3] = 2\)
2. \(a \langle 3 \triangleleft 5 \rangle [3] = 5\)
3. \(a \langle 3 \triangleleft 5 \rangle [3] = 3\)
4. \(a[3] = 2\land a \langle 3 \triangleleft 5 \rangle [3] = 5\)