Description: Show what implication
inside "there exists" really expands to (using
implication directly inside "there exists" is usually a
mistake).
Those inexperienced with formal notations of classical logic may use
expressions combining "there exists" with implication. That is
usually a
mistake, because as proven using imor 428, such an expression can be
rewritten using not with or - and that is often not what the
author
intended. New users of formal notation who use "there exists"
with an
implication should consider if they meant "and" instead of
"implies". A
stark example is shown in eximp-surprise2 42531. See also alimp-surprise 42526
and empty-surprise 42528. (Contributed by David A. Wheeler,
17-Oct-2018.) |