Formula (First-Order Logic)

Definition

Formula (First-Order Logic)

Let be a signature and a set of variables. The set of formulas over is defined inductively:

An atomic formula is for and terms .

Satisfaction

Let be an interpretation. Satisfaction is defined inductively:

We write when the formula is not satisfied, and or as shorthand.

Coincidence Lemma

Definition

Coincidence Lemma (First-Order Logic)

Let be a formula and let be two variable assignments that agree on . Then

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

Link to original