Formula (First-Order Logic)

first-order-logic

Definition

Formula (First-Order Logic)

Let $(\mathcal{F},\mathcal{P})$ be a signature and $\mathcal{V}$ a set of variables. The set of formulas over $(\mathcal{F},\mathcal{P})$ is defined inductively:

$$\begin{array}{rl}\phi \text{ atomic}& :\phi \text{ is a formula}\\ \phi \text{ a formula}& :\neg \phi \text{ is a formula}\\ \phi ,\psi \text{ formulas}& :(\phi \wedge \psi ),(\phi \vee \psi ),(\phi \to \psi )\text{ are formulas}\\ x\in \mathcal{V},\phi \text{ a formula}& :(\forall x\phi ),(\exists x\phi )\text{ are formulas}\end{array}$$

An atomic formula is $P(t_1,\dots ,t_n)$ for $P/n\in \mathcal{P}$ and terms $t_i$.

Satisfaction

Let $(\mathcal{M},\ell )$ be an interpretation. Satisfaction is defined inductively:

$$\begin{array}{rl}(\mathcal{M},\ell )\models P(t_1,\dots ,t_n)& ⟺\left(t_1^{(\mathcal{M},\ell )},\dots ,t_n^{(\mathcal{M},\ell )}\right)\in P^{\mathcal{M}}\\ (\mathcal{M},\ell )\models \neg \phi & ⟺\text{not }(\mathcal{M},\ell )\models \phi \\ (\mathcal{M},\ell )\models \phi \wedge \psi & ⟺(\mathcal{M},\ell )\models \phi \text{ and }(\mathcal{M},\ell )\models \psi \\ (\mathcal{M},\ell )\models \phi \vee \psi & ⟺(\mathcal{M},\ell )\models \phi \text{ or }(\mathcal{M},\ell )\models \psi \\ (\mathcal{M},\ell )\models \phi \to \psi & ⟺(\mathcal{M},\ell )\models \psi \text{ whenever }(\mathcal{M},\ell )\models \phi \\ (\mathcal{M},\ell )\models \forall x\phi & ⟺(\mathcal{M},\ell [d/x])\models \phi \text{ for all }d\in \mathcal{D}\\ (\mathcal{M},\ell )\models \exists x\phi & ⟺(\mathcal{M},\ell [d/x])\models \phi \text{ for some }d\in \mathcal{D}\end{array}$$

We write $(\mathcal{M},\ell )/\models \phi$ when the formula is not satisfied, and $\mathcal{M},\ell \models \phi$ or $\mathcal{M}{\models }_{\ell }\phi$ as shorthand.

Coincidence Lemma

Definition

Coincidence Lemma (First-Order Logic)

Let $\phi$ be a formula and let $\ell ,{\ell }^{\prime }$ be two variable assignments that agree on $\mathrm{free}(\phi )$. Then

$$(\mathcal{M},\ell )\models \phi ⟺(\mathcal{M},{\ell }^{\prime })\models \phi$$

Satisfaction depends only on the free variables. Bound variables do not affect the truth value.

Link to original