Grim reference (alpha)

Exists

Input: Exists(f(x), ForElement(x, S))
f(x)   for some x∈Sf(x) \;\text{ for some } x \in S

True if f(x)f(x) is true for some xx in SS, and false otherwise.

Input: Exists(Equal(Exp(x), 2), ForElement(x, RR), GreaterEqual(x, 0))
ex=2   for some x∈R with x≥0{e}^{x} = 2 \;\text{ for some } x \in \mathbb{R} \text{ with } x \ge 0

An example of a quantified formula.

Input: Equivalent(Exists(P(x), ForElement(x, S)), Element(True, Set(P(x), ForElement(x, S))))
(P(x)   for some x∈S)  ⟺  (True⁡∈{P(x):x∈S})\left(P(x) \;\text{ for some } x \in S\right) \iff \left(\operatorname{True} \in \left\{ P(x) : x \in S \right\}\right)

Equivalent characterization of this operator.

Input: Equivalent(Exists(P(x), ForElement(x, S), Q(x)), Element(True, Set(P(x), ForElement(x, S), Q(x))))
(P(x)   for some x∈S with Q(x))  ⟺  (True⁡∈{P(x):x∈S and⁡ Q(x)})\left(P(x) \;\text{ for some } x \in S \text{ with } Q(x)\right) \iff \left(\operatorname{True} \in \left\{ P(x) : x \in S \,\mathbin{\operatorname{and}}\, Q(x) \right\}\right)

Equivalent characterization of this operator.

Last updated: 2020-03-06 00:22:16