# 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 `x`

that satisfies _{0}`A(x`

.
_{0}) ↔ ∃(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