Logic and Proof MT24, First-order logic

• A set of constant symbols $c _ 1, c _ 2, \ldots$ (can be finite/infinite)
• A set of function symbols $f _ 1, f _ 2, \ldots$ (can be finite/infinite), each with associated arity $k > 0$.
• A set of predicate symbols $P _ 1, P _ 2, \ldots$ (can be finite/infinite)

• Each variable is a term.
• Each constant symbol is a term.
• If $t _ 1, \ldots, t _ k$ are terms and $f$ is a $k$-ary function symbol, then $f(t _ 1, \ldots, t _ k)$ is a term.

• If $t _ 1, \ldots, t _ k$ are terms and $P$ is a $k$-ary function symbol, then $P(t _ 1, \ldots, t _ k)$ is a formula.
• If $F$ is a formula, $\lnot F$ is a formula
• If $F$ and $G$ are fomulas
  • $(F \lor G)$ is a formula
  • $(F \land G)$ is a formula
• If $F$ is a formula
  • $\exists x F$ is a formula
  • $\forall x F$ is a formula

If $t _ 1, \ldots, t _ k$ are terms and $P$ is a $k$-ary function symbol, then $P(t _ 1, \ldots, t _ k)$ is an atomic formula.

\[(\forall x F) \land G\]

\[G\]

If it is in the scope of some quantifier, it is bound, otherwise it is free.

$x$ is a free variable, so it should really be

\[F(x) := \forall y(x + y = y)\]

This helps keep the notation consistent and makes it more obvious that you can “plug” this into to other propositional formulas.

• A non-empty set $A$, called the universe of the structure
• For each $k$-ary predicate symbol $P$ in $\sigma$, a $k$-ary relation $P^{\mathcal A} \subset A^k$
• For each $k$-ary function symbol $f$ in $\sigma$, a $k$-ay function $f : A^k \to A$
• For each constant symbol $c$, an element $c^\mathcal A$ of $A$.

• If $t$ is a constant symbol$c$, then $t^\mathcal A (\pmb a) = c^\mathcal A$
• If $t$ is the variable $x _ i$, then $t^\mathcal A(\pmb a) = a _ i$
• If $t$ is a term $f(t _ 1, \ldots, t _ k)$, then $t^\mathcal A(\pmb a) = f^\mathcal A(t _ 1^\mathcal A(\pmb a), \ldots, t _ k^\mathcal A(\pmb a))$

It is defined inductively like so:

• $\mathcal A \models P(t _ 1, \ldots, t _ k)(\pmb a)$ if and only if $(t _ 1^\mathcal A(\pmb a), \ldots, t _ k^\mathcal A(\pmb a)) \in P^\mathcal A$
• $\mathcal A \models (F \land G)(\pmb a)$ if and only if $\mathcal A \models F(\pmb a)$ and $\mathcal A \models G(\pmb a)$
• $\mathcal A \models (F \lor G)(\pmb a)$ if and only if $\mathcal A \models F(\pmb a)$ or $\mathcal A \models G(\pmb a)$
• $\mathcal A \models (\lnot F) (\pmb a)$ if and only if $\mathcal A \not\models F(\pmb a)$
• If $F$ is $\exists y G(\pmb x, y)$ then $\mathcal A \models \exists y F(\pmb a)$ if and only if there exists $b \in A$ such that $\mathcal A \models G(\pmb a, b)$
• If $F$ is $\forall y G(\pmb x, y)$ then $A \models \forall x F(\pmb a)$ if and only if $\mathcal A \models F(\pmb a, b)$ for all $b \in A$

If working in first-order logic with equality, then:

• If $F$ is the formula $t _ 1 = t _ 2$, then $\mathcal A \models F(\pmb a)$ if and only if $t^\mathcal A(\pmb a) = t _ 2^\mathcal A(\pmb a)$.

$\mathcal A \models F(\pmb a)$ for some $\sigma$-structure $\mathcal A$ and valuation $\pmb a$ of free variables in $F$.

$\mathcal A \models F(\pmb a)$ for every $\sigma$-structure $\mathcal A$ and valuation $\pmb a$ of free variables in $F$.

Every $\sigma$-structure $\mathcal A$ that satisfies $\pmb S$ also satisfies $F$.

The formula can be written

\[Q _ 1 y _ 1 Q _ 2 y _ 2 \cdots Q _ n y _ n F\]

where each $Q _ i$ is a quantifier and $F$ contains no quantifiers. and $F$ is the matrix of the formula.

No variable occurs both bound and free and all quantifiers in formula refer to different variables.

The formula with $t$ substituted for every free occurences of $x$ in $F$.

Suppose:

• $t$ is a term built over variables $\pmb x$
• $F(\pmb x, y)$ is a formula such that no variable in $t$ occurs bound in $F$
• $b := t^\mathcal A(\pmb a)$

Then:

• $\mathcal A \models Ft/y$ iff $\mathcal A \models F(\pmb a, b)$.

It has only relation and constant symbols, no function symbols.

\[\forall^\ast H = \forall x _ 1 \forall x _ 2 \cdots \forall x _ n H\]

1. Show that it is valid by considering an arbitrary model and assignment
2. Show $\lnot F$ is unsatisfiable using first-order resolution

Consider the structure $\mathcal A = (A, P^\mathcal A, Q^\mathcal A)$ where $A = \lbrace 1, 2 \rbrace$, $P^\mathcal A = \lbrace 1 \rbrace$ and $Q^\mathcal A = \lbrace 2 \rbrace$, and with the assignment $x^\mathcal A = 2$.

@example~ @exam~

Given $\pmb v \in \mathcal S$, define

\[F _ {\pmb v} = \forall x _ 1 \cdots \forall x _ k \big( R(s^{a _ 1}(x _ 1), \ldots, s^{a _ k}(x _ k)) \to R(s^{b _ 1}(x _ 1), \ldots, s^{b _ k}(x _ k)) \big)\]

where for each $1 \le i \le k$, we have:

• If $v _ i = -1$, $a _ i = 1$ and $b _ i = 0$
• If $v _ i = 0$, $a _ i = 0$ and $b _ i = 0$
• If $v _ i = 0$, $a _ i = 0$ and $b _ i = 1$

Intuitively, $R$ is a $k$-ary relation which should indicate that $R(x _ 1, \ldots, x _ k)$ is reachable; $F _ \pmb v$ says that $R$ is closed under adding $\pmb v$. $s$ is supposed to represent the successor here.

Then let

\[F = \left( R(s(0), 0, \ldots, 0) \land \bigwedge _ {v \in \mathcal S} F _ {\pmb v}\right) \to R(0, \ldots, 0, s(0))\]

This says that if the initial vector is reachable and $R$ obeys all the rules introduced by $F _ {\pmb v}$, then the final vector is reachable.

$F$ valid implies $(0, \ldots, 0, 1) \in \mathsf{Reach} _ \mathcal S$: If $F$ is valid, then it is satisfied by $\mathcal N = (N, R^\mathcal N, 0^\mathcal N, s^\mathcal N)$ where:

• $N = \mathbb N$
• $R^\mathcal N = \mathsf{Reach} _ \mathcal S$
• $0^\mathcal N = 0$
• $s^\mathcal N = (n \mapsto n + 1)$

Then by definition of $\mathsf{Reach} _ \mathcal S$, $\mathcal N \models R(s(0), 0, \ldots, 0) \land \bigwedge _ {v \in \mathcal S} F _ {\pmb v}$. Hence $\mathcal N \models R(0, \ldots, 0, s(0))$, and so $(0, \cdots, 0, 1) \in \mathsf{Reach} _ \mathcal S$.

$(0, \ldots, 0, 1) \in \mathsf{Reach} _ \mathcal S$ implies $F$ is valid: Suppose that $(0, \ldots, 0, 1) \in \mathsf{Reach} _ \mathcal S$. Consider a structure $\mathcal A$ where $\mathcal A \models R(s(0), 0, \ldots, 0) \land \bigwedge _ {v \in \mathcal S} F _ {\pmb v}$. Consider the set $\tilde R \subseteq \mathbb R^k$ of tuples $(n _ 1, \ldots, n _ k)$ such that $\mathcal A \models (s^{n _ 1}(0), \ldots, s^{n _ k}(0))$. Then $\tilde R$ satisfies the first two conditions, and so by minimality of $\mathsf{Reach} _ \mathcal S$, we have $\mathsf{Reach} _ \mathcal S \subseteq \tilde R$. Hence $\mathcal A \models R(0, \ldots, 0, s(0))$ and so $F$ is valid.

@example~ @exam~

Let $N _ {k, m}$ be an upper bound on the number of formulas of quantifier depth $k$ in $m$ free variables up to logical equivalence.

We have $N _ {0, m} \le 2^{2^{m^2} }$, as there are $m^2$ atomic formulas on $m$ variables and hence the number of quantifier-free formulas in $m$ variables up to logical equivalence is $2^{2^{m^2} }$.

We also have $N _ {k+1, m} \le 2^{2^{N _ {k, m+1} } }$, since every formula of quantifier depth $k+1$ is a boolean combination of formulas $\exists x \varphi$, where $\varphi$ has quantifier depth $k$ and $m+1$ free variables, including $x$.

Hence

\[N _ {k, m} \le (\Phi \circ \cdots \circ \Phi)((m+k)^2)\]

where $\Phi(x) = 2^x$ and the composition is performed $2k$ times.

@example~ @sheets~

In the following, let $I _ 1, \ldots, I _ {2^s}$ be an enumeration of the subsets of $\lbrace 1, \ldots, s \rbrace$.

\[\begin{aligned} F &\equiv \forall \pmb x \exists \pmb y \bigvee^s _ {i = 1} (F _ i \land F _ i') &&(\text{def.}) \\\\ &\equiv \forall \pmb x \bigvee^s _ {i = 1} ((\exists \pmb y F _ i) \land F _ i') &&(1\star) \\\\ &\equiv \forall \pmb x \bigwedge^{2^s} _ {j = 1} \left( \bigvee _ {i \in I _ j} \exists \pmb y F _ i \lor \bigvee _ {i \notin I _ j} F _ i' \right) &&(2\star) \\\\ &\equiv \bigwedge^{2^s} _ {j = 1} \left( \bigvee _ {i \in I _ J} \exists \pmb y F _ i \lor \forall \pmb x \bigvee _ {i \notin I _ j} F _ i' \right) &&(3\star) \\\\ &\equiv \bigwedge^{2^s} _ {j = 1} \left( \exists \pmb y \bigvee _ {i \in I _ J} F _ i \lor \forall \pmb x \bigvee _ {i \notin I _ j} F _ i' \right) &&(1\star) \\\\ &\equiv \bigwedge^{2^s} _ {j = 1} \left( \exists \pmb y _ j \bigvee _ {i \in I _ j} F _ i[\pmb y _ j / \pmb y] \lor \forall \pmb x \bigvee _ {i \notin I _ j} F _ i' \right) &&(\text{rename}) \\\\ &\equiv \exists \pmb y _ 1 \cdots \exists \pmb y _ {2^s} \bigwedge^{2^s} _ {j = 1} \left( \bigvee _ {i \in I _ j} F _ i[\pmb y _ j / \pmb y] \lor \forall \pmb x \bigvee _ {i \notin I _ j} F _ i' \right) &&(4\star) \\\\ &\equiv \exists \pmb y _ 1 \cdots \exists \pmb y _ {2^s} \forall \pmb x \bigwedge^{2^s} _ {j = 1} \left( \bigvee _ {i \in I _ j} F _ i[\pmb y _ j / \pmb y] \lor \bigvee _ {i \notin I _ j} F _ i' \right) && (3\star) \end{aligned}\]

where:

• $(1\star)$ follows from the fact that $\exists$ distributes over disjunction, and that by assumption $\pmb y$ is not mentioned in $F _ i’$
• $(2\star)$ follows from just expanding the disjunction, i.e. we may write $(\phi _ 1 \land \psi _ 1) \lor (\phi _ 2 \land \psi _ 2) \lor \cdots \lor (\phi _ s \land \psi _ s)$ as $\bigwedge^{2^s} _ {j=1} \left( \bigvee _ {i \in I _ j} \phi _ i \lor \bigvee _ {i \notin I _ j} \psi _ i \right)$.
• $(3\star)$ follows from the fact that $\forall$ distributes over conjunction
• $(4\star)$ is not because $\exists$ distributes over conjunction, that is not true. It just comes from noting that after renaming each of the variables is different

@example~ @sheets~