First-Order Logic (Classical)

Definition

First-order logic is a formal system extending propositional logic to include quantifiers, variables, and predicates. It distinguishes between objects (terms) and properties of objects (formulas). Unlike second-order logic, quantification occurs only over variables, not over predicates or functions.

Syntax

The syntax is defined relative to a signature $\Sigma$ containing function symbols and relation symbols with fixed arities.

Alphabet

• Variable: $x,y,z,\dots$
• Logical connectives: $\neg ,\wedge ,\vee ,\to ,\perp$
• Quantifiers: $\forall ,\exists$
• Equality: $=$ (typically treated as a logical constant)
• Auxiliary symbols: parentheses.

Terms

The set of terms is defined inductively:

1. Any variable is a term.
2. If $f\in \Sigma$ is an $n$-ary function symbol and $t_1,\dots ,t_n$ are terms, then $f(t_1,\dots ,t_n)$ is a term.

Formulas

The set of formulas is defined inductively:

1. If $R\in \Sigma$ is an $n$-ary relation symbol and $t_1,\dots ,t_n$ are terms, $R(t_1,\dots ,t_n)$ is an atomic formula.
2. If $t_1,t_2$ are terms, $t_1=t_2$ is an atomic formula.
3. If $\varphi ,\psi$ are formulas, then $\neg \varphi$, $\varphi \wedge \psi$, $\varphi \vee \psi$, $\varphi \to \psi$ are formulas.
4. If $\varphi$ is a formula and $x$ is a variable, $\forall x.\varphi$ and $\exists x.\varphi$ are formulas.

Semantics

Semantics are defined via Tarski’s definition of truth relative to a structure $\mathcal{M}=(D,I)$.

• $D$ is a non-empty domain (universe).
• $I$ interprets $n$-ary function symbols as functions $D^n\to D$ and $n$-ary relation symbols as subsets of $D^n$.

Satisfaction

Let $\sigma :\text{Var}\to D$ be a variable assignment. The satisfaction relation $\mathcal{M},\sigma \models \varphi$ is defined inductively.

$$\begin{array}{rl}\mathcal{M},\sigma \models \forall x.\varphi & ⟺\text{for all }d\in D,\mathcal{M},\sigma [x\mapsto d]\models \varphi \\ \mathcal{M},\sigma \models \exists x.\varphi & ⟺\text{there exists }d\in D\text{ s.t. }\mathcal{M},\sigma [x\mapsto d]\models \varphi \end{array}$$

Metatheoretic Properties

• Soundness: If $\Gamma ⊢\varphi$, then $\Gamma \models \varphi$.
• Completeness (Gödel): If $\Gamma \models \varphi$, then $\Gamma ⊢\varphi$.
• Compactness: A set of sentences is satisfiable iff every finite subset is satisfiable.
• Löwenheim-Skolem: If a countable theory has an infinite model, it has models of all infinite cardinalities.
• Incompleteness (Gödel): Any sufficiently strong consistent effective theory containing arithmetic is incomplete.
• Undecidability (Church-Turing): The decision problem for validity is undecidable (semidecidable).

Relation to Type Theory

In the context of the Curry-Howard Correspondance:

• Universal quantification $\forall x.P(x)$ corresponds to the dependent product type $\Pi (x:A).P(x)$.
• Existential quantification $\exists x.P(x)$ corresponds to the dependent sum type $\Sigma (x:A).P(x)$ (specifically the propositional truncation thereof in HoTT to ensure proof irrelevance).
• Predicates are modeled as type families $P:A\to \mathcal{U}$.

See also

Intuinistic First-Order Logic