First-Order Logic

Propositional logic talks about facts. First-order logic (FOL) talks about objects, their properties, and their relations.

Syntax additions over propositional logic

• Constants: $\text{Socrates}, \text{Aristotle}$ — refer to specific objects.
• Variables: $x, y, z$ — range over objects.
• Predicates: $\text{Mortal}(x)$, $\text{Teaches}(x, y)$ — true/false depending on the object(s).
• Functions: $\text{FatherOf}(x)$ — return an object.
• Quantifiers: $\forall x$ (for all $x$), $\exists x$ (there exists $x$).

Famous example

$\forall x \, (\text{Man}(x) \to \text{Mortal}(x))$ $\text{Man}(\text{Socrates})$ $\therefore \text{Mortal}(\text{Socrates})$

Classical "Socrates is mortal" — a valid FOL inference.

Semantics

A model in FOL consists of a domain (set of objects) and interpretations of all constants, predicates, and functions over that domain. A sentence is true in the model if everything works out under that interpretation.

Inference rules

• Universal instantiation: from $\forall x \, P(x)$ infer $P(t)$ for any term $t$.
• Existential instantiation: from $\exists x \, P(x)$ infer $P(c)$ for a fresh constant $c$.
• Generalization: from $P(c)$ where $c$ is arbitrary, infer $\forall x \, P(x)$.
• Modus ponens: from $\alpha \to \beta$ and $\alpha$ infer $\beta$.

These plus resolution give you a complete proof system for FOL — anything true is provable.

Decidability

Propositional logic is decidable (SAT is hard but decidable). FOL is semi-decidable: if a sentence is valid, you'll eventually prove it; if it's not, the algorithm may run forever. This is the classical Church-Turing undecidability result for FOL.

What FOL can't do

• Quantify over predicates ("there's a property $P$ such that..."). Need second-order logic.
• Capture inductive reasoning naturally (Peano axioms for arithmetic require an infinite axiom schema).
• Talk about probability or fuzziness directly.

Modern uses

• Theorem proving (Lean, Coq) — though those use higher-order logic.
• Knowledge bases (Prolog, Datalog — restricted fragments).
• Description logics — fragments of FOL that are decidable and used in ontologies (OWL, used by Wikipedia/Wikidata).
• Verification of distributed protocols (TLA+ uses something close to first-order set theory).