Epsilon Calculus

A formal logic term.

if and only if
for all
there exists

In classical logic, an ε-term ε(x) A(x) denotes some value x0 that satisfies A(x0) ↔ ∃(x) A(x).

Note that this is different from ∃ in that it answers a satisfactory object (a "witness") instead of just the boolean answer to the query.

In some constructive logic, the ε-term will converge to a witness if and only if a witness exists, and otherwise will diverge (fail to yield a value).

In a deep sense, ε is to ∃ what λ is to ∀.

To edit this page see HTML special characters and symbols.

This page is linked from: Lambda Calculus