First-order logic · The Lumenary

Lens

MotivationH

Saying exactly what we mean

A function $f : \R \to \R$ is continuous if

\forall x\ \forall \varepsilon > 0\ \exists \delta > 0\ \forall y\ \big( |x - y| < \delta \to |f(x) - f(y)| < \varepsilon \big),

and uniformly continuous if

\forall \varepsilon > 0\ \exists \delta > 0\ \forall x\ \forall y\ \big( |x - y| < \delta \to |f(x) - f(y)| < \varepsilon \big).

The only difference is where " $\forall x$ " stands — and $x \mapsto x^2$ is continuous but not uniformly continuous. In the lesson on propositional logic you made "and", "or", "not" and "if … then" exact. This lesson does the same for the quantifiers "for all" and "there exists", which carry most of the weight in mathematical statements.

There is a second motive. In the 1920s David Hilbert asked questions about mathematics itself: can every true statement be proved? Is there an algorithm that decides whether a statement follows from axioms? To answer such questions — and they were answered, by Gödel, Church and Turing — statements and proofs must themselves become mathematical objects. First-order logic is the language in which this was done, and in which most of mathematics, through the axioms of ZFC, can be written.

IntuitionH

Syntax, meaning and proof

First-order logic has three layers.

Syntax. Formulas are strings of symbols, built by rules, like $\forall x\, \exists y\, (y < x)$ . On their own they mean nothing.
Semantics. A structure gives the symbols a meaning: a set of elements for the quantifiers to range over, and an actual relation for $<$ . The sentence above is true in $(\Z, <)$ — below every integer there is another — and false in $(\N, <)$ , where nothing lies below $0$ . Truth is always truth in a structure.
Proof. A proof system manipulates formulas by rules, without looking at any structure.

This gives two notions of " $\varphi$ follows from $\Gamma$ ": $\Gamma \models \varphi$ (semantic consequence: $\varphi$ is true in every structure in which all of $\Gamma$ is true) and $\Gamma \vdash \varphi$ (derivability: there is a formal proof). The soundness theorem, proved in this lesson, says $\vdash$ implies $\models$ : proofs never lead from truth to falsehood. The completeness theorem of Kurt Gödel (1929) says that conversely $\models$ implies $\vdash$ . That these two very different notions coincide is one of the great facts of logic.

The word "first-order" refers to what the quantifiers range over: elements of the structure — never subsets, functions or relations on it. That restriction is what makes the beautiful theorems of first-order logic true, and also what limits its expressive power.

DefinitionsH

The language and its meaning

Definition— signature

A signature $L$ consists of constant symbols, function symbols and relation symbols, each function and relation symbol with an arity (number of arguments) $n \ge 1$ .

Examples: the signature of groups $\{\cdot, e, {}^{-1}\}$ (binary function, constant, unary function); of orders $\{<\}$ (binary relation); of graphs $\{E\}$ ; of rings $\{+, \cdot, -, 0, 1\}$ ; of set theory $\{\in\}$ . The symbol $=$ and the logical symbols $\bot, \neg, \wedge, \vee, \to, \forall, \exists$ , brackets and the variables $x_0, x_1, \dots$ are always available.

Definition— terms and formulas

Terms are built from variables and constants by applying function symbols: if $f$ is $n$ -ary and $t_1, \dots, t_n$ are terms, so is $f(t_1, \dots, t_n)$ . Atomic formulas are $\bot$ , $t_1 = t_2$ , and $R(t_1, \dots, t_n)$ for an $n$ -ary relation symbol $R$ . Formulas are built from atomic formulas: if $\varphi, \psi$ are formulas and $x$ is a variable, then $\neg \varphi$ , $(\varphi \wedge \psi)$ , $(\varphi \vee \psi)$ , $(\varphi \to \psi)$ , $\forall x\, \varphi$ and $\exists x\, \varphi$ are formulas.

An occurrence of $x$ in $\varphi$ is bound if it lies inside a part $\forall x\, \psi$ or $\exists x\, \psi$ , and free otherwise. A sentence is a formula with no free variables. In $\exists y\, (y \cdot y = x)$ the variable $y$ is bound and $x$ is free: the formula says something about $x$ (" $x$ is a square"), not about $y$ .

Definition— structure

An $L$ -structure $\mathcal{M}$ is a non-empty set $M$ (the domain) together with an element $c^{\mathcal{M}} \in M$ for each constant symbol, a function $f^{\mathcal{M}} : M^n \to M$ for each $n$ -ary function symbol, and a relation $R^{\mathcal{M}} \subseteq M^n$ for each $n$ -ary relation symbol.

An assignment is a function $s$ from the variables to $M$ . The value $t^{\mathcal{M}}[s]$ of a term is computed in the obvious way: $x^{\mathcal{M}}[s] = s(x)$ , $c^{\mathcal{M}}[s] = c^{\mathcal{M}}$ and $f(t_1, \dots, t_n)^{\mathcal{M}}[s] = f^{\mathcal{M}}(t_1^{\mathcal{M}}[s], \dots, t_n^{\mathcal{M}}[s])$ . For $a \in M$ , write $s[x \mapsto a]$ for the assignment that agrees with $s$ except that it sends $x$ to $a$ .

Definition— satisfaction (Tarski)

The relation $\mathcal{M} \models \varphi[s]$ (" $\varphi$ is true in $\mathcal{M}$ under $s$ ") is defined by recursion on $\varphi$ :

$\mathcal{M} \not\models \bot[s]$ ;
$\mathcal{M} \models (t_1 = t_2)[s]$ iff $t_1^{\mathcal{M}}[s] = t_2^{\mathcal{M}}[s]$ ;
$\mathcal{M} \models R(t_1, \dots, t_n)[s]$ iff $(t_1^{\mathcal{M}}[s], \dots, t_n^{\mathcal{M}}[s]) \in R^{\mathcal{M}}$ ;
$\neg, \wedge, \vee, \to$ are interpreted by their truth tables;
$\mathcal{M} \models \forall x\, \varphi[s]$ iff $\mathcal{M} \models \varphi[s[x \mapsto a]]$ for every $a \in M$ ;
$\mathcal{M} \models \exists x\, \varphi[s]$ iff $\mathcal{M} \models \varphi[s[x \mapsto a]]$ for some $a \in M$ .

The truth of $\varphi$ depends only on the values of $s$ at the free variables of $\varphi$ (Lemma 1 below). So for a sentence $\sigma$ we simply write $\mathcal{M} \models \sigma$ , " $\sigma$ is true in $\mathcal{M}$ ", or " $\mathcal{M}$ is a model of $\sigma$ ".

Definition— models and consequence

A theory is a set $\Gamma$ of sentences; a model of $\Gamma$ is a structure in which every sentence of $\Gamma$ is true. $\Gamma \models \varphi$ ( $\varphi$ is a semantic consequence of $\Gamma$ ) means: for every structure $\mathcal{M}$ and every assignment $s$ , if $\mathcal{M} \models \gamma[s]$ for all $\gamma \in \Gamma$ , then $\mathcal{M} \models \varphi[s]$ . A formula is valid, $\models \varphi$ , if it is true in every structure under every assignment.

Substitution

We write $\varphi[t/x]$ for the result of replacing the free occurrences of $x$ in $\varphi$ by the term $t$ . There is a trap: in $\varphi = \exists y\, \neg(y = x)$ ("something differs from $x$ "), naively substituting $y$ for $x$ gives $\exists y\, \neg(y = y)$ , which is false everywhere — the $y$ we put in was captured by the quantifier. Substitution must avoid capture, by renaming bound variables first: $\exists z\, \neg(z = y)$ . We always assume this has been done. (The Lean formalisation avoids the issue altogether with de Bruijn indices, see below.)

Natural deduction

A derivation shows a sequent $\Gamma \vdash \varphi$ (" $\varphi$ follows from the assumptions $\Gamma$ ") using the rules below. One introduction and one elimination rule per symbol, plus classical reductio. We write $\Gamma, \psi$ for $\Gamma \cup \{\psi\}$ and $\neg\varphi$ for $\varphi \to \bot$ .

Rule	From	Infer
assumption	—	$\Gamma \vdash \varphi$ when $\varphi \in \Gamma$
$\to$ I	$\Gamma, \varphi \vdash \psi$	$\Gamma \vdash \varphi \to \psi$
$\to$ E	$\Gamma \vdash \varphi \to \psi$ and $\Gamma \vdash \varphi$	$\Gamma \vdash \psi$
$\wedge$ I	$\Gamma \vdash \varphi$ and $\Gamma \vdash \psi$	$\Gamma \vdash \varphi \wedge \psi$
$\wedge$ E	$\Gamma \vdash \varphi \wedge \psi$	$\Gamma \vdash \varphi$ , and $\Gamma \vdash \psi$
$\vee$ I	$\Gamma \vdash \varphi$ (or $\Gamma \vdash \psi$ )	$\Gamma \vdash \varphi \vee \psi$
$\vee$ E	$\Gamma \vdash \varphi \vee \psi$ , $\ \Gamma, \varphi \vdash \chi$ , $\ \Gamma, \psi \vdash \chi$	$\Gamma \vdash \chi$
$\bot$ E	$\Gamma \vdash \bot$	$\Gamma \vdash \varphi$
RAA	$\Gamma, \neg\varphi \vdash \bot$	$\Gamma \vdash \varphi$
$\forall$ I	$\Gamma \vdash \varphi[y/x]$ , $y$ not free in $\Gamma$ or in $\forall x\, \varphi$	$\Gamma \vdash \forall x\, \varphi$
$\forall$ E	$\Gamma \vdash \forall x\, \varphi$	$\Gamma \vdash \varphi[t/x]$ for any term $t$
$\exists$ I	$\Gamma \vdash \varphi[t/x]$ for some term $t$	$\Gamma \vdash \exists x\, \varphi$
$\exists$ E	$\Gamma \vdash \exists x\, \varphi$ and $\Gamma, \varphi[y/x] \vdash \psi$ , $y$ not free in $\Gamma$ , $\psi$ or $\exists x\, \varphi$	$\Gamma \vdash \psi$
$=$ I	—	$\Gamma \vdash t = t$
$=$ E	$\Gamma \vdash s = t$ and $\Gamma \vdash \varphi[s/x]$	$\Gamma \vdash \varphi[t/x]$

The side conditions on $\forall$ I and $\exists$ E (the eigenvariable conditions) formalise familiar habits: "let $y$ be arbitrary" is only legitimate if nothing has been assumed about $y$ ; and "let $y$ be such an element" must not let $y$ leak into the conclusion. $\Gamma \vdash \varphi$ for a set $\Gamma$ means that $\Gamma_0 \vdash \varphi$ is derivable for some finite $\Gamma_0 \subseteq \Gamma$ .

Worked examplesH

Writing and reading formulas

Example— Axioms as sentences

Groups (signature $\{\cdot, e, {}^{-1}\}$ ): $\forall x\, \forall y\, \forall z\ (x \cdot y) \cdot z = x \cdot (y \cdot z)$ ; $\ \forall x\ (x \cdot e = x \wedge e \cdot x = x)$ ; $\ \forall x\ (x \cdot x^{-1} = e \wedge x^{-1} \cdot x = e)$ .
Strict linear orders ( $\{<\}$ ): $\forall x\, \neg(x < x)$ ; $\ \forall x\, \forall y\, \forall z\, (x < y \wedge y < z \to x < z)$ ; $\ \forall x\, \forall y\, (x < y \vee x = y \vee y < x)$ .
Fields ( $\{+, \cdot, -, 0, 1\}$ ): the commutative ring axioms, $\neg(0 = 1)$ , and $\forall x\, (\neg(x = 0) \to \exists y\ x \cdot y = 1)$ .
"There are at least three elements": $\exists x\, \exists y\, \exists z\, (\neg x = y \wedge \neg x = z \wedge \neg y = z)$ — a sentence in the empty signature.
Graphs ( $\{E\}$ ): "no vertex is isolated" is $\forall x\, \exists y\, E(x, y)$ ; "there is no triangle" is $\neg \exists x\, \exists y\, \exists z\, (E(x, y) \wedge E(y, z) \wedge E(x, z))$ .

Example— Unwinding satisfaction

Let $\mathcal{C} = (\{1, 2, 3\}, E)$ be the directed 3-cycle, $E = \{(1, 2), (2, 3), (3, 1)\}$ .

$\mathcal{C} \models \forall x\, \exists y\, E(x, y)$ : for $x = 1, 2, 3$ choose $y = 2, 3, 1$ .
$\mathcal{C} \not\models \exists y\, \forall x\, E(x, y)$ : for any $y$ , the choice $x = y$ fails, since $E$ has no loops. Swapping the quantifiers changed the truth value.
$\mathcal{C} \models \forall x\, \forall y\, (E(x, y) \to \neg E(y, x))$ : no edge is reversed.

In $(\N, <)$ , $\ \exists x\, \forall y\, \neg(y < x)$ ("there is a least element") is true (take $x = 0$ ); in $(\Z, <)$ it is false (for any $x$ , take $y = x - 1$ ). In $(\Q, <)$ , $\ \forall x\, \forall y\, (x < y \to \exists z\, (x < z \wedge z < y))$ ("density") is true (take $z = (x + y)/2$ ); in $(\Z, <)$ it is false ( $x = 0$ , $y = 1$ ).

Example— What first-order logic cannot say directly

"Every non-empty subset has a least element" (the well-ordering of $\N$ ) quantifies over subsets; it is a second-order statement. First-order arithmetic replaces it by a schema: one induction axiom $\big(\varphi(0) \wedge \forall n\, (\varphi(n) \to \varphi(n + 1))\big) \to \forall n\, \varphi(n)$ for each formula $\varphi$ . This covers only the subsets that a formula can define, and it is genuinely weaker: by the compactness theorem, first-order arithmetic has non-standard models (see completeness and compactness). Similarly "the domain is finite" and "the graph is connected" cannot be expressed by any set of first-order sentences, and "the graph can be properly coloured with three colours" needs "there exist three sets of vertices such that …" — an existential second-order statement.

Example— A derivation

We derive $\forall x\, (P(x) \to Q(x)),\ \forall x\, P(x) \vdash \forall x\, Q(x)$ . Let $\Gamma$ be the two assumptions and $y$ a variable not occurring in them.

$\Gamma \vdash \forall x\, (P(x) \to Q(x))$ — assumption.
$\Gamma \vdash P(y) \to Q(y)$ — $\forall$ E on 1, with $t = y$ .
$\Gamma \vdash \forall x\, P(x)$ — assumption.
$\Gamma \vdash P(y)$ — $\forall$ E on 3.
$\Gamma \vdash Q(y)$ — $\to$ E on 2 and 4.
$\Gamma \vdash \forall x\, Q(x)$ — $\forall$ I on 5; allowed because $y$ is not free in $\Gamma$ .

This is the formal version of "let $y$ be arbitrary; then $P(y)$ , hence $Q(y)$ ; since $y$ was arbitrary, $Q$ holds for all".

ProofH

Soundness and invariance

Two lemmas about the semantics come first. Both are proved by induction on terms and formulas, and both are formalised in Lean below.

Theorem— Lemma 1 (coincidence)

If assignments $s$ and $s'$ agree on the free variables of $\varphi$ , then $\mathcal{M} \models \varphi[s]$ iff $\mathcal{M} \models \varphi[s']$ .

Proof

For terms, $t^{\mathcal{M}}[s] = t^{\mathcal{M}}[s']$ when $s, s'$ agree on the variables of $t$ (induction on $t$ ). For formulas, induction on $\varphi$ : atomic formulas by the term case; connectives directly; and for $\forall x\, \psi$ , the assignments $s[x \mapsto a]$ and $s'[x \mapsto a]$ agree on the free variables of $\psi$ (those of $\forall x\, \psi$ , plus $x$ ), so the induction hypothesis applies for every $a$ . The case $\exists$ is the same.

∎

Theorem— Lemma 2 (substitution)

If $t$ is substitutable for $x$ in $\varphi$ (no capture), then $\mathcal{M} \models \varphi[t/x][s]$ iff $\mathcal{M} \models \varphi[s[x \mapsto t^{\mathcal{M}}[s]]]$ .

Proof

First for terms: $u[t/x]^{\mathcal{M}}[s] = u^{\mathcal{M}}[s[x \mapsto t^{\mathcal{M}}[s]]]$ , by induction on $u$ (the variable $x$ is replaced by $t$ , whose value is exactly what the new assignment gives $x$ ). Then by induction on $\varphi$ . The atomic cases are the term case and the connectives are immediate. For $\forall y\, \psi$ with $y \neq x$ : since there is no capture, $y$ does not occur in $t$ , so $t^{\mathcal{M}}[s[y \mapsto a]] = t^{\mathcal{M}}[s]$ by Lemma 1, and the induction hypothesis for $\psi$ under $s[y \mapsto a]$ gives the claim for every $a$ . If $y = x$ , then $x$ is not free in $\forall x\, \psi$ , the substitution does nothing, and Lemma 1 applies.

∎

Theorem— Theorem 3 (soundness)

If $\Gamma \vdash \varphi$ , then $\Gamma \models \varphi$ .

Proof

By induction on the derivation, we show for each rule: if the premises are semantic consequences, so is the conclusion. Fix a structure $\mathcal{M}$ and an assignment $s$ making every formula of $\Gamma$ true.

Assumption: $\varphi \in \Gamma$ is true under $s$ by hypothesis.
$\to$ I: if $\mathcal{M} \models \varphi[s]$ then $s$ makes all of $\Gamma, \varphi$ true, so by the induction hypothesis $\mathcal{M} \models \psi[s]$ ; hence $\mathcal{M} \models (\varphi \to \psi)[s]$ . $\to$ E, $\wedge$ I/E, $\vee$ I/E and $\bot$ E are the corresponding facts about truth tables (for $\vee$ E, whichever disjunct is true, the corresponding premise gives $\chi$ ; for $\bot$ E, the premise is never true, so the case is vacuous).
RAA: if $\mathcal{M} \not\models \varphi[s]$ , then $s$ makes $\Gamma, \neg\varphi$ true, and the premise gives $\mathcal{M} \models \bot[s]$ , which is impossible. So $\mathcal{M} \models \varphi[s]$ . (This step uses classical reasoning in the metatheory.)
$\forall$ E: by hypothesis $\mathcal{M} \models \varphi[s[x \mapsto a]]$ for every $a$ ; take $a = t^{\mathcal{M}}[s]$ and apply Lemma 2 to get $\mathcal{M} \models \varphi[t/x][s]$ . $\exists$ I is the same argument backwards, with the witness $a = t^{\mathcal{M}}[s]$ .
$\forall$ I: let $a \in M$ . The assignment $s' = s[y \mapsto a]$ agrees with $s$ on the free variables of $\Gamma$ (since $y$ is not free there), so by Lemma 1 it makes $\Gamma$ true, and the induction hypothesis gives $\mathcal{M} \models \varphi[y/x][s']$ . By Lemma 2 this is $\mathcal{M} \models \varphi[s'[x \mapsto a]]$ , and since $y$ is not free in $\forall x\, \varphi$ , Lemma 1 turns it into $\mathcal{M} \models \varphi[s[x \mapsto a]]$ . As $a$ was arbitrary, $\mathcal{M} \models \forall x\, \varphi[s]$ .
$\exists$ E: by the first premise there is $a$ with $\mathcal{M} \models \varphi[s[x \mapsto a]]$ . As in the previous case, $s' = s[y \mapsto a]$ makes $\Gamma$ and $\varphi[y/x]$ true, so the second premise gives $\mathcal{M} \models \psi[s']$ , and since $y$ is not free in $\psi$ , $\mathcal{M} \models \psi[s]$ .
$=$ I is reflexivity of equality in $M$ . $=$ E: if $s^{\mathcal{M}}[s] = t^{\mathcal{M}}[s]$ , then by Lemma 2, $\varphi[s/x]$ and $\varphi[t/x]$ are true under $s$ for exactly the same reason.

∎

Soundness is the tool for proving that something is not derivable: exhibit one structure where the premises are true and the conclusion false.

Example— Consequences of soundness

$\nvdash \exists x\, P(x) \to \forall x\, P(x)$ : in the structure $(\{0, 1\}, P = \{1\})$ some element has $P$ and not every element does.
$\vdash \forall x\, P(x) \to \exists x\, P(x)$ (assume $\forall x\, P(x)$ , use $\forall$ E with $t = x$ , then $\exists$ I with $t = x$ ). Soundness then says the sentence is valid — which is true only because structures are non-empty. The definition of structure and the rules of the proof system have to fit together.
Every theory with a model is consistent ( $\Gamma \nvdash \bot$ ): a derivation of $\bot$ would make $\bot$ true in the model. For instance, the group axioms are consistent because $(\Z, +, 0, -)$ is a group.

Theorem— Theorem 4 (isomorphic structures satisfy the same sentences)

Let $h : \mathcal{M} \to \mathcal{N}$ be an isomorphism of $L$ -structures: a bijection $M \to N$ with $h(c^{\mathcal{M}}) = c^{\mathcal{N}}$ , $h(f^{\mathcal{M}}(\vec a)) = f^{\mathcal{N}}(h(\vec a))$ and $\vec a \in R^{\mathcal{M}} \iff h(\vec a) \in R^{\mathcal{N}}$ . Then for every formula $\varphi$ and assignment $s$ , $\mathcal{M} \models \varphi[s]$ iff $\mathcal{N} \models \varphi[h \circ s]$ . In particular $\mathcal{M}$ and $\mathcal{N}$ satisfy exactly the same sentences.

Proof

For terms, $h(t^{\mathcal{M}}[s]) = t^{\mathcal{N}}[h \circ s]$ , by induction on $t$ using that $h$ commutes with constants and functions. For formulas, by induction on $\varphi$ . Equations: $t_1^{\mathcal{M}}[s] = t_2^{\mathcal{M}}[s]$ iff their images under $h$ are equal, because $h$ is injective. Relations: by the condition on $R$ . Connectives: immediate. Quantifiers: $\mathcal{M} \models \forall x\, \psi[s]$ iff for all $a \in M$ , $\mathcal{M} \models \psi[s[x \mapsto a]]$ , iff (induction hypothesis, since $h \circ s[x \mapsto a] = (h \circ s)[x \mapsto h(a)]$ ) for all $a \in M$ , $\mathcal{N} \models \psi[(h \circ s)[x \mapsto h(a)]]$ , iff for all $b \in N$ , $\mathcal{N} \models \psi[(h \circ s)[x \mapsto b]]$ — here we use that $h$ is surjective, so $b = h(a)$ ranges over all of $N$ . That is $\mathcal{N} \models \forall x\, \psi[h \circ s]$ . The case $\exists$ is the same.

∎

So sentences prove non-isomorphism: $(\N, <) \not\cong (\Z, <)$ because "there is a least element" separates them, and $(\Z, <) \not\cong (\Q, <)$ because of density. The converse of Theorem 4 fails: $(\Q, <)$ and $(\R, <)$ satisfy exactly the same first-order sentences (as shown in the completeness lesson), but they are not isomorphic, since $\Q$ is countable and $\R$ is not. A first-order theory usually has many non-isomorphic models.

Theorem— Theorem 5 (Gödel's completeness theorem, 1929)

If $\Gamma \models \varphi$ , then $\Gamma \vdash \varphi$ . Equivalently: every consistent set of sentences has a model.

We do not prove it here; the proof (Henkin's construction of a model out of the language itself) is the subject of the lesson on completeness, compactness and Löwenheim–Skolem. Together, soundness and completeness say $\Gamma \vdash \varphi \iff \Gamma \models \varphi$ .

Formal mathematicsF

A first-order logic built in Lean

We build a complete, small first-order logic in Lean, so that every definition of this lesson can be read as code, and then prove soundness. Mathlib has its own first-order logic (FirstOrder.Language), with semantics and the theorem that isomorphisms preserve truth, but at this version no proof calculus — so we write our own.

Syntax. Signatures, terms and formulas, as inductive types:

SignatureLean 4Formally verified

/-- A **signature** lists the non-logical symbols: for each arity `n`, the function symbols
`Func n` and the relation symbols `Rel n`. Constants are function symbols of arity `0`. -/
structure Signature where
  /-- Function symbols of each arity. -/
  Func : ℕ → Type
  /-- Relation symbols of each arity. -/
  Rel : ℕ → Type

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

TermLean 4Formally verified

/-- **Terms** are built from variables `var i` by applying function symbols: if `f` has arity
`n` and `t₀, …, tₙ₋₁` are terms, so is `f(t₀, …, tₙ₋₁)`. -/
inductive Term (L : Signature) : Type
  | var : ℕ → Term L
  | func : {n : ℕ} → L.Func n → (Fin n → Term L) → Term L

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

FormulaLean 4Formally verified

/-- **Formulas**: `⊥`, equations `t = u`, atomic formulas `R(t₀, …, tₙ₋₁)`, the connectives
`→, ∧, ∨`, and the quantifiers `∀, ∃`. A quantifier binds variable `0` of its body (de Bruijn
indices), so `all (rel R ![var 0, var 1])` is `∀x R(x, y)` where `y` is the free variable `0`
outside the quantifier. -/
inductive Formula (L : Signature) : Type
  | falsum : Formula L
  | eq : Term L → Term L → Formula L
  | rel : {n : ℕ} → L.Rel n → (Fin n → Term L) → Formula L
  | imp : Formula L → Formula L → Formula L
  | and : Formula L → Formula L → Formula L
  | or : Formula L → Formula L → Formula L
  | all : Formula L → Formula L
  | ex : Formula L → Formula L

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Variables are de Bruijn indices: a variable is a number, and inside a quantifier the variable $0$ is the one just bound, while the others shift up by one. So $\forall x\, \exists y\, R(x, y)$ is written all (ex (rel R ![var 1, var 0])). This removes variable capture entirely; the price is that substitution has to shift indices.

Semantics. A structure interprets the symbols; an environment (assignment) is a function from indices to elements, and cons a ρ gives the newly bound variable the value a. Satisfaction is Tarski's definition, clause by clause:

StructureLean 4Formally verified

/-- A **structure** for a signature: a domain `M` (a type) with an interpretation of each
function symbol as a function `Mⁿ → M` and of each relation symbol as a relation on `Mⁿ`.
Non-emptiness is not a field: it is automatic wherever an environment `ρ : ℕ → M` exists. -/
structure Structure (L : Signature) (M : Type u) where
  /-- Interpretation of function symbols. -/
  funMap : {n : ℕ} → L.Func n → (Fin n → M) → M
  /-- Interpretation of relation symbols. -/
  relMap : {n : ℕ} → L.Rel n → (Fin n → M) → Prop

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

consLean 4Formally verified

/-- Extend an environment (an assignment `ρ` of elements to variables) by a value `a` for a
newly bound variable `0`; the old variable `i` becomes `i + 1`. -/
def cons {M : Type u} (a : M) (ρ : ℕ → M) : ℕ → M
  | 0 => a
  | i + 1 => ρ i

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

evalLean 4Formally verified

/-- The value of a term in a structure `S`, given values `ρ i` for the variables. -/
def Term.eval {M : Type u} (S : Structure L M) (ρ : ℕ → M) : Term L → M
  | .var i => ρ i
  | .func f ts => S.funMap f (fun i => (ts i).eval S ρ)

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

RealizeLean 4Formally verified

/-- **Satisfaction** `M ⊨ φ[ρ]`: the formula `φ` is true in the structure `S` when its free
variables take the values `ρ`. This is Tarski's definition, clause by clause; the quantifier
clauses range over all elements of the domain — *elements*, never subsets. -/
def Formula.Realize {M : Type u} (S : Structure L M) : Formula L → (ℕ → M) → Prop
  | .falsum, _ => False
  | .eq t u, ρ => t.eval S ρ = u.eval S ρ
  | .rel R ts, ρ => S.relMap R (fun i => (ts i).eval S ρ)
  | .imp φ ψ, ρ => φ.Realize S ρ → ψ.Realize S ρ
  | .and φ ψ, ρ => φ.Realize S ρ ∧ ψ.Realize S ρ
  | .or φ ψ, ρ => φ.Realize S ρ ∨ ψ.Realize S ρ
  | .all φ, ρ => ∀ a : M, φ.Realize S (cons a ρ)
  | .ex φ, ρ => ∃ a : M, φ.Realize S (cons a ρ)

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

HoldsLean 4Formally verified

/-- A formula **holds** in a structure if it is true under every assignment of the variables.
For a sentence (no free variables) the assignment does not matter, and this is `M ⊨ φ`. -/
def Formula.Holds {M : Type u} (S : Structure L M) (φ : Formula L) : Prop :=
  ∀ ρ : ℕ → M, φ.Realize S ρ

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Here is satisfaction unwound in an example: the group axioms as sentences, and the proof that $(\Z, +, 0, -)$ satisfies them, in which each sentence becomes an ordinary statement about integers:

GroupFuncLean 4Formally verified

/-- The function symbols of the signature of groups: a binary `mul`, a constant `one` and a
unary `inv`. -/
inductive GroupFunc : ℕ → Type
  | mul : GroupFunc 2
  | one : GroupFunc 0
  | inv : GroupFunc 1

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

groupAxiomsLean 4Formally verified

/-- **The group axioms as first-order sentences** (variables are de Bruijn indices; in
`∀x∀y∀z`, `z` is `var 0`, `y` is `var 1`, `x` is `var 2`):
`∀x∀y∀z (x·y)·z = x·(y·z)`, `∀x x·1 = x`, `∀x 1·x = x`, `∀x x·x⁻¹ = 1`, `∀x x⁻¹·x = 1`. -/
def groupAxioms : List (Formula sigGroup) :=
  let mul (s t : Term sigGroup) : Term sigGroup := .func GroupFunc.mul ![s, t]
  let one : Term sigGroup := .func GroupFunc.one ![]
  let inv (s : Term sigGroup) : Term sigGroup := .func GroupFunc.inv ![s]
  [ .all (.all (.all (.eq (mul (mul (.var 2) (.var 1)) (.var 0))
                          (mul (.var 2) (mul (.var 1) (.var 0)))))),
    .all (.eq (mul (.var 0) one) (.var 0)),
    .all (.eq (mul one (.var 0)) (.var 0)),
    .all (.eq (mul (.var 0) (inv (.var 0))) one),
    .all (.eq (mul (inv (.var 0)) (.var 0)) one) ]

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

intAddLean 4Formally verified

/-- The integers as a structure for the signature of groups: `·` is `+`, `1` is `0` and `⁻¹`
is negation. -/
def intAdd : Structure sigGroup ℤ where
  funMap := fun {n} f xs => match n, f, xs with
    | _, GroupFunc.mul, xs => xs 0 + xs 1
    | _, GroupFunc.one, _ => 0
    | _, GroupFunc.inv, xs => -xs 0
  relMap := fun R _ => Empty.elim R

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

intAdd_groupLean 4Proved here from basic factsFormally verified

/-- **`(ℤ, +, 0, −)` satisfies the group axioms.** Unwinding the definition of satisfaction turns
each sentence into an ordinary statement about integers — `(a + b) + c = a + (b + c)`,
`a + 0 = a`, … — which the ring-arithmetic lemmas prove. -/
theorem intAdd_group : ∀ φ ∈ groupAxioms, φ.Holds intAdd := by
  intro φ hφ ρ
  simp only [groupAxioms, List.mem_cons, List.not_mem_nil, or_false] at hφ
  rcases hφ with rfl | rfl | rfl | rfl | rfl
  · intro a b c
    show (a + b) + c = a + (b + c)
    exact Int.add_assoc a b c
  · intro a
    show a + 0 = a
    exact Int.add_zero a
  · intro a
    show 0 + a = a
    exact Int.zero_add a
  · intro a
    show a + -a = 0
    exact Int.add_right_neg a
  · intro a
    show -a + a = 0
    exact Int.add_left_neg a

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Substitution and the substitution lemma (Lemma 2). Moving a substitution under a quantifier uses up; instantiating the bound variable with a term uses inst:

substLean 4Formally verified

/-- Simultaneous substitution in a term: replace each variable `var i` by the term `σ i`. -/
def Term.subst (σ : ℕ → Term L) : Term L → Term L
  | .var i => σ i
  | .func f ts => .func f (fun i => (ts i).subst σ)

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

upLean 4Formally verified

/-- Moving a substitution under a quantifier: the newly bound variable `0` stays itself, and the
terms substituted for the other variables are shifted so that they do not get captured. -/
def up (σ : ℕ → Term L) : ℕ → Term L
  | 0 => .var 0
  | i + 1 => (σ i).shift

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

instLean 4Formally verified

/-- The substitution `φ(t)`: put the term `t` for the bound variable `0` and shift the other
variables down (they were one level deeper under the quantifier). -/
def inst (t : Term L) : ℕ → Term L
  | 0 => t
  | i + 1 => .var i

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

substLean 4Formally verified

/-- Capture-avoiding substitution in a formula. Under a quantifier the substitution is
replaced by `up σ`. -/
def Formula.subst : (ℕ → Term L) → Formula L → Formula L
  | _, .falsum => .falsum
  | σ, .eq t u => .eq (t.subst σ) (u.subst σ)
  | σ, .rel R ts => .rel R (fun i => (ts i).subst σ)
  | σ, .imp φ ψ => .imp (φ.subst σ) (ψ.subst σ)
  | σ, .and φ ψ => .and (φ.subst σ) (ψ.subst σ)
  | σ, .or φ ψ => .or (φ.subst σ) (ψ.subst σ)
  | σ, .all φ => .all (φ.subst (up σ))
  | σ, .ex φ => .ex (φ.subst (up σ))

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

shiftLean 4Formally verified

/-- Shift all free variables of a formula up by one. -/
def Formula.shift (φ : Formula L) : Formula L := φ.subst (fun i => .var (i + 1))

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

eval_substLean 4Proved here from basic factsFormally verified

/-- Substituting and then evaluating is evaluating in the environment of substituted values:
`⟦t[σ]⟧ρ = ⟦t⟧(i ↦ ⟦σ i⟧ρ)`. Induction on the term. -/
theorem Term.eval_subst (σ : ℕ → Term L) (ρ : ℕ → M) (t : Term L) :
    (t.subst σ).eval S ρ = t.eval S (fun i => (σ i).eval S ρ) := by
  induction t with
  | var i => rfl
  | func f ts ih => simp only [Term.subst, Term.eval, ih]

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

realize_substLean 4Proved here from basic factsFormally verified

/-- **The substitution lemma.** `M ⊨ φ[σ][ρ]` exactly when `M ⊨ φ[i ↦ ⟦σ i⟧ρ]`: substitution in
the syntax corresponds to changing the assignment in the semantics. Induction on `φ`; the
quantifier cases use `eval_up`. This lemma is the heart of the soundness proof for the
quantifier rules. -/
theorem Formula.realize_subst (φ : Formula L) :
    ∀ (σ : ℕ → Term L) (ρ : ℕ → M),
      (φ.subst σ).Realize S ρ ↔ φ.Realize S (fun i => (σ i).eval S ρ) := by
  induction φ with
  | falsum => intro σ ρ; exact Iff.rfl
  | eq t u => intro σ ρ; simp only [Formula.subst, Formula.Realize, Term.eval_subst]
  | rel R ts => intro σ ρ; simp only [Formula.subst, Formula.Realize, Term.eval_subst]
  | imp φ ψ ihφ ihψ => intro σ ρ; simp only [Formula.subst, Formula.Realize, ihφ, ihψ]
  | and φ ψ ihφ ihψ => intro σ ρ; simp only [Formula.subst, Formula.Realize, ihφ, ihψ]
  | or φ ψ ihφ ihψ => intro σ ρ; simp only [Formula.subst, Formula.Realize, ihφ, ihψ]
  | all φ ih => intro σ ρ; simp only [Formula.subst, Formula.Realize, ih, eval_up]
  | ex φ ih => intro σ ρ; simp only [Formula.subst, Formula.Realize, ih, eval_up]

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

realize_shiftLean 4Proved here from basic factsFormally verified

/-- A shifted formula does not see the newly bound variable: `M ⊨ φ↑[a, ρ] ↔ M ⊨ φ[ρ]`. -/
theorem Formula.realize_shift (φ : Formula L) (a : M) (ρ : ℕ → M) :
    φ.shift.Realize S (cons a ρ) ↔ φ.Realize S ρ := by
  rw [Formula.shift, Formula.realize_subst]
  exact Iff.rfl

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

realize_instLean 4Proved here from basic factsFormally verified

/-- Instantiating the bound variable by a term `t` is the same as giving it the value of `t`:
`M ⊨ φ(t)[ρ] ↔ M ⊨ φ[⟦t⟧ρ, ρ]`. -/
theorem Formula.realize_inst (φ : Formula L) (t : Term L) (ρ : ℕ → M) :
    (φ.subst (inst t)).Realize S ρ ↔ φ.Realize S (cons (t.eval S ρ) ρ) := by
  rw [Formula.realize_subst]
  have h : (fun i => (inst t i).eval S ρ) = cons (t.eval S ρ) ρ := by
    funext i
    cases i <;> rfl
  rw [h]

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

realize_shift plays the role of Lemma 1 for the eigenvariable conditions: in the rules allI and exE the assumptions are shifted, which is how "the variable $0$ is fresh" is expressed with de Bruijn indices.

Natural deduction and soundness (Theorem 3). The proof is one case per rule, as above:

DerivableLean 4Formally verified

/-- **Natural deduction**, in sequent form: `Derivable Γ φ` means that `φ` can be derived from
the list of assumptions `Γ`. One introduction and one elimination rule per connective, ex falso,
classical reductio ad absurdum, and two rules for equality. In `allI` the assumptions are
shifted, so the variable `0` is *fresh* — it occurs free in no assumption (the eigenvariable
condition); in `exE` the witness is likewise a fresh variable. -/
inductive Derivable : List (Formula L) → Formula L → Prop
  | assume {Γ : List (Formula L)} {φ : Formula L} : φ ∈ Γ → Derivable Γ φ
  | impI {Γ : List (Formula L)} {φ ψ : Formula L} :
      Derivable (φ :: Γ) ψ → Derivable Γ (.imp φ ψ)
  | impE {Γ : List (Formula L)} {φ ψ : Formula L} :
      Derivable Γ (.imp φ ψ) → Derivable Γ φ → Derivable Γ ψ
  | andI {Γ : List (Formula L)} {φ ψ : Formula L} :
      Derivable Γ φ → Derivable Γ ψ → Derivable Γ (.and φ ψ)
  | andE₁ {Γ : List (Formula L)} {φ ψ : Formula L} : Derivable Γ (.and φ ψ) → Derivable Γ φ
  | andE₂ {Γ : List (Formula L)} {φ ψ : Formula L} : Derivable Γ (.and φ ψ) → Derivable Γ ψ
  | orI₁ {Γ : List (Formula L)} {φ ψ : Formula L} : Derivable Γ φ → Derivable Γ (.or φ ψ)
  | orI₂ {Γ : List (Formula L)} {φ ψ : Formula L} : Derivable Γ ψ → Derivable Γ (.or φ ψ)
  | orE {Γ : List (Formula L)} {φ ψ χ : Formula L} : Derivable Γ (.or φ ψ) →
      Derivable (φ :: Γ) χ → Derivable (ψ :: Γ) χ → Derivable Γ χ
  | falsumE {Γ : List (Formula L)} {φ : Formula L} : Derivable Γ .falsum → Derivable Γ φ
  | raa {Γ : List (Formula L)} {φ : Formula L} : Derivable (φ.not :: Γ) .falsum → Derivable Γ φ
  | allI {Γ : List (Formula L)} {φ : Formula L} :
      Derivable (Γ.map Formula.shift) φ → Derivable Γ (.all φ)
  | allE {Γ : List (Formula L)} {φ : Formula L} (t : Term L) :
      Derivable Γ (.all φ) → Derivable Γ (φ.subst (inst t))
  | exI {Γ : List (Formula L)} {φ : Formula L} (t : Term L) :
      Derivable Γ (φ.subst (inst t)) → Derivable Γ (.ex φ)
  | exE {Γ : List (Formula L)} {φ ψ : Formula L} : Derivable Γ (.ex φ) →
      Derivable (φ :: Γ.map Formula.shift) ψ.shift → Derivable Γ ψ
  | eqRefl {Γ : List (Formula L)} (t : Term L) : Derivable Γ (.eq t t)
  | eqSubst {Γ : List (Formula L)} {φ : Formula L} {s t : Term L} : Derivable Γ (.eq s t) →
      Derivable Γ (φ.subst (inst s)) → Derivable Γ (φ.subst (inst t))

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

soundnessLean 4Proved here from basic factsFormally verified

/-- **The soundness theorem.** If `φ` is derivable from `Γ`, then `φ` is true in every structure,
under every assignment that makes all of `Γ` true: `Γ ⊢ φ` implies `Γ ⊨ φ`.
Proof by induction on the derivation, one case per rule, exactly as in the lesson. The
propositional rules are the truth-table facts; `raa` uses classical logic in the metatheory;
the quantifier rules use the substitution lemma (`realize_inst`) and the fact that shifted
formulas ignore the new variable (`realize_shift`). -/
theorem soundness {Γ : List (Formula L)} {φ : Formula L} (h : Derivable Γ φ) :
    ∀ {M : Type u} (S : Structure L M) (ρ : ℕ → M),
      (∀ ψ ∈ Γ, ψ.Realize S ρ) → φ.Realize S ρ := by
  induction h with
  | assume hφ => intro M S ρ hΓ; exact hΓ _ hφ
  | impI _ ih =>
    intro M S ρ hΓ hφ
    apply ih S ρ
    intro ψ hψ
    rcases List.mem_cons.1 hψ with rfl | hψ
    · exact hφ
    · exact hΓ ψ hψ
  | impE _ _ ih₁ ih₂ => intro M S ρ hΓ; exact ih₁ S ρ hΓ (ih₂ S ρ hΓ)
  | andI _ _ ih₁ ih₂ => intro M S ρ hΓ; exact ⟨ih₁ S ρ hΓ, ih₂ S ρ hΓ⟩
  | andE₁ _ ih => intro M S ρ hΓ; exact (ih S ρ hΓ).1
  | andE₂ _ ih => intro M S ρ hΓ; exact (ih S ρ hΓ).2
  | orI₁ _ ih => intro M S ρ hΓ; exact Or.inl (ih S ρ hΓ)
  | orI₂ _ ih => intro M S ρ hΓ; exact Or.inr (ih S ρ hΓ)
  | orE _ _ _ ih ih₁ ih₂ =>
    intro M S ρ hΓ
    rcases ih S ρ hΓ with hφ | hψ
    · apply ih₁ S ρ
      intro χ hχ
      rcases List.mem_cons.1 hχ with rfl | hχ
      · exact hφ
      · exact hΓ χ hχ
    · apply ih₂ S ρ
      intro χ hχ
      rcases List.mem_cons.1 hχ with rfl | hχ
      · exact hψ
      · exact hΓ χ hχ
  | falsumE _ ih => intro M S ρ hΓ; exact (ih S ρ hΓ).elim
  | @raa Γ φ _ ih =>
    intro M S ρ hΓ
    by_contra hn
    apply ih S ρ
    intro ψ hψ
    rcases List.mem_cons.1 hψ with rfl | hψ
    · exact hn
    · exact hΓ ψ hψ
  | @allI Γ φ _ ih =>
    intro M S ρ hΓ a
    apply ih S (cons a ρ)
    intro ψ hψ
    obtain ⟨χ, hχ, rfl⟩ := List.mem_map.1 hψ
    exact (Formula.realize_shift S χ a ρ).2 (hΓ χ hχ)
  | @allE Γ φ t _ ih =>
    intro M S ρ hΓ
    exact (Formula.realize_inst S φ t ρ).2 (ih S ρ hΓ (t.eval S ρ))
  | @exI Γ φ t _ ih =>
    intro M S ρ hΓ
    exact ⟨t.eval S ρ, (Formula.realize_inst S φ t ρ).1 (ih S ρ hΓ)⟩
  | @exE Γ φ ψ _ _ ih₁ ih₂ =>
    intro M S ρ hΓ
    obtain ⟨a, ha⟩ := ih₁ S ρ hΓ
    have h := ih₂ S (cons a ρ) (by
      intro χ hχ
      rcases List.mem_cons.1 hχ with rfl | hχ
      · exact ha
      · obtain ⟨θ, hθ, rfl⟩ := List.mem_map.1 hχ
        exact (Formula.realize_shift S θ a ρ).2 (hΓ θ hθ))
    exact (Formula.realize_shift S ψ a ρ).1 h
  | eqRefl t => intro M S ρ _; rfl
  | @eqSubst Γ φ s t _ _ ih₁ ih₂ =>
    intro M S ρ hΓ
    have hst : s.eval S ρ = t.eval S ρ := ih₁ S ρ hΓ
    have hs := (Formula.realize_inst S φ s ρ).1 (ih₂ S ρ hΓ)
    rw [hst] at hs
    exact (Formula.realize_inst S φ t ρ).2 hs

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Using soundness. A derivation of $\forall x\, \varphi \to \exists x\, \varphi$ , and a proof that $\exists x\, P(x) \to \forall x\, P(x)$ is not derivable, by the two-element countermodel:

all_imp_exLean 4Proved here from basic factsFormally verified

/-- **`∀x φ → ∃x φ` is derivable**: assume `∀x φ`, instantiate it at the variable `0`, and use
that same variable as the witness for `∃x φ`. By soundness it is true in every structure — which
is only correct because structures are non-empty (an environment `ρ : ℕ → M` needs an element). -/
theorem all_imp_ex (φ : Formula L) : Derivable [] (.imp (.all φ) (.ex φ)) :=
  .impI (.exI (.var 0) (.allE (.var 0) (.assume (List.mem_singleton_self _))))

Axioms used: No axiomsformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

boolPLean 4Formally verified

/-- The two-element structure `{false, true}` in which `P` holds of `true` only. -/
def boolP : Structure sigP Bool where
  funMap := fun f _ => Empty.elim f
  relMap := fun {n} R xs => match n, R, xs with
    | _, PRel.P, xs => xs 0 = true

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

ex_imp_all_not_derivableLean 4Proved here from basic factsFormally verified

/-- **`∃x P(x) → ∀x P(x)` is not derivable.** If it were, soundness would make it true in every
structure; but in `boolP` some element satisfies `P` (namely `true`) and not every element does
(`false` does not). Soundness turns a single countermodel into a proof of underivability. -/
theorem ex_imp_all_not_derivable : ¬ Derivable [] (.imp (.ex (pAt 0)) (.all (pAt 0))) := by
  intro h
  have htrue := soundness h boolP (fun _ => true) (by simp)
  have hfalse : false = true := htrue ⟨true, rfl⟩ false
  exact Bool.false_ne_true hfalse

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Isomorphism invariance (Theorem 4), and its application to $(\N, <)$ and $(\Z, <)$ :

IsoLean 4Formally verified

/-- An **isomorphism of structures**: a bijection that commutes with the interpretation of every
function symbol and preserves and reflects every relation. -/
structure Iso {M : Type u} {N : Type v} (S : Structure L M) (T : Structure L N) where
  /-- The underlying bijection. -/
  toEquiv : M ≃ N
  /-- It commutes with the functions. -/
  map_fun : ∀ {n} (f : L.Func n) (xs : Fin n → M),
    toEquiv (S.funMap f xs) = T.funMap f (fun i => toEquiv (xs i))
  /-- It preserves and reflects the relations. -/
  map_rel : ∀ {n} (R : L.Rel n) (xs : Fin n → M),
    S.relMap R xs ↔ T.relMap R (fun i => toEquiv (xs i))

Axioms used: Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

realizeLean 4Proved here from basic factsFormally verified

/-- **Isomorphisms preserve truth**: `M ⊨ φ[ρ]` if and only if `N ⊨ φ[e ∘ ρ]`, for every
formula. Induction on `φ`: equations use that `e` is injective, atomic formulas use `map_rel`,
and the quantifier cases use that `e` is surjective (every element of `N` is `e(a)`). -/
theorem Iso.realize (e : Iso S T) (φ : Formula L) :
    ∀ ρ : ℕ → M, φ.Realize S ρ ↔ φ.Realize T (fun i => e.toEquiv (ρ i)) := by
  have hcons : ∀ (a : M) (ρ : ℕ → M),
      (fun i => e.toEquiv (cons a ρ i)) = cons (e.toEquiv a) (fun i => e.toEquiv (ρ i)) := by
    intro a ρ
    funext i
    cases i <;> rfl
  induction φ with
  | falsum => intro ρ; exact Iff.rfl
  | eq t u =>
    intro ρ
    simp only [Formula.Realize, ← e.eval, e.toEquiv.apply_eq_iff_eq]
  | rel R ts =>
    intro ρ
    simp only [Formula.Realize, ← e.eval]
    exact e.map_rel R _
  | imp φ ψ ihφ ihψ => intro ρ; simp only [Formula.Realize, ihφ, ihψ]
  | and φ ψ ihφ ihψ => intro ρ; simp only [Formula.Realize, ihφ, ihψ]
  | or φ ψ ihφ ihψ => intro ρ; simp only [Formula.Realize, ihφ, ihψ]
  | all φ ih =>
    intro ρ
    simp only [Formula.Realize]
    constructor
    · intro h b
      have hb := (ih (cons (e.toEquiv.symm b) ρ)).1 (h _)
      rw [hcons, Equiv.apply_symm_apply] at hb
      exact hb
    · intro h a
      rw [ih, hcons]
      exact h _
  | ex φ ih =>
    intro ρ
    simp only [Formula.Realize]
    constructor
    · rintro ⟨a, ha⟩
      refine ⟨e.toEquiv a, ?_⟩
      rw [← hcons, ← ih]
      exact ha
    · rintro ⟨b, hb⟩
      refine ⟨e.toEquiv.symm b, ?_⟩
      rw [ih, hcons, Equiv.apply_symm_apply]
      exact hb

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

holds_iffLean 4Proved here from basic factsFormally verified

/-- **Isomorphic structures satisfy exactly the same formulas** (in particular the same
sentences). Every assignment in `N` is `e ∘ ρ` for an assignment `ρ` in `M` (take
`ρ = e⁻¹ ∘ ρ'`), so "true under all assignments" transfers both ways. -/
theorem Iso.holds_iff (e : Iso S T) (φ : Formula L) : φ.Holds S ↔ φ.Holds T := by
  constructor
  · intro h ρ'
    have := (e.realize φ (fun i => e.toEquiv.symm (ρ' i))).1 (h _)
    simpa only [Equiv.apply_symm_apply] using this
  · intro h ρ
    exact (e.realize φ ρ).2 (h _)

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

hasLeastLean 4Formally verified

/-- The sentence "there is a least element", `∃x ∀y ¬(y < x)`. Inside both quantifiers, `y` is
`var 0` and `x` is `var 1`. -/
def hasLeast : Formula sigOrd :=
  .ex (.all (Formula.not (.rel OrdRel.lt ![.var 0, .var 1])))

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

nat_hasLeastLean 4Proved here from basic factsFormally verified

/-- `(ℕ, <) ⊨ ∃x ∀y ¬(y < x)`: take `x = 0`; no natural number is below `0`. -/
theorem nat_hasLeast : hasLeast.Holds (orderStructure ℕ) := by
  intro ρ
  refine ⟨0, fun b hb => ?_⟩
  exact Nat.not_lt_zero b hb

Axioms used: propextformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

int_not_hasLeastLean 4Proved here from basic factsFormally verified

/-- `(ℤ, <) ⊭ ∃x ∀y ¬(y < x)`: whatever `x` is proposed, `y = x − 1` is smaller. -/
theorem int_not_hasLeast : ¬ hasLeast.Holds (orderStructure ℤ) := by
  intro h
  obtain ⟨a, ha⟩ := h (fun _ => 0)
  exact ha (a - 1) (show a - 1 < a by omega)

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

nat_not_iso_intLean 4Proved here from basic factsFormally verified

/-- **`(ℕ, <)` and `(ℤ, <)` are not isomorphic.** An order isomorphism `ℕ ≃o ℤ` would be an
isomorphism of `{<}`-structures (`a < b ↔ e a < e b`), and isomorphic structures satisfy the
same sentences; but "there is a least element" is true in `ℕ` and false in `ℤ`. -/
theorem nat_not_iso_int : IsEmpty (ℕ ≃o ℤ) := by
  constructor
  intro e
  let iso : Iso (orderStructure ℕ) (orderStructure ℤ) :=
    { toEquiv := e.toEquiv
      map_fun := fun f _ => Empty.elim f
      map_rel := fun {n} R xs => match n, R, xs with
        | _, OrdRel.lt, xs => e.lt_iff_lt.symm }
  exact int_not_hasLeast ((iso.holds_iff hasLeast).1 nat_hasLeast)

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

Mathlib's version of Theorem 4, for its own syntax:

iso_sentence_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version of isomorphism invariance, for its own syntax (`FirstOrder.Language`,
`Sentence`) and semantics (`Sentence.Realize`): an isomorphism of `L`-structures `M ≃[L] N`
preserves the truth of every sentence. This applies
`FirstOrder.Language.StrongHomClass.realize_sentence`. -/
theorem iso_sentence_library {L : FirstOrder.Language} {M : Type u} {N : Type v}
    [L.Structure M] [L.Structure N] (e : L.Equiv M N) (φ : L.Sentence) :
    φ.Realize M ↔ φ.Realize N :=
  FirstOrder.Language.StrongHomClass.realize_sentence e φ

Axioms used: propext, Quot.soundformal/Lumenary/FirstOrderLogic.leanTry it in the Lean web editor

What is and is not formalised. Formalised and proved here: the syntax, Tarski semantics, the substitution lemma, natural deduction, soundness, isomorphism invariance, and the examples. Simplifications: constants are function symbols of arity $0$ , contexts are lists, and the de Bruijn presentation replaces named variables. Not formalised: Gödel's completeness theorem (see the completeness lesson for what Mathlib and the Lumenary formalise around it).

ComputationC

Truth in every small structure

Tarski's definition is an algorithm when the domain is finite: a quantifier is a loop over the elements. The experiment stores formulas in the signature $\{R\}$ as nested Python tuples, implements satisfaction clause by clause, and evaluates the axioms of equivalence relations, partial orders and linear orders in all $2^9 = 512$ structures on a three-element domain. It counts models and models up to isomorphism (a theory usually has many non-isomorphic models), checks that isomorphic copies satisfy the same sentences, and separates the five partial orders on three points with four sentences.

Truth in every structure with at most three elementsPythonExact computationExhaustive finite checkComputationally tested

"""Tarski's definition of truth, run on every structure with three elements.

Formulas in the signature {R} (one binary relation) are stored as nested
tuples, and `satisfies` follows the definition of satisfaction clause by
clause: a quantifier becomes a loop over the domain, never over subsets. We
evaluate the axioms of equivalence relations, partial orders and linear
orders on all 2^(n*n) relations on {0, ..., n-1} for n <= 3, count the
models and the models up to isomorphism, and check on every structure that
isomorphic structures satisfy the same sentences. Four sentences then tell
the five partial orders on three points apart. Exact and exhaustive for
these finite domains.
"""

from itertools import permutations, product

def satisfies(domain, rel, formula, env=None):
    """Tarski's definition: is `formula` true in (domain, rel) under env?"""
    env = env or {}
    tag = formula[0]
    if tag == "R":
        return (env[formula[1]], env[formula[2]]) in rel
    if tag == "eq":
        return env[formula[1]] == env[formula[2]]
    if tag == "not":
        return not satisfies(domain, rel, formula[1], env)
    if tag == "and":
        return (satisfies(domain, rel, formula[1], env)
                and satisfies(domain, rel, formula[2], env))
    if tag == "or":
        return (satisfies(domain, rel, formula[1], env)
                or satisfies(domain, rel, formula[2], env))
    if tag == "imp":
        return (not satisfies(domain, rel, formula[1], env)
                or satisfies(domain, rel, formula[2], env))
    if tag in ("all", "some"):
        var, body = formula[1], formula[2]
        values = (satisfies(domain, rel, body, {**env, var: a})
                  for a in domain)
        return all(values) if tag == "all" else any(values)
    raise ValueError(f"unknown formula {formula!r}")

def R(x, y):
    """The atomic formula R(x, y)."""
    return ("R", x, y)

REFLEXIVE = ("all", "x", R("x", "x"))
SYMMETRIC = ("all", "x", ("all", "y", ("imp", R("x", "y"), R("y", "x"))))
TRANSITIVE = ("all", "x", ("all", "y", ("all", "z", (
    "imp", ("and", R("x", "y"), R("y", "z")), R("x", "z")))))
ANTISYMMETRIC = ("all", "x", ("all", "y", (
    "imp", ("and", R("x", "y"), R("y", "x")), ("eq", "x", "y"))))
TOTAL = ("all", "x", ("all", "y", ("or", R("x", "y"), R("y", "x"))))

THEORIES = {
    "equivalence relation": [REFLEXIVE, SYMMETRIC, TRANSITIVE],
    "partial order": [REFLEXIVE, ANTISYMMETRIC, TRANSITIVE],
    "linear order": [REFLEXIVE, ANTISYMMETRIC, TRANSITIVE, TOTAL],
}

SENTENCES = {
    "least": ("some", "x", ("all", "y", R("x", "y"))),
    "greatest": ("some", "x", ("all", "y", R("y", "x"))),
    "total": TOTAL,
    "comparable": ("some", "x", ("some", "y", (
        "and", ("not", ("eq", "x", "y")), R("x", "y")))),
}

def all_relations(n):
    """Every binary relation on {0, ..., n-1}, as a frozenset of pairs."""
    pairs = list(product(range(n), repeat=2))
    return [frozenset(p for p, keep in zip(pairs, bits) if keep)
            for bits in product((False, True), repeat=len(pairs))]

def models(n, theory):
    """Relations on {0..n-1} satisfying every sentence of the theory."""
    domain = range(n)
    return [r for r in all_relations(n)
            if all(satisfies(domain, r, s) for s in theory)]

def relabel(rel, perm):
    """The isomorphic copy of rel obtained by renaming x as perm[x]."""
    return frozenset((perm[a], perm[b]) for a, b in rel)

def canonical(rel, n):
    """A label for the isomorphism class of (range(n), rel)."""
    return min(tuple(sorted(relabel(rel, p))) for p in permutations(range(n)))

def invariance_holds(n, sentences):
    """Do all relabellings of every relation satisfy the same sentences?"""
    domain = range(n)
    for rel in all_relations(n):
        truth = [satisfies(domain, rel, s) for s in sentences]
        for perm in permutations(range(n)):
            copy = relabel(rel, perm)
            if [satisfies(domain, copy, s) for s in sentences] != truth:
                return False
    return True

def main():
    print("Models of three theories in the signature {R}, domain {0..n-1}")
    print(f"{'theory':<22}{'n=1':>5}{'n=2':>5}{'n=3':>5}   up to iso (n=3)")
    for name, theory in THEORIES.items():
        counts = [len(models(n, theory)) for n in (1, 2, 3)]
        classes = len({canonical(r, 3) for r in models(3, theory)})
        print(f"{name:<22}" + "".join(f"{c:>5}" for c in counts)
              + f"   {classes}")
    ok = invariance_holds(3, list(SENTENCES.values()))
    print("Isomorphic copies agree on all four sentences below (512")
    print(f"relations x 6 relabellings): {ok}")
    print()
    print("The partial orders on 3 points up to isomorphism, and which")
    print("sentences they satisfy (least, greatest, total, comparable):")
    seen = {}
    for r in models(3, THEORIES["partial order"]):
        seen.setdefault(canonical(r, 3), r)
    for key in sorted(seen, key=len):
        strict = sorted((a, b) for a, b in seen[key] if a != b)
        truth = ["T" if satisfies(range(3), seen[key], s) else "F"
                 for s in SENTENCES.values()]
        print(f"  x < y for (x, y) in {str(strict):<26} {' '.join(truth)}")
    print()
    print("Epistemic status: exact and exhaustive for domains with at most")
    print("three elements. Truth in an infinite structure cannot be decided")
    print("by looping over the domain, and isomorphism invariance for all")
    print("structures is the theorem proved in the lesson, not this check.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The evidence is exact and exhaustive for these finite structures, nothing more. For infinite structures the loop never ends — and in fact, as Church and Turing showed in 1936, no algorithm decides whether a first-order sentence is valid.

Explore

Explore: structures you can see

A graph is a structure. A graph is a structure for the signature $\{E\}$ , with $E$ the adjacency relation. Use the Degrees tab to decide which of these sentences are true in each graph: $\forall x\, \exists y\, E(x, y)$ (no isolated vertex); $\exists x\, \forall y\, (\neg x = y \to E(x, y))$ (some vertex is adjacent to all others); $\forall x\, \exists y\, \exists z\, (\neg y = z \wedge E(x, y) \wedge E(x, z))$ (every degree is at least $2$ ); $\neg \exists x\, \exists y\, \exists z\, (E(x, y) \wedge E(y, z) \wedge E(x, z))$ (no triangle). Then try the Colouring tab: "can be coloured with three colours" is true of some of these graphs and false of others, yet it is not expressible by a first-order sentence in $\{E\}$ that works for all graphs — it needs quantifiers over sets of vertices.

Which sentences are true in this graph?

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

Graph

|V| = 6|E| = 10Select a vertex to see the edges that meet there.

deg(A) = 3deg(B) = 3deg(C) = 3deg(D) = 3deg(E) = 3deg(H) = 5

3 + 3 + 3 + 3 + 3 + 5 = 20 = 2 × 10

Every edge has two ends, so it adds exactly 2 to the total: the degrees add up to 20 = 2 × 10. This is the handshake lemma, Σ deg(v) = 2|E|.

Vertices of odd degree: 6. This number is always even, because the total is even.

Tautologies are valid, but validity is more. If a propositional formula is a tautology, every sentence obtained by substituting first-order sentences for its letters is valid. For instance $(p \to q) \wedge p \to q$ is a tautology, so $(\forall x\, P(x) \to \exists y\, Q(y)) \wedge \forall x\, P(x) \to \exists y\, Q(y)$ is valid. Now type $p \to q$ : it is not a tautology, yet the sentence $\forall x\, P(x) \to \exists x\, P(x)$ with this skeleton is valid. Its validity comes from the meaning of the quantifiers (and non-empty domains), which no truth table can see.

The propositional skeleton of a first-order sentence

Type a formula of propositional logic and see its value in every possible case.

Formula

Read as: ((p → q) ∧ p) → q

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Tautology — true in all 4 rows.

p	q	p → q	(p → q) ∧ p	(p → q) ∧ p → q
T	T	T	T	T
T	F	F	F	T
F	T	T	F	T
F	F	T	F	T

4 rows: one for every way of making the 2 variables true or false.

Exercises

1. First-order logic

Warm-upHuman

In the signature of fields $\{+, \cdot, -, 0, 1\}$ , which sentence says "every non-zero element has a multiplicative inverse"?

Choose one

\forall x\, \big(\neg(x = 0) \to \exists y\ (x \cdot y = 1)\big)

\exists y\, \forall x\, \big(\neg(x = 0) \to x \cdot y = 1\big)

\forall x\, \exists y\, \big(\neg(x = 0) \wedge x \cdot y = 1\big)

\forall x\ (x \cdot x^{-1} = 1)

2. First-order logic

Warm-upHuman

Let $\mathcal{C} = (\{1, 2, 3\}, E)$ with $E = \{(1,2), (2,3), (3,1)\}$ (a directed triangle). Which sentences are true in $\mathcal{C}$ ? Choose all that apply.

Choose all that apply

\forall x\, \exists y\ E(x, y)

\exists y\, \forall x\ E(x, y)

\forall x\, \forall y\, \big(E(x, y) \to \neg E(y, x)\big)

\forall x\, \forall y\, \forall z\, \big(E(x, y) \wedge E(y, z) \to E(x, z)\big)

\forall x\, \exists y\, \exists z\, \big(E(x, y) \wedge E(y, z) \wedge E(z, x)\big)

3. First-order logic

CoreHuman

Which of these properties of a structure $(M, <)$ can be expressed by a single first-order sentence in the signature $\{<\}$ ? Choose all that apply.

Choose all that apply

There is a least element.Between any two elements there is a third.Every non-empty subset has a least element.There are exactly three elements.There are only finitely many elements.

4. First-order logic

CoreHuman

Which statement is the soundness theorem?

Choose one

\Gamma \vdash \varphi

then

\Gamma \models \varphi

.If

\Gamma \models \varphi

then

\Gamma \vdash \varphi

.Every consistent theory has a model.There is an algorithm deciding whether

\Gamma \vdash \varphi

5. First-order logic

CoreHuman

Someone "derives" $P(y) \vdash \forall x\, P(x)$ as follows: (1) $P(y) \vdash P(y)$ by assumption; (2) $P(y) \vdash \forall x\, P(x)$ by $\forall$ I. Which statement is right?

Choose one

Step 2 is illegal:

\forall

I requires that

y

is not free in the assumptions, but

y

is free in

P(y)

.The derivation is correct.Step 1 is illegal: one cannot assume a formula with a free variable.It needs

\forall

E instead of

\forall

6. First-order logic

CoreHuman

Which sentence proves that $(\mathbb{Z}, <)$ and $(\mathbb{Q}, <)$ are not isomorphic?

Choose one

\forall x\, \forall y\, \big(x < y \to \exists z\, (x < z \wedge z < y)\big)

\forall x\, \exists y\ (y < x)

\forall x\, \exists y\ (x < y)

"There are countably many elements."

7. First-order logic

StretchFormal

In the Lean formalisation, the rule allI : Derivable (Γ.map Formula.shift) φ → Derivable Γ (.all φ) shifts every assumption (variable $i$ becomes $i + 1$ ) before deriving the body φ. What does the shift achieve?

Choose one

It makes the de Bruijn variable

0

fresh — it occurs free in no assumption — which is the eigenvariable condition of

\forall

I.It renames bound variables to avoid capture during substitution.It weakens the assumptions, so that fewer formulas are derivable.Nothing: it is needed only to make the types match.

8. First-order logic

CoreComputational

On a finite domain, quantifiers are loops. Write forall(domain, pred) and exists(domain, pred), and use them to write serial(domain, rel), which decides $\forall x\, \exists y\ R(x, y)$ for a relation rel given as a set of pairs, and has_hub(domain, rel), which decides $\exists y\, \forall x\ R(x, y)$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

Confusing $\models$ with $\vdash$ . $\Gamma \models \varphi$ is about truth in all models — a statement quantifying over all structures. $\Gamma \vdash \varphi$ is about the existence of a finite derivation — a combinatorial statement about strings. They are defined completely differently; soundness and Gödel's completeness theorem are the (non-trivial!) theorems that make them coincide.

Misconception

Quantifying over subsets in a first-order formula. In a first-order formula, $\forall x$ and $\exists x$ range over elements of the domain. "For every subset $S$ …" is second-order; first-order theories approximate it with schemas (one axiom per formula), as in induction. In the language of set theory the elements are sets, so there "every subset" becomes first-order — at the price of moving to a different structure.

Misconception

"A theory determines its model." Most theories have many non-isomorphic models: the group axioms have models of every size, abelian and not; the axioms of linear orders have a finite model $\{0 < 1 < \dots < n - 1\}$ for every $n \ge 1$ , and infinite models $\N$ , $\Z$ , $\Q$ , $\R$ , … Even a complete theory such as that of $(\Q, <)$ has non-isomorphic models, such as $(\R, <)$ . By the Löwenheim–Skolem theorem, a theory with an infinite model has models of every infinite size.

Misconception

"The order of quantifiers doesn't matter." $\forall x\, \exists y\, (y > x)$ is true in $(\N, <)$ , while $\exists y\, \forall x\, (y > x)$ is false. Quantifiers of the same kind can be swapped; $\forall$ and $\exists$ cannot. Continuity versus uniform continuity is the classic example.

Misconception

"Domains may be empty." In standard first-order logic every structure is non-empty, which is why $\forall x\, \varphi \to \exists x\, \varphi$ is valid and derivable. Logics allowing empty domains ("free" or "inclusive" logics) exist, but they need different rules.

ViewpointsH

Many ways of seeing

Algebra— Equations, varieties and Birkhoff's theorem

Many algebraic theories — monoids, groups, rings, vector spaces over a fixed field, lattices — are axiomatised by equations, universally quantified identities $\forall \vec x\ (s = t)$ . Garrett Birkhoff (1935) characterised such classes exactly: a class of structures is defined by equations if and only if it is closed under homomorphic images, substructures and products (the HSP theorem). So fields are not an equational class: $\mathbb{F}_2 \times \mathbb{F}_2$ has zero divisors, so it is not a field, and closure under products fails — the field axiom $\forall x\, (\neg x = 0 \to \exists y\, xy = 1)$ is not an equation. Logic and algebra meet again in the Lindenbaum–Tarski algebra: formulas up to provable equivalence form a Boolean algebra, and soundness and completeness become statements about its homomorphisms to $\{0, 1\}$ .

Topology— Compactness is compactness

Fix a signature and consider the set $S$ of all complete theories of structures, $\mathrm{Th}(\mathcal{M}) = \{ \sigma \mid \mathcal{M} \models \sigma \}$ (two structures giving the same set count once). Give it the topology whose basic open sets are $[\varphi] = \{ T \in S \mid \varphi \in T \}$ . The sets $[\varphi]$ are both open and closed, and $S$ is a compact Hausdorff space — a Stone space. Its compactness is precisely the compactness theorem of first-order logic: a set of sentences has a model as soon as every finite subset does. (Stone's representation theorem (1936) makes this precise: Boolean algebras correspond to such spaces.) Model theorists study type spaces, spaces of this kind built from formulas with free variables, with genuinely topological methods: isolated points, Cantor–Bendixson rank, and so on. See model theory.

Geometry— Quantifier elimination and semialgebraic geometry

Alfred Tarski proved (published 1948–1951) that the first-order theory of the real ordered field $(\R, +, \cdot, 0, 1, <)$ admits quantifier elimination: every formula is equivalent to one without quantifiers, a Boolean combination of polynomial inequalities. Geometrically (the Tarski–Seidenberg theorem): the projection of a semialgebraic set — a set in $\R^n$ defined by polynomial equations and inequalities — is again semialgebraic. For example, $\exists y\, (x^2 + y^2 = 1)$ defines the projection of the circle onto the $x$ -axis, and it is equivalent to the quantifier-free formula $-1 \le x \le 1$ . As a consequence, elementary Euclidean geometry is decidable — see Euclidean geometry.

Computation— Validity is semi-decidable but not decidable

By the completeness theorem, a sentence is valid iff it has a derivation; derivations are finite strings that can be listed one by one and checked mechanically. So there is a procedure that halts with "yes" exactly on the valid sentences: validity is semi-decidable (recursively enumerable). But Alonzo Church and Alan Turing (1936) proved that no algorithm decides validity — it never answers "no" correctly on all invalid sentences — settling Hilbert's Entscheidungsproblem negatively. Restricted fragments can be decidable: Presburger arithmetic ( $\N$ with $+$ only) is decidable, and so is monadic first-order logic (only unary relations). See computability. Automated theorem provers and proof assistants such as Lean live in the gap between these two facts.

Category theory— Quantifiers as adjoints

F. William Lawvere (1969) observed that the quantifiers are characterised by universal properties. For formulas in variables $x, y$ and in $x$ alone, ordered by entailment, "weakening" regards a formula $\psi(x)$ as a formula in $x, y$ . Then $\exists y$ and $\forall y$ are its left and right adjoints: $\exists y\, \varphi(x, y) \vdash \psi(x)$ iff $\varphi(x, y) \vdash \psi(x)$ , and $\psi(x) \vdash \forall y\, \varphi(x, y)$ iff $\psi(x) \vdash \varphi(x, y)$ — which are exactly the rules $\exists$ E and $\forall$ I with their eigenvariable conditions. This leads to the interpretation of first-order logic in categories other than sets, such as toposes: see categorical logic.

History & global context

History and global context

The study of valid inference is ancient: Aristotle's syllogistic, the propositional logic of the Stoics, and, in India, the Nyāya school's analysis of inference and the later Navya-Nyāya technical language. Medieval logicians writing in Arabic and Latin developed these traditions further. Quantifiers as we use them are much younger.
George Boole (1847, 1854) made propositional logic algebraic. Gottlob Frege's Begriffsschrift (1879) introduced quantifiers and a formal proof system; Charles S. Peirce and his student Oscar Howard Mitchell introduced quantifiers independently (1883–1885). Giuseppe Peano's notation and Whitehead and Russell's Principia Mathematica (1910–1913) spread the ideas.
Leopold Löwenheim (1915) and Thoralf Skolem (1920) proved the first theorems about models; David Hilbert and Wilhelm Ackermann's textbook (1928) isolated first-order logic and asked whether its rules are complete. Kurt Gödel proved completeness in his 1929 doctoral thesis (published 1930). Alfred Tarski gave the definition of truth in a structure ("The concept of truth in formalized languages", in Polish 1933).
Natural deduction was introduced independently by Gerhard Gentzen and Stanisław Jaśkowski in 1934. Church and Turing proved the undecidability of validity in 1936; Leon Henkin's proof of completeness (1949) is the one usually taught today.

Saying exactly what we mean

Syntax, meaning and proof

The language and its meaning

Substitution

Natural deduction

Writing and reading formulas

Soundness and invariance

A first-order logic built in Lean

Truth in every small structure

Explore: structures you can see

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading