Existential Quantifier ∃

A formula that uses a existential quantifier expresses there exists a value with a particular property. For example, (E. x (= (* (2) x) (6))) means that there exists some number x for which (= (* (2) x) (6)). Existential quantifiers are part of predicate calculus.

Definition

The existential quantifier is defined using the universal quantifier as (<-> (E. x ph) (-. (A. x (-. ph)))) /edit/peano_new/predicate/predicate.gh/df-ex.