Exists

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

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

Input: Exists(Equal(Exp(x), 2), ForElement(x, RR), GreaterEqual(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))))
$$\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))))
$$\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