Epsilon Calculus

Origin. Hilbert, Bernays (1920s). Choice operator. Indefinite description. Quantifier elimination. Foundation of Hilbert's program.

Models. Epsilon terms for witnesses. Choice functions. Quantifier-free reasoning. Extended term language.

Formalism.

Epsilon term: εx.φ(x): "an x such that φ(x)." Indefinite description. Choice of witness. Term, not formula.

Critical axiom: φ(t) → φ(εx.φ(x)). If something satisfies φ, so does the epsilon term. Existence implies witness.

Quantifier definitions: ∃x.φ(x) := φ(εx.φ(x)). ∀x.φ(x) := φ(εx.¬φ(x)). Quantifiers via epsilon. Elimination possible.

Properties: εx.φ(x) always denotes (if domain nonempty). Even if nothing satisfies φ. Arbitrary choice then. Total function.

Extensionality (optional): ∀x(φ(x) ↔ ψ(x)) → εx.φ(x) = εx.ψ(x). Same predicate, same choice. Often not assumed.

First epsilon theorem: Provable in ε-calculus with quantifiers. Implies provable in ε-calculus with certain reductions. Quantifier-free core.

Second epsilon theorem: Herbrand's theorem connection. Witness extraction. Proof-theoretic content.

Relation to description: ιx.φ(x): definite description. εx.φ(x): indefinite. ι requires uniqueness. ε does not.

Symbols.

Metatheory. Choice operators. Quantifier elimination. Epsilon theorems. Herbrand connection.

Applies to. Proof theory. Hilbert's program. Witness extraction. Foundations.

Limitations. Non-constructive. Arbitrary choice. Extensionality issues. Complex metatheory.