Epsilon CalculusA formal logic term.
|↔||if and only if|
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