Epsilon Calculus
A formal logic term.
| Legenda | |
|---|---|
| ε | epsilon |
| λ | lambda |
| ↔ | 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 ∀.
- The Stanford Encyclopedia of Philosophy's entry.
To edit this page see HTML special characters and symbols.
This page is linked from: Lambda Calculus