How dumb is Dan Christensen aka Wonky Man?
He doesn't understand that what he describes works
also the other way around. Introducing empty domains

to FOL? Is Dan Christensen blind or is it simply
Alzheimer like Archimedes Plutonium has. Here is
how you introduce empty domains in FOL:

We don't need this, only do this if you want a non-empty domain:
> No, 1. The first line of your proof should introduce the axiom: EXIST(a):U(a)

But we do this:
> Yes, 2. Restrict every universal quantifier as follows: Aa(P(a)) ---> ALL(a):[U(a) => P(a)] (Note the '=>')
> Yes, 3. Restrict every existential quantifier as follows: Ea(P(a)) ---> EXIST(a):[U(a) & P(a)] (Note the '&')

To be ultra correct we also do:
> 4. If P(x) is some predicate, add the axiom: ALL(a):[P(a) => U(a)]

Here is the Drinker Paradox:

a) With implicit non-empty domain:
∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~7x%28Dx~5~6yDy%29

b) With explicit domain:
∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy))) is invalid.
https://www.umsu.de/trees/#~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29

c) With explicit non-empty domain:
∃tUt → (∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy)))) is valid.
https://www.umsu.de/trees/#~7tUt~5~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29

Easy, isn't it?

Dan Christensen schrieb am Mittwoch, 9. September 2020 um 18:55:17 UTC+2:
> I have noticed in various math forums that students have difficulties with quantifiers in proofs using standard first-order logic (FOL), difficulties that can often be cleared up by making explicit the implicit non-empty domain of discourse (universe) assumed for any given proof. According to FOL theory, in any given proof, this implicit "universe" may be the infinite set of all natural numbers, or just a dog and a cat. Of course, this is not formally stated in FOL proofs. By formally stating it in a DC Proof version, students may be able resolve their difficulties with proofs in standard FOL.
>
> In standard FOL, every formal proof has an implicit non-empty universe (or domain of discourse) that implicitly restricts all quantifiers in that proof. This non-emptiness manifests itself in the rule of Universal Specification (or Instantiation). If, for example, we are given a universal generalization Ax(P(x)) in FOL, then we can introduce a new free variable y such that P(y) and then conclude that Ex(P(x)). (See example below.)
>
> This is not usually the case in mathematical proofs where every quantifier is restricted to some, possibly empty, domain or set. In any given mathematical proof, there may be several different, possibly empty domains associated with different quantifiers. As in most mathematical proofs, this is also the case in my DC Proof system. It does not assume a priori the existence of any object(s), not even the empty set. Proofs of existence in DC Proof will require users to introduce at least one premise or axiom.
>
> If one is constrained to work in standard FOL for a proof (e.g. in a philosophy course), you may be able to simulate the above features of FOL using DC Proof by using the following workarounds:
>
> 1. The first line of your proof should introduce the axiom: EXIST(a):U(a)
>
> 2. Restrict every universal quantifier as follows:
>
> Aa(P(a)) ---> ALL(a):[U(a) => P(a)] (Note the '=>')
>
> 3. Restrict every existential quantifier as follows:
>
> Ea(P(a)) ---> EXIST(a):[U(a) & P(a)] (Note the '&')
>
> 4. Whenever given Aa(P(a)) in FOL and you want introduce a new free variable x by Universal Specification, you must first introduce the premise U(x), then you can apply the DC Proof rule of Universal Specification to the universal quantifier to obtain P(x). You will, of course, eventually have to discharge that premise by applying the DC Proof Conclusion Rule.
>
> 5. For every free variable x, we must have U(x).
>
>
> EXAMPLE FOL Proof of Ax(P(a)) => Ea(P(a)):
>
> 1. Aa(P(a)) (Assume)
> 2. P(x) (Universal Specification, 1)
> 3. Ex(P(a)) (Existential Generalization, 2)
> 4. Ax(P(a)) => Ea(P(a)) (Intro =>, 1, 2)
>
> Translates to DC Proof:
>
> 1 EXIST(a):U(a)
> Axiom
>
> 2 ALL(a):[U(a) => P(a)]
> Premise
>
> 3 U(x)
> E Spec, 1
>
> 4 U(x) => P(x)
> U Spec, 2
>
> 5 P(x)
> Detach, 4, 3
>
> 6 U(x) & P(x)
> Join, 3, 5
>
> 7 ALL(a):[U(a) => P(a)] => EXIST(a):[U(a) & P(a)]
> Conclusion, 2
>
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen aka Wonky Man halucinated:
> AFAICT in conventional mathematics, which has no such domain, you will probably need Russell'

I don't see any Russell here, both formulas deal
with empty domains, in both formulas the explicit
universe of discourse U(_) can be empty as FOL

does not pursue some existential import assumption
for its predicates. You are plain crazy wonky man
and a complete crank as usual:

b) With explicit domain:
∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy))) is invalid.
https://www.umsu.de/trees/#~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29

c) With explicit non-empty domain:
∃tUt → (∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy)))) is valid.
https://www.umsu.de/trees/#~7tUt~5~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29

Where do you see Russell? You are plain crazy and
a complete crank as usual. All that the Drinker Paradox
needs is a non-empty domain but not Russell. Bringing

the Russell to the Drinker is silly nonsense, see also:

Discussion
This proof illustrates several properties of classical predicate logic
which do not always agree with ordinary language.
Non-empty domain
Excluded middle
https://paradox.fandom.com/wiki/Drinker_paradox

Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 12:37:36 UTC+2:
> How dumb is Dan Christensen aka Wonky Man?
> He doesn't understand that what he describes works
> also the other way around. Introducing empty domains
>
> to FOL? Is Dan Christensen blind or is it simply
> Alzheimer like Archimedes Plutonium has. Here is
> how you introduce empty domains in FOL:
>
> We don't need this, only do this if you want a non-empty domain:
> > No, 1. The first line of your proof should introduce the axiom: EXIST(a):U(a)
>
> But we do this:
> > Yes, 2. Restrict every universal quantifier as follows: Aa(P(a)) ---> ALL(a):[U(a) => P(a)] (Note the '=>')
> > Yes, 3. Restrict every existential quantifier as follows: Ea(P(a)) ---> EXIST(a):[U(a) & P(a)] (Note the '&')
>
> To be ultra correct we also do:
> > 4. If P(x) is some predicate, add the axiom: ALL(a):[P(a) => U(a)]
>
> Here is the Drinker Paradox:
>
> a) With implicit non-empty domain:
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x%28Dx~5~6yDy%29
>
> b) With explicit domain:
> ∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy))) is invalid.
> https://www.umsu.de/trees/#~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29
>
> c) With explicit non-empty domain:
> ∃tUt → (∀z(Dz → Uz) → ∃x(Ux ∧ (Dx → ∀y(Uy → Dy)))) is valid.
> https://www.umsu.de/trees/#~7tUt~5~6z%28Dz~5Uz%29~5~7x%28Ux~1%28Dx~5~6y%28Uy~5Dy%29%29%29
>
> Easy, isn't it?
>
> Dan Christensen schrieb am Mittwoch, 9. September 2020 um 18:55:17 UTC+2:
> > I have noticed in various math forums that students have difficulties with quantifiers in proofs using standard first-order logic (FOL), difficulties that can often be cleared up by making explicit the implicit non-empty domain of discourse (universe) assumed for any given proof. According to FOL theory, in any given proof, this implicit "universe" may be the infinite set of all natural numbers, or just a dog and a cat. Of course, this is not formally stated in FOL proofs. By formally stating it in a DC Proof version, students may be able resolve their difficulties with proofs in standard FOL.
> >
> > In standard FOL, every formal proof has an implicit non-empty universe (or domain of discourse) that implicitly restricts all quantifiers in that proof. This non-emptiness manifests itself in the rule of Universal Specification (or Instantiation). If, for example, we are given a universal generalization Ax(P(x)) in FOL, then we can introduce a new free variable y such that P(y) and then conclude that Ex(P(x)). (See example below.)
> >
> > This is not usually the case in mathematical proofs where every quantifier is restricted to some, possibly empty, domain or set. In any given mathematical proof, there may be several different, possibly empty domains associated with different quantifiers. As in most mathematical proofs, this is also the case in my DC Proof system. It does not assume a priori the existence of any object(s), not even the empty set. Proofs of existence in DC Proof will require users to introduce at least one premise or axiom.
> >
> > If one is constrained to work in standard FOL for a proof (e.g. in a philosophy course), you may be able to simulate the above features of FOL using DC Proof by using the following workarounds:
> >
> > 1. The first line of your proof should introduce the axiom: EXIST(a):U(a)
> >
> > 2. Restrict every universal quantifier as follows:
> >
> > Aa(P(a)) ---> ALL(a):[U(a) => P(a)] (Note the '=>')
> >
> > 3. Restrict every existential quantifier as follows:
> >
> > Ea(P(a)) ---> EXIST(a):[U(a) & P(a)] (Note the '&')
> >
> > 4. Whenever given Aa(P(a)) in FOL and you want introduce a new free variable x by Universal Specification, you must first introduce the premise U(x), then you can apply the DC Proof rule of Universal Specification to the universal quantifier to obtain P(x). You will, of course, eventually have to discharge that premise by applying the DC Proof Conclusion Rule.
> >
> > 5. For every free variable x, we must have U(x).
> >
> >
> > EXAMPLE FOL Proof of Ax(P(a)) => Ea(P(a)):
> >
> > 1. Aa(P(a)) (Assume)
> > 2. P(x) (Universal Specification, 1)
> > 3. Ex(P(a)) (Existential Generalization, 2)
> > 4. Ax(P(a)) => Ea(P(a)) (Intro =>, 1, 2)
> >
> > Translates to DC Proof:
> >
> > 1 EXIST(a):U(a)
> > Axiom
> >
> > 2 ALL(a):[U(a) => P(a)]
> > Premise
> >
> > 3 U(x)
> > E Spec, 1
> >
> > 4 U(x) => P(x)
> > U Spec, 2
> >
> > 5 P(x)
> > Detach, 4, 3
> >
> > 6 U(x) & P(x)
> > Join, 3, 5
> >
> > 7 ALL(a):[U(a) => P(a)] => EXIST(a):[U(a) & P(a)]
> > Conclusion, 2
> >
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Quite intersting find. Since FOL has this theorem:
ALL(x):U(x) => EXIST(x):U(x)

We can switch off a possible empty domain as well with:
(Alternative) We don't need this, only do this if you want a non-empty domain:
> No, 1'. The first line of your proof should introduce the axiom: ALL(a):U(a)

The above works only in FOL. It would also make obsolete:
(Obsolete) To be ultra correct we also do:
> 4. If P(x) is some predicate, add the axiom: ALL(a):[P(a) => U(a)]

Example: The Drinker Paradox:
∀xPx → ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is valid.
https://www.umsu.de/trees/#~6xPx~5~7x%28Px~1%28Dx~5~6y%28Py~5Dy%29%29%29

Now the predicate P **is** the Domain of Discourse, since
we have ALL(a):P(a), and its also non-empty, since we use FOL.

A further find, this is also obsolete, because ALL(a):U(a) :

(Obsolete) But we do this:
> Yes, 2. Restrict every universal quantifier as follows: Aa(P(a)) ---> ALL(a):[U(a) => P(a)] (Note the '=>')
> Yes, 3. Restrict every existential quantifier as follows: Ea(P(a)) ---> EXIST(a):[U(a) & P(a)] (Note the '&')

So the Drinker Paradox is this one in FOL:

∀xPx → ∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~6xPx~5~7x%28Dx~5~6yDy%29

Looking at the proof it seems ∀xPx is not used, so we get also:

∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~7x%28Dx~5~6yDy%29

Mostowski Collapse schrieb am Mittwoch, 19. Oktober 2022 um 15:07:21 UTC+2:
> Quite intersting find. Since FOL has this theorem:
> ALL(x):U(x) => EXIST(x):U(x)
>
> We can switch off a possible empty domain as well with:
> (Alternative) We don't need this, only do this if you want a non-empty domain:
> > No, 1'. The first line of your proof should introduce the axiom: ALL(a):U(a)
>
> The above works only in FOL. It would also make obsolete:
> (Obsolete) To be ultra correct we also do:
> > 4. If P(x) is some predicate, add the axiom: ALL(a):[P(a) => U(a)]
> Example: The Drinker Paradox:
> ∀xPx → ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is valid.
> https://www.umsu.de/trees/#~6xPx~5~7x%28Px~1%28Dx~5~6y%28Py~5Dy%29%29%29
>
> Now the predicate P **is** the Domain of Discourse, since
> we have ALL(a):P(a), and its also non-empty, since we use FOL.