Ground Atom (First-Order Logic)

first-order-logic

Definition

Ground Atom (First-Order Logic)

A ground atom is an atomic formula $P(t_1,\dots ,t_n)$ where every $t_i$ is a ground term.

Intuition

A ground formula has no variables, so its truth depends only on the structure — no variable assignment is needed. The structure already fixes what every constant and function symbol means, so every ground term evaluates to a concrete element of the domain.

Evaluating a ground atom

Let $\mathcal{M}=(\mathbb{N},\mathcal{I})$ with ${\text{zero}}^{\mathcal{M}}=0$, ${\text{succ}}^{\mathcal{M}}(n)=n+1$, and ${\text{Even}}^{\mathcal{M}}=\{0,2,4,\dots \}$.

Formula	Terms evaluate to	Tuple in $P^{\mathcal{M}}$?	$\mathcal{M}\models$?
$\text{Even}(\text{zero})$	$0$	$0\in {\text{Even}}^{\mathcal{M}}$	yes
$\text{Even}(\text{succ}(\text{zero}))$	$1$	$1\notin {\text{Even}}^{\mathcal{M}}$	no
$\text{Even}(\text{succ}(\text{succ}(\text{zero})))$	$2$	$2\in {\text{Even}}^{\mathcal{M}}$	yes

Satisfaction

A structure alone determines the satisfaction of ground formulas.

For a structure $\mathcal{M}=(\mathcal{D},\mathcal{I})$ and a ground atom $P(t_1,\dots ,t_n)$:

$$\mathcal{M}\models P(t_1,\dots ,t_n)⟺(t_1^{\mathcal{M}},\dots ,t_n^{\mathcal{M}})\in P^{\mathcal{M}}$$

Satisfaction extends inductively to the Boolean connectives:

$$\begin{array}{rl}\mathcal{M}\models \neg \phi & ⟺\text{not }\mathcal{M}\models \phi \\ \mathcal{M}\models \phi \wedge \psi & ⟺\mathcal{M}\models \phi \text{ and }\mathcal{M}\models \psi \\ \mathcal{M}\models \phi \vee \psi & ⟺\mathcal{M}\models \phi \text{ or }\mathcal{M}\models \psi \\ \mathcal{M}\models \phi \to \psi & ⟺\mathcal{M}\models \psi \text{ whenever }\mathcal{M}\models \phi \end{array}$$