"Why can't we use implication for the existential quantifier?" (From MSE)

[Dan Christensen]

(This is based on a posting yesterday at MSE: http://math.stackexchange.com/questions/1487910/why-cant-we-use-implication-for-the-existential-quantifier/1489952#1489952 )

Let A = the set of apples. Let D = the set of things that are delicious

Using a universal quantifier, we can say:

For all x, x in A implies x in D, i.e. all apples are delicious.

Using an existential quantifier, we can say:

There exists x such that x in A and x in D, i.e. some apples are delicious.

Essentially, the OP wanted to know why this could not also be written as an implication:

There exists x such that x in A IMPLIES x in D.

Equivalently, this could be written:

There exists x such that x not in A or x in D.

For a given x, either of the following possibilities would satisfy this condition:

1. x in A and x in D, i.e. some apples are delicious (as above)

2. x not in A and x in D, i.e. some non-apples are delicious

3. x not in A and x not D, i.e. some non-apples are not delicious

So, the implication allows for more possibilities than the conjunction.

Furthermore, the implication following the existential quantifier as here is a set-theoretic variation of the so-called Drinker's Paradox (see my blog). For ANY set A and ANY proposition P, we can prove using ordinary set theory and the rules of logic that:

There exists x such that x in A implies P. (Ex:[x in A => P])

So, to avoid confusion, we should probably try to avoid altogether such constructs in mathematics.


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Mostowski Collapse]

Now that you have this nifty theorem, for a domain of
discourse that potentially has also sets:

28 ALL(s):[Set(s) => EXIST(a):~a e s]
Rem DNeg, 27
http://www.dcproof.com/UniversalSet.htm

Can you also prove what Quine proves here:

212. ALL(y):EXIST(x):[x =\= y]
https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up

I mean if ~a e s, then s u {a} =\= s. But how would
we get rid of Set(s), so that we don't end up with

ALL(y):[Set(y) => ...]. Do we even have in DC Proof
~EXIST(x): [Set(x) & ~Set(x)] ? Would this help?

[Mostowski Collapse]

Why can Quine even prove it? Does he by chance assume
a non-empty universe? Although ALL(y):... would be automatically
true in a empty universe. And for a non-empty universe there is

only the struggle between sets and urelements. What does the
subset axiom do for an urelement? It could treat the urelement
like the empty set. Quine writes:

"With help of f210 and *202 it is now possible to prove a theorem
to the effect that, whatever y may be, there is something else.; in
other words, that there is more than one entity."

212. ALL(y):EXIST(x):[x =\= y]
https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up

But this is from his "new foundation" I guess. His 210 is already
a little alien, it has a) existence of the some universal set V,
and curiously this set has b) V e V. And his 202 is subset axiom,

but unrestricted, respectively restricted to V, also alien to normal
set theory. He also shows somewhere existence of empty set
Λ, written by a kind of greek big lambda, not sure whether his proof 212

amounts to showing V =\= Λ, at least this would also suffice. Right?

[Mostowski Collapse]

I think Dan could prove this here:

ALL(s):[Set(s) => ALL(y):EXIST(x):[~x=y]]

Because he can use Set(s) to construct the empty set. And he
can use Set(s) to construct s u {a} which will not be empty.
As soon as we have two elements the conclusion follows:

∃x∃y¬x=y → ∀x∃y¬x=y is valid.
https://www.umsu.de/trees/#~7x~7y%28~3x=y%29~5~6x~7y%28~3x=y%29

Funny theorem, which gives the impression of a movement
where a quantifier goes from ∃x to ∀x. But can we get rid
of the ALL(s):[Set(s) => ..] precondition? So as to arrive

at the same result as Quine. So Quine assumes a non-empty
domain of discourse, even more specifically he has EXIST(a):Set(a).
So where are the many text books that don't assume a non-empty

domain of discourse, I am still currious!