Predicate Logic

Definition

Predicate logic or predicate calculus is a family of formal systems extending propositional logic by adding terms, variables, predicates, and quantifiers. It distinguishes between objects, represented by terms, and statements about objects, represented by formulas.

First-order logic restricts quantification to individual objects in a domain. Second-order logic also allows quantification over predicates or relations, and higher-order logic iterates this further.

Predicate logic may be given either a classical or an intuitionistic proof theory. The intuitionistic first-order fragment rejects specifically classical principles such as Law of the Excluded Middle and Double Negation Elimination.

Language

A first-order language consists of:

• variables
• function symbols
• relation symbols
• constant symbols
• logical symbols such as $\perp$, $\wedge$, $\vee$, $\to$, $\forall$, and $\exists$

Terms are built from variables and function symbols. Formulas are built from atomic formulas using propositional connectives and quantifiers.

Judgments have the form $\Gamma ⊢\phi$, where $\Gamma$ is a context of assumptions and $\phi$ is a formula.

Deduction

The deductive rules for the propositional connectives are inherited from propositional logic. Predicate logic adds quantifier rules.

For universal quantification:

$$\frac{\Gamma ⊢\phi (x)x\notin FV(\Gamma )}{\Gamma ⊢\forall x.\phi (x)}\frac{\Gamma ⊢\forall x.\phi (x)}{\Gamma ⊢\phi (t)}$$

For existential quantification:

$$\frac{\Gamma ⊢\phi (t)}{\Gamma ⊢\exists x.\phi (x)}\frac{\Gamma ⊢\exists x.\phi (x)\Delta ,\phi (x)⊢\psi }{\Gamma ,\Delta ⊢\psi }$$

provided $x$ does not occur free in $\Gamma$, $\Delta$, or $\psi$.

The classical version is obtained by adding specifically classical principles such as excluded middle.

Semantics

Classical first-order logic is usually interpreted by Tarski semantics relative to a structure $\mathcal{M}=(D,I)$.

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

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

\mathcal{M}, \sigma \vDash \forall x . \phi &\iff \text{for all } d \in D, \mathcal{M}, \sigma[x \mapsto d] \vDash \phi \\ \mathcal{M}, \sigma \vDash \exists x . \phi &\iff \text{there exists } d \in D \text{ such that } \mathcal{M}, \sigma[x \mapsto d] \vDash \phi \end{aligned}$$ Intuitionistic first-order logic is instead interpreted by semantics such as [[Kripke Semantics]] or algebraic semantics in [[Heyting Algebra|Heyting algebras]]. In a Heyting algebra, implication is characterized by $x \land a \leq b \iff x \leq (a \to b)$, and negation is the pseudo-complement $\neg a = (a \to 0)$. ## Intuitionistic First-Order Logic *Intuitionistic first-order logic* is the restriction of first-order logic to constructive rules. Under the Brouwer-Heyting-Kolmogorov interpretation, a proposition is true only when a proof or construction is given. The following principles are classically valid but not derivable intuitionistically in general: - [[Law of the Excluded Middle]]: $P \lor \neg P$ - [[Double Negation Elimination]]: $\neg \neg P \to P$ - Peirce's law: $((P \to Q) \to P) \to P$ - Drinker paradox: $\exists x (P(x) \to \forall y P(y))$ - One direction of De Morgan's law: $\neg(A \land B) \to \neg A \lor \neg B$ - Definability of $\exists$ from $\forall$: $\neg \forall x \neg P(x) \to \exists x P(x)$ Intuitionistic predicate logic also has structural features absent in the classical setting: - *Disjunction property*: if $\vdash \phi \lor \psi$ for a closed formula, then $\vdash \phi$ or $\vdash \psi$. - *Existence property*: if $\vdash \exists x . \phi(x)$, then there is a term $t$ such that $\vdash \phi(t)$. - The connectives remain independent: for example, $\exists$ is not interdefinable with $\forall$ by negation, and $\lor$ is not definable from $\land$, $\to$, and $\neg$. ## Metatheory For classical first-order logic, standard metatheorems include: - [[Soundness]] - [[Completeness (Logic)]] - [[Compactness]] - [[Löwenheim-Skolem]] - [[Gödel's incompleteness theorems]] - [[Undecidability]] of validity For intuitionistic first-order logic, one still has soundness and completeness with respect to [[Kripke Semantics]] in classical metatheory. Constructively, completeness for the intended semantics is not generally provable; results of Kreisel show that such completeness principles imply weak excluded-middle principles in the metatheory. Decidability also differs between fragments. Full first-order logic is undecidable in both settings, but some fragments behave differently; for example, monadic predicate logic is decidable classically but undecidable intuitionistically. ## Relation to Type Theory In the context of the [[Curry-Howard Correspondence]]: - Universal quantification $\forall x . P(x)$ corresponds to the [[dependent product]] type $(x : A) \to P(x)$. - Existential quantification $\exists x . P(x)$ corresponds to the [[dependent sum]] type $(x : A) \times P(x)$, or its propositional truncation in settings with proof relevance. - Predicates are modeled as [[Type Family|type families]] $P : A \to \mathcal{U}$. The Gödel-Gentzen double-negation translation embeds classical first-order logic into intuitionistic first-order logic. ## Related Concepts - [[Propositional Logic]] - [[Natural deduction]] - [[First-Order Structure]] - [[Tarski Semantics]] - [[Kripke Semantics]] - [[Heyting Algebra]] ## References [[dummett2000-intuitionism]] [[troelstra-schwichtenberg2000-basic-proof-theory]] [[vanDalen2013-logic-structure]]