Predicate Calculus

Definition

Predicate calculus is a family of formal system extending propositional logic to include quantifiers, variables, and predicates. It distinguishes between objects (terms) and properties of objects (formulas).

First-order logic restricts the predicates to only predicates over terms. Second-order logic adds in predicate variables, and enables quantification over these varibles. Higher-order logic adds in predicates over predicates as well as terms.

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 (Logic) (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