Drinkers Paradox (in DC Proof format)

[Dan Christensen]

THEOREM (The Drinkers' Paradox) ('@' = epsilon, '|' = OR-operator)

Let p be the set of people in a local pub. Let d be the set of drinkers. If p is non-empty, then there exist
someone in the pub who, if he is drinking, then so is everyone else in the pub.

ALL(p):ALL(d):[Set(p) & Set(d)
=> [EXIST(a):a @ p
=> EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]

This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com


PROOF

Prove: ALL(p):ALL(d):[Set(p) & Set(d)
=> [EXIST(a):a @ p
=> EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]

Suppose...

1 Set(p) & Set(d)
Premise

2 Set(p)
Split, 1

3 Set(d)
Split, 1


Prove: EXIST(a):a @ p
=> EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]

Suppose...

4 EXIST(a):a @ p
Premise

Two cases: Either everyone in the pub is drinking, or NOT everyone in the pub is drinking

5 ALL(b):[b @ p => b @ d] | ~ALL(b):[b @ p => b @ d]
Or Not


Case 1: Everyone in the pub is drinking

Prove: ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]

Suppose...

6 ALL(b):[b @ p => b @ d]
Premise

7 x @ p
E Spec, 4

8 ~x @ d | ALL(b):[b @ p => b @ d]
Arb Or, 6

9 x @ p & [~x @ d | ALL(b):[b @ p => b @ d]]
Join, 7, 8

Case 1

As Required:

10 ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]
Conclusion, 6


Case 2: NOT everyone in the pub is drinking

Prove: ~ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]

Suppose...

11 ~ALL(b):[b @ p => b @ d]
Premise

12 ~~EXIST(b):~[b @ p => b @ d]
Quant, 11

13 EXIST(b):~[b @ p => b @ d]
Rem DNeg, 12

14 EXIST(b):~~[b @ p & ~b @ d]
Imply-And, 13

15 EXIST(b):[b @ p & ~b @ d]
Rem DNeg, 14

16 y @ p & ~y @ d
E Spec, 15

17 y @ p
Split, 16

18 ~y @ d
Split, 16

19 ~y @ d | ALL(b):[b @ p => b @ d]
Arb Or, 18

20 y @ p & [~y @ d | ALL(b):[b @ p => b @ d]]
Join, 17, 19

Case 2

As Required:

21 ~ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]
Conclusion, 11

22 [ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]]
& [~ALL(b):[b @ p => b @ d]
=> EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]]
Join, 10, 21

23 EXIST(a):[a @ p & [~a @ d | ALL(b):[b @ p => b @ d]]]
Cases, 5, 22

24 EXIST(a):[a @ p & [~~a @ d => ALL(b):[b @ p => b @ d]]]
Imply-Or, 23

25 EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]
Rem DNeg, 24

As Required:

26 EXIST(a):a @ p
=> EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]
Conclusion, 4

As Required:

27 ALL(p):ALL(d):[Set(p) & Set(d)
=> [EXIST(a):a @ p
=> EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]
Conclusion, 1

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

[Dan Christensen]

On Saturday, May 24, 2014 2:17:46 PM UTC-4, Dan Christensen wrote:
> THEOREM (The Drinkers' Paradox) ('@' = epsilon, '|' = OR-operator)
>
>
>
> Let p be the set of people in a local pub. Let d be the set of drinkers. If p is non-empty, then there exist
>
> someone in the pub who, if he is drinking, then so is everyone else in the pub.
>
>
>
> ALL(p):ALL(d):[Set(p) & Set(d)
>
> => [EXIST(a):a @ p
>
> => EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]
>

I will try to give some of the intuition behind this seemingly counter-intuitive result.

With only one person in the pub, it all makes sense: If that one person is drinking, then, of course, everyone in the pub is drinking.

It gets a little more interesting with two people in the pub. It MIGHT be argued that if they simply took turns drinking over the TIME of an hour, then the theorem would be falsified. Neither one of them, it MIGHT be argued can be the person identified in the theorem whose drinking somehow CAUSES everyone else in the pub to drink.

In everyday usage (as often in science), the conditional "if" usually suggests causality between events over a period of time. We might say, after observing weather patterns over time that, if it is raining, then it is cloudy. We might theorize that the presence of clouds, among other conditions, CAUSES rain. And that clouds must be present at sometime time BEFORE it starts to rain.

In mathematics, however, there is no passage of time and no notion of cause-and-effect. In a mathematical analysis of above scenario, we don't talk about time and causality -- that would be the realm of science. Rather, we might look at what might be thought of as a collection of still photos (with no time stamps). We would have one or more photos of one of the two patrons drinking and the other not drinking, in no particular order. We would not be able to discern any causal relations or the passage of time from these photos alone. If we are going use the conditional "if" in describing them, it must be in a sense detached from notions of causality and time. In mathematics, the conditional "if" is exactly that.

In mathematics, the conditional "if X then Y" suggests no causality or ordering of events in time. It means precisely it must be false that both X is true and Y is false. Or equivalently (and more useful here), X is false OR Y is true.

In ANY collection of still photos of two people drinking (with no hint of causality or the passage of time), the Pub Theorem holds! Using the above logical equivalence, we can restate the theorem as follows:

Let p be the set of people in a local pub. Let d be the set of drinkers. If p is non-empty, then there exists X in the pub such that either X is not drinking OR everyone in the pub is drinking.

Consider two cases: Either (1) both are drinking or (2) it is false that both are drinking.

Case 1: Both are drinking. Then, clearly, there exists X in the pub (either one of the drinkers) such that either X is not drinking OR everyone in the pub is drinking. (The later being the case.)

Case 2: It is false that both are drinking. Again, there must exist X in the pub (either one of the patrons in question) such that either X is not drinking or everyone in the pub is drinking. (The former being the case.)

Thus the theorem holds in both cases.

To summarize: It might be argued, as above, that this result is ambiguous in "real time", but it is certainly true at any given instant in time.

[Dan Christensen]

On Saturday, May 24, 2014 2:17:46 PM UTC-4, Dan Christensen wrote:

> THEOREM (The Drinkers' Paradox) ('@' = epsilon, '|' = OR-operator)
>
>
>
> Let p be the set of people in a local pub. Let d be the set of drinkers. If p is non-empty, then there exist
>
> someone in the pub who, if he is drinking, then so is everyone else in the pub.
>

We could probably remove any paradoxical elements of this "theorem" by restating it slightly as (with change in caps):

Let p be the set of people in a local pub. Let d be the set of drinkers. If p is non-empty, then, AT ANY GIVEN INSTANT, there exists someone in the pub who, if he or she is drinking, then so is everyone else in the pub.

This would remove any temporal or causal aspects of this scenario, making it less of a philosophical conundrum, and more of a straightforward mathematical problem.

[Dan Christensen]

(Revised version. Recall that '@' = espilon, '|' = OR-operator)

THEOREM (The Drinkers Paradox)
*******

ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
=> EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]

In words: Suppose we have someone in a pub. Then, at any given instant, there exists someone in the pub who, if he drinks, then everyone else in the pub also drinks.

Note that there is no single individual that is the designated "leader of the drinkers" even briefly when everyone might happen to be drinking. Only one person (x) is designated as a patron in the pub.

There is no cause and effect here, no signal to suddenly start or stop drinking. We are simply considering all possibilities of who is drinking or not at any given instant in time.

The key to this proof is the use of the Arbitrary Antecedent and Arbitrary Consequent Rules.

The Arbitrary Antecedent Rule: Q --> P => Q for arbitrary P i.e. every thing implies a truth-hood

The Arbitrary Consequent Rule: P --> ~P => Q for arbitrary P i.e. every thing follows from a falsehood


(This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )


PROOF
*****

1 Set(pub) & Set(drinkers) & EXIST(c):c @ pub
Premise

Let pub be a set

2 Set(pub)
Split, 1

Let drinkers be a set

3 Set(drinkers)
Split, 1

pub is not empty

4 EXIST(c):c @ pub
Split, 1

Let x be any one of the patrons in the pub at an unspecified instant in time

5 x @ pub
E Spec, 4


Two cases to consider: At this instant in time, we have either

(1) every patron in the pub is drinking, or
(2) NOT every patron in the pub is drinking

6 ALL(d):[d @ pub => d @ drinkers] | ~ALL(d):[d @ pub => d @ drinkers]
Or Not


Case 1
******

Suppose all patrons are drinking at this instant in time

7 ALL(d):[d @ pub => d @ drinkers]
Premise


Apply Arbitrary Antecedent Rule: Q --> P => Q for arbitrary P

8 x @ drinkers => ALL(d):[d @ pub => d @ drinkers]
Arb Ante, 7

9 x @ pub
& [x @ drinkers => ALL(d):[d @ pub => d @ drinkers]]
Join, 5, 8

10 EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]
E Gen, 9

Case 1

As Required:

11 ALL(d):[d @ pub => d @ drinkers]
=> EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]
Conclusion, 7


Case 2
******

Suppose not all patrons are drinking at the moment

12 ~ALL(d):[d @ pub => d @ drinkers]
Premise

Change quantifier

13 ~~EXIST(d):~[d @ pub => d @ drinkers]
Quant, 12

14 EXIST(d):~[d @ pub => d @ drinkers]
Rem DNeg, 13

15 EXIST(d):~~[d @ pub & ~d @ drinkers]
Imply-And, 14

16 EXIST(d):[d @ pub & ~d @ drinkers]
Rem DNeg, 15

Let y be a patron in the pub that is NOT drinking at the moment

17 y @ pub & ~y @ drinkers
E Spec, 16

18 y @ pub
Split, 17

19 ~y @ drinkers
Split, 17


Apply Arbitrary Consequence Rule: P --> ~P => Q for arbitrary Q

20 ~~y @ drinkers => ALL(d):[d @ pub => d @ drinkers]
Arb Cons, 19

21 y @ drinkers => ALL(d):[d @ pub => d @ drinkers]
Rem DNeg, 20

22 y @ pub
& [y @ drinkers => ALL(d):[d @ pub => d @ drinkers]]
Join, 18, 21

23 EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]
E Gen, 22

Case 2

As Required:

24 ~ALL(d):[d @ pub => d @ drinkers]
=> EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]
Conclusion, 12

Join results from both cases

25 [ALL(d):[d @ pub => d @ drinkers]
=> EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]]
& [~ALL(d):[d @ pub => d @ drinkers]
=> EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]]
Join, 11, 24

In both cases, we have...

26 EXIST(c):[c @ pub
& [c @ drinkers => ALL(d):[d @ pub => d @ drinkers]]]
Cases, 6, 25

As Required:

27 ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
=> EXIST(c):[c @ a
& [c @ b => ALL(d):[d @ a => d @ b]]]]
Conclusion, 1

[Peter Percival]

Dan Christensen wrote:

>
> The Arbitrary Antecedent Rule: Q --> P => Q for arbitrary P i.e. every thing implies a truth-hood
>
> The Arbitrary Consequent Rule: P --> ~P => Q for arbitrary P i.e. every thing follows from a falsehood

Excuse me sir, why two kinds of arrow? These:

Q -> (P -> Q) , P -> (~P -> Q)

are tautologies, where -> is material implication (or the
truth-functional if-then). They are among a handful of formulae often
called the paradoxes of material implication. Is one of your arrows
material implication? If so, what's the other?

Also, I'm surprised that you have used no brackets. Do you have a
convention of associating to the right?

--
[...] They listened at his heart.
Little-less-nothing!-and that ended it.
No more to build on there. And they, since they
Were not the one dead, turned to their affairs.
"Out, Out-", Robert Frost, 1916.

[Peter Percival]

Dan Christensen wrote:
> (Revised version. Recall that '@' = espilon, '|' = OR-operator)
>
> THEOREM (The Drinkers Paradox)
> *******
>
> ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
> => EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]
>
> In words: Suppose we have someone in a pub. Then, at any given instant, there exists someone in the pub who, if he drinks, then everyone else in the pub also drinks.

I don't see what sets have got to do with it. A nice simple formal
statement is

(Ex)(D(x) -> (Ux)D(x)).

Two quantifiers! Why you have five, I don't know. I would prove (in an
informal sense) my version as follows. There are two cases:
(i) someone in the pub isn't drinking; or
(ii) everyone in the pub is drinking.
If "if someone in the pub is drinking then everyone in the pub is
drinking" can be shown to be true in both case (i) and case (ii) then we
are done (because (i) and (ii) exhaust the possibilities).
In case (i) choose a non-drinker, call him Jim, then

if Jim is drinking, everyone is drinking

is true because the antecedent is false. I.e., if J abbreviates "Jim is
drinking", and A abbreviates "everyone is drinking" we have

~J -> (J -> A)

a tautology. In case (ii)

if Jim is drinking, everyone is drinking

is true because the consequent is true. I.e. we have

A -> (J -> A)

a tautology.

[Dan Christensen]

On Thursday, May 29, 2014 11:11:48 AM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
>
>
>
> >
>
> > The Arbitrary Antecedent Rule: Q --> P => Q for arbitrary P i.e. every thing implies a truth-hood
>
> >
>
> > The Arbitrary Consequent Rule: P --> ~P => Q for arbitrary P i.e. every thing follows from a falsehood
>
>
>
> Excuse me sir, why two kinds of arrow? These:
>
>
>
> Q -> (P -> Q) , P -> (~P -> Q)
>
>
>
> are tautologies, where -> is material implication (or the
>
> truth-functional if-then). They are among a handful of formulae often
>
> called the paradoxes of material implication. Is one of your arrows
>
> material implication? If so, what's the other?
>

A => B means A implies B, the same conditional used in just about a every mathematics text book.

'-->' is used to describe a rule of inference. So, Q --> P => Q means that from Q, we can infer P => Q.

[Peter Percival]

Peter Percival wrote:
> Dan Christensen wrote:
>> (Revised version. Recall that '@' = espilon, '|' = OR-operator)
>>
>> THEOREM (The Drinkers Paradox)
>> *******
>>
>> ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
>> => EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]
>>
>> In words: Suppose we have someone in a pub. Then, at any given
>> instant, there exists someone in the pub who, if he drinks, then
>> everyone else in the pub also drinks.
>
> I don't see what sets have got to do with it. A nice simple formal
> statement is
>
> (Ex)(D(x) -> (Ux)D(x)).

You may prefer a new variable: (Ex)(D(x) -> (Uy)D(y)).

[Peter Percival]

Dan Christensen wrote:
> On Thursday, May 29, 2014 11:11:48 AM UTC-4, Peter Percival wrote:
>> Dan Christensen wrote:
>>
>>
>>
>>>
>>
>>> The Arbitrary Antecedent Rule: Q --> P => Q for arbitrary P i.e. every thing implies a truth-hood
>>
>>>
>>
>>> The Arbitrary Consequent Rule: P --> ~P => Q for arbitrary P i.e. every thing follows from a falsehood
>>
>>
>>
>> Excuse me sir, why two kinds of arrow? These:
>>
>>
>>
>> Q -> (P -> Q) , P -> (~P -> Q)
>>
>>
>>
>> are tautologies, where -> is material implication (or the
>>
>> truth-functional if-then). They are among a handful of formulae often
>>
>> called the paradoxes of material implication. Is one of your arrows
>>
>> material implication? If so, what's the other?
>>
>
> A => B means A implies B, the same conditional used in just about a every mathematics text book.
>
> '-->' is used to describe a rule of inference. So, Q --> P => Q means that from Q, we can infer P => Q.

Thank you.

[Dan Christensen]

On Thursday, May 29, 2014 11:31:38 AM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
>
> > (Revised version. Recall that '@' = espilon, '|' = OR-operator)
>
> >
>
> > THEOREM (The Drinkers Paradox)
>
> > *******
>
> >
>
> > ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
>
> > => EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]
>
> >
>
> > In words: Suppose we have someone in a pub. Then, at any given instant, there exists someone in the pub who, if he drinks, then everyone else in the pub also drinks.
>
>
>
> I don't see what sets have got to do with it. A nice simple formal
>
> statement is
>
>
>
> (Ex)(D(x) -> (Ux)D(x)).
>

You mean (Ex)(D(x) -> (Ax)D(x))?

I like to keep predicates to a minimum. I prefer to use set notation so that I can formally generalize over all sets at the end. I also like to make the domain of quantification explicit for every quantifier as is common practice in mathematics. With your version, we have the bizarre notation of everyone and everything in the universe being a drinker.

[Peter Percival]

Dan Christensen wrote:
> On Thursday, May 29, 2014 11:31:38 AM UTC-4, Peter Percival wrote:
>> Dan Christensen wrote:
>>
>>> (Revised version. Recall that '@' = espilon, '|' = OR-operator)
>>
>>>
>>
>>> THEOREM (The Drinkers Paradox)
>>
>>> *******
>>
>>>
>>
>>> ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
>>
>>> => EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]
>>
>>>
>>
>>> In words: Suppose we have someone in a pub. Then, at any given
>>> instant, there exists someone in the pub who, if he drinks, then
>>> everyone else in the pub also drinks.
>>
>>
>>
>> I don't see what sets have got to do with it. A nice simple
>> formal
>>
>> statement is
>>
>>
>>
>> (Ex)(D(x) -> (Ux)D(x)).
>>
>
> You mean (Ex)(D(x) -> (Ax)D(x))?

Yes. Hintikka uses E and U, and if they're good enough for him, they're
good enough for me! (But I sympathize, most people use A, don't they?)

>
> I like to keep predicates to a minimum.

There's just one: D, D(x) means "x drinks in the pub".

> I prefer to use set notation so that I can formally generalize over
> all sets at the end. I also like to make the domain of quantification
> explicit for every quantifier as is common practice in mathematics.
> With your version, we have the bizarre notation of everyone and
> everything in the universe being a drinker.

Since the paradox is about drinkers in a pub and naught else, taking the
domain of quantification to be the set of drinkers in the pub is
sensible. If you want an all-inclusive (whatever that may mean) domain
and relativized quantifiers, there still only needs to be two
quantifiers and now just two predicates, D as before and (let's say) X
with X(x) meaning "x is in the restricted domain X".

So (Ex in X)(...) becomes (Ex)(X(x) & ...) and
(Ux in X)(...) becomes (Ux)(X(x) -> ...) and my

(Ex)(D(x) -> (Uy)D(y)) [A 2nd post of mine considered this clearer
formally, it doesn't matter.]

becomes first

(Ex)(X(x) & (D(x) -> (Uy)D(y)))

and then

(Ex)(X(x) & (D(x) -> (Uy)(X(y) -> D(y)))).

Still only two quantifiers, and now just two predicates.

[Dan Christensen]

On Thursday, May 29, 2014 12:10:13 PM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
>
> > On Thursday, May 29, 2014 11:31:38 AM UTC-4, Peter Percival wrote:
>
> >> Dan Christensen wrote:
>
> >>
>
> >>> (Revised version. Recall that '@' = espilon, '|' = OR-operator)
>
> >>
>
> >>>
>
> >>
>
> >>> THEOREM (The Drinkers Paradox)
>
> >>
>
> >>> *******
>
> >>
>
> >>>
>
> >>
>
> >>> ALL(a):ALL(b):[Set(a) & Set(b) & EXIST(c):c @ a
>
> >>
>
> >>> => EXIST(c):[c @ a & c @ b => ALL(d):[d @ a => d @ b]]]
>
> >>
>
> >>>
>
> >>
>
> >>> In words: Suppose we have someone in a pub. Then, at any given
>
> >>> instant, there exists someone in the pub who, if he drinks, then
>
> >>> everyone else in the pub also drinks.
>
> >>
>
> >>
>
> >>
>
> >> I don't see what sets have got to do with it. A nice simple
>
> >> formal
>
> >>
>
> >> statement is
>
> >>
>
> >>
>
> >>
>
> >> (Ex)(D(x) -> (Ux)D(x)).
>
> >>
>
> >
>
> > You mean (Ex)(D(x) -> (Ax)D(x))?
>
>
>
> Yes. Hintikka uses E and U, and if they're good enough for him, they're
>
> good enough for me! (But I sympathize, most people use A, don't they?)
>
> >
>
> > I like to keep predicates to a minimum.
>
>
>
> There's just one: D, D(x) means "x drinks in the pub".

I have no predicates, but 2 sets:

pub = the set of patrons in the pub (the "universe" here)

drinkers = the set of drinkers.

>
> > I prefer to use set notation so that I can formally generalize over
>
> > all sets at the end. I also like to make the domain of quantification
>
> > explicit for every quantifier as is common practice in mathematics.
>
> > With your version, we have the bizarre notation of everyone and
>
> > everything in the universe being a drinker.
>
>
>
> Since the paradox is about drinkers in a pub and naught else, taking the
>
> domain of quantification to be the set of drinkers in the pub is
>
> sensible.

To be useful for other applications, your really need to generalize as much as you can.

> If you want an all-inclusive (whatever that may mean) domain
>
> and relativized quantifiers, there still only needs to be two
>
> quantifiers and now just two predicates, D as before and (let's say) X
>
> with X(x) meaning "x is in the restricted domain X".
>
>
>
> So (Ex in X)(...) becomes (Ex)(X(x) & ...) and
>
> (Ux in X)(...) becomes (Ux)(X(x) -> ...) and my
>

Yes, but then you couldn't formally generalize on the predicate X.

>
>
> (Ex)(D(x) -> (Uy)D(y)) [A 2nd post of mine considered this clearer
>
> formally, it doesn't matter.]
>
>
>
> becomes first
>
>
>
> (Ex)(X(x) & (D(x) -> (Uy)D(y)))
>
>
>
> and then
>
>
>
> (Ex)(X(x) & (D(x) -> (Uy)(X(y) -> D(y)))).
>
>
>
> Still only two quantifiers, and now just two predicates.
>

You are leaving out the fact that the pub (the "universe" here) is non-empty. That's one extra quantifier. Yes, I know that is always assumed by logicians, but not by mathematicians. They like to be more specific -- on this point anyway.

The other 2 additional quantifiers are to generalize the result for all sets -- something you cannot do for all predicates in FOL.

[Peter Percival]

Dan Christensen wrote:
> On Thursday, May 29, 2014 12:10:13 PM UTC-4, Peter Percival wrote:
>> Dan Christensen wrote:

>>> I like to keep predicates to a minimum.

>> There's just one: D, D(x) means "x drinks in the pub".
>
> I have no predicates, but 2 sets:
> pub = the set of patrons in the pub (the "universe" here)
> drinkers = the set of drinkers.
>

A (one place) predicate denotes a subset of the domain of
quantification, so there is no substantial difference between x in P and
P(x). If you have two sets then you do have two predicates.

[Dan Christensen]

On Thursday, May 29, 2014 1:33:08 PM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
>
> > On Thursday, May 29, 2014 12:10:13 PM UTC-4, Peter Percival wrote:
>
> >> Dan Christensen wrote:
>
>
>
> >>> I like to keep predicates to a minimum.
>
>
>
> >> There's just one: D, D(x) means "x drinks in the pub".
>
> >
>
> > I have no predicates, but 2 sets:
>
> > pub = the set of patrons in the pub (the "universe" here)
>
> > drinkers = the set of drinkers.
>
> >
>
>
>
> A (one place) predicate denotes a subset of the domain of
>
> quantification, so there is no substantial difference between x in P and
>
> P(x). If you have two sets then you do have two predicates.
>

But you can't formally generalize over predicates in FOL.

[Dan Christensen]

From my soon to be posted blog entry:

The Drinker's Theorem: If there is even one person in a pub, then there must exist a person there who, if he or she is drinking, then every one else there must also be drinking.

It doesn't matter how many are drinking or not drinking. There is no "lead drinker" influencing the others present. There is no need to assume any awareness among patrons of any other individuals in the pub. How is this possible? The key is a precise understanding of the logic "if".

Full text at: http://dcproof.com/DrinkersParadox.html

[George Greene]

On Thursday, May 29, 2014 11:45:59 AM UTC-4, Dan Christensen wrote:
> You mean (Ex)(D(x) -> (Ax)D(x))?

No, actually, we mean
Ex[ Dx --> Ax[Dx] ]
because spelling the quantifier (Qx) makes it look like the open parenthesis
has been CLOSED and that the statement is therefore OVER -- BUT IT'S NOT -- there's still A WHOLE 2nd HALF of it left -- THE BIGGER half, in fact.

>PP> (But I sympathize, most people use A, don't they?)
No, they don't. What ARE ACTUALLY used in that dialect are
A BACKWARDS E and an UPSIDE-DOWN A ; The E and A here are JUST LAME
ASCII APPROXIMATIONS.

> I like to keep predicates to a minimum.

You CAN'T do that HERE. And you ARE not doing it.
You are ADDING an UNnecessary (binary) predicate (epsilon)
to a context where only ONE predicate is needed.
Even more to the point, you haven't even understood what kind of
predicate it is: This is AN ARBITRARY unary first-order predicate.
This is actually *A*SECOND*ORDER* validity! It is not even a first-order
theorem at all! The actual theorem is
AD[ Ex[ Dx --> Ax[Dx] ] ]

When you prove the first-order instance, the fact that you are proving it
for a D that IS NOT MENTIONED ANYWHERE ELSE (in any other prior machinery)
means that you can invoke the inference rule of universal generalization ON THE *D*. So having proved your FIRST-order theorem with the unary D that you NECESSARILY HAD to add (since the theorem IS ABOUT *THAT* unary first-order predicate), you are, in fact, thereby proving a much more powerful SECOND order result -- having proved this first-order validity, all you have to do to make it 2nd-order just INCANT "2nd-order universal generalization".

Don't cheat yourself out of the most important part of the result.

I realize you are only writing a first-order prover, but the whole point is,
this first-order result IS THE LEMMA THAT ONE MUST PROVE AS A SUBGOAL in the
2nd-order proof. Since you are not writing a 2nd-order prover, you don't have
to actually BOTHER icing the cake or capping the stack. Or gilding the lily -- you can just leave the first-order result there for all to see, unvarnished as it were. Anybody with a brain will NOTICE that it generalizes to any D, that the "drinks" here is every bit as arbitrary as the "shaves" was in the binary case for Russell's Paradox.

The point is, the D is mandatory because that IS THE thing that is being universally generalized; that is THE thing that actually HAS the universal property being demonstrated here.

THE SETS ARE COMPLETELY irrelevant. ALL BINARY predicates (VERY much including epsilon) are COMPLETELY irrelevant to this. This is a 2nd-order result ABOUT UNARY 1st-order predicates in GENERAL -- about ALL of them. And it is, moreover, I repeat, THE OPPOSITE of a paradox (though of course every paradox is dual to this kind of validity; since a paradox has to be contradictory, you can ALWAYS assert THE DENIAL of the paradox as a theorem; in the case of Russell's Paradox, people have preferred to state the contradiction as a paradox, but in the case of this one, for some reason, people are preferring to state the validity/theorem; the denial doesn't sound all that paradoxical -- even though it is impossible -- because in natural language, the gloss on causality&implication will not match material implication.

Just for the record, the statement of the denial of Russell's Paradox as a 2nd-order theorem is usually attributed to Thomson;
Thomson, J. F., 1962, "On Some Paradoxes", in Analytical Philosophy, ed. R. J. Butler. New York: Barnes & Noble, pp. 104-119.
It would look something like
AR[~ Er[ Ax[xRr<-> ~xRx] ] ]
while Russell's Paradox itself would be
Er[ Ax[xRr<-> ~xRx] ] (this can't possibly ever be true because it
always necessarily comes up false when you instantiate x to r).

[Dan Christensen]

On Monday, June 2, 2014 6:32:06 PM UTC-4, George Greene wrote:

> > I like to keep predicates to a minimum.
>
>
>
> You CAN'T do that HERE.
> And you ARE not doing it.
>
> You are ADDING an UNnecessary (binary) predicate (epsilon)
>
> to a context where only ONE predicate is needed.
>

The nice thing about sets, is that, unlike predicates, you CAN generalize on them (existential or universal).

> Even more to the point, you haven't even understood what kind of
>
> predicate it is: This is AN ARBITRARY unary first-order predicate.
>

I understood that.

> This is actually *A*SECOND*ORDER* validity! It is not even a first-order
>
> theorem at all! The actual theorem is
>
> AD[ Ex[ Dx --> Ax[Dx] ] ]
>
>
>
> When you prove the first-order instance, the fact that you are proving it
>
> for a D that IS NOT MENTIONED ANYWHERE ELSE (in any other prior machinery)
>
> means that you can invoke the inference rule of universal generalization ON THE *D*. So having proved your FIRST-order theorem with the unary D that you NECESSARILY HAD to add (since the theorem IS ABOUT *THAT* unary first-order predicate), you are, in fact, thereby proving a much more powerful SECOND order result -- having proved this first-order validity, all you have to do to make it 2nd-order just INCANT "2nd-order universal generalization".
>
>
>
> Don't cheat yourself out of the most important part of the result.
>

[snip]

Thanks, George, but I think will stick to generalizing on free variables and sets. This is way too radical for me.

[Peter Percival]

Dan Christensen wrote:
> On Monday, June 2, 2014 6:32:06 PM UTC-4, George Greene wrote:
>
>>> I like to keep predicates to a minimum.
>>
>>
>>
>> You CAN'T do that HERE.
>> And you ARE not doing it.
>>
>> You are ADDING an UNnecessary (binary) predicate (epsilon)
>>
>> to a context where only ONE predicate is needed.
>>
>
> The nice thing about sets, is that, unlike predicates, you CAN generalize on them (existential or universal).

You've said that before, and it seems odd to me because one can prefix
predicate variables with $\forall$ and $\exist$. That is what happens
in second (and higher) order predicate calculus. You may not want to
because second and higher order predicate calculi are not effective and
complete (if sound).

--
Nam Nguyen in sci.logic in the thread 'Q on incompleteness proof'
on 16/07/2013 at 02:16: "there can be such a group where informally
it's impossible to know the truth value of the abelian expression
Axy[x + y = y + x]".

[Dan Christensen]

On Tuesday, June 3, 2014 8:27:20 AM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
>
> > On Monday, June 2, 2014 6:32:06 PM UTC-4, George Greene wrote:
>
> >
>
> >>> I like to keep predicates to a minimum.
>
> >>
>
> >>
>
> >>
>
> >> You CAN'T do that HERE.
>
> >> And you ARE not doing it.
>
> >>
>
> >> You are ADDING an UNnecessary (binary) predicate (epsilon)
>
> >>
>
> >> to a context where only ONE predicate is needed.
>
> >>
>
> >
>
> > The nice thing about sets, is that, unlike predicates, you CAN generalize on them (existential or universal).
>
>
>
> You've said that before, and it seems odd to me because one can prefix
>
> predicate variables with $\forall$ and $\exist$. That is what happens
>
> in second (and higher) order predicate calculus. You may not want to
>
> because second and higher order predicate calculi are not effective and
>
> complete (if sound).
>

Thanks, but, as seems to be the widespread convention in mathematics, I think I will continue to generalize only on free variables, functions and sets.

[Peter Percival]

Dan Christensen wrote:
> On Tuesday, June 3, 2014 8:27:20 AM UTC-4, Peter Percival wrote:
>> Dan Christensen wrote:

>>> The nice thing about sets, is that, unlike predicates, you CAN generalize on them (existential or universal).

>> You've said that before, and it seems odd to me because one can prefix
>> predicate variables with $\forall$ and $\exist$. That is what happens
>> in second (and higher) order predicate calculus. You may not want to
>> because second and higher order predicate calculi are not effective and
>> complete (if sound).

I meant "not effective or sound" (not that it matters).

> Thanks, but, as seems to be the widespread convention in mathematics, I think I will continue to generalize only on free variables, functions and sets.

Which is to say you use first order set theory (with urelemente such as
natural numbers)?

[Dan Christensen]

See my latest blog posting "The Drinker's Paradox" (dated today) at http://www.dcproof.wordpress.com

[George Greene]

On Thursday, May 29, 2014 1:33:08 PM UTC-4, Peter Percival wrote:
> A (one place) predicate denotes a subset of the domain of
>
> quantification, so there is no substantial difference between x in P and
>
> P(x).

This is absolutely 100% false.
NOT EVERY DEFINABLE PREDICATE CAN BE a set.
In particular, the predicate or unary-formula-schema
~(xex) (where x is the parameter) CANNOT become
{x:~xex}.
As soon as you invoke epsilon, you are DIALING DOWN from the class of "all possible predicates"( literally, all possible subcollections of the domain of discourse, WHICH IS *THE*SECOND*-order domain, if you include the UNdefinable subcollections as well) TO the class OF SETS.
You are invoking all the mystery of the set-class distinction AND of the question of JUST WHICH subcollections-of-the-domain (just WHICH fragments of the SECOND-order domain) YOU CAN CONSISTENTLY CRAM INTO the FIRST-order domain.
THAT IS A DEEP philosophical question (which "collections" can ALSO be "individuals"??) -- if you stay AT FIRST-order THEN IT CAN'T be "all" of them (but it can and must, at 2nd-order -- wherefore FIRST-order set-theory BECOMES ABOUT the question of shoehorning higher-orders INTO first-order in an appealling manner).

ALL THIS PHILOSOPHY *IS*NOT* something you NEED TO BOTHER With if you are just doing something as simple and tautological (valid, excuse me; tautology connotes propositional/0th-order) as the Drinks Theorem.

> If you have two sets then you do have two predicates.

But if there is no substantial difference then it must also conversely be the case that if you have (or need) two predicates, then you have (or CAN use) two sets. THIS IS *NOT* the case. You do NOT have two predicates OR two sets.
You have ONE predicate and NO sets. The pub IS THE DOMAIN OF DISCOURSE, is THE WHOLE universe, which is the quintessential/canonical example of something that IS NOT a set (because it is too big).
THE DOMAIN OF DISCOURSE *AND* the "Extensions" IN GENERAL of the DRINKS predicate D (THE ARBITRARY predicate in this example) ARE *CLASSES*, NOT sets!!

[Peter Percival]

George Greene wrote:
> On Thursday, May 29, 2014 1:33:08 PM UTC-4, Peter Percival wrote:
>> A (one place) predicate denotes a subset of the domain of
>>
>> quantification, so there is no substantial difference between x in
>> P and
>>
>> P(x).
>
> This is absolutely 100% false. NOT EVERY DEFINABLE PREDICATE CAN BE
> a set. In particular, the predicate or unary-formula-schema ~(xex)
> (where x is the parameter) CANNOT become {x:~xex}.

You are right. I should have said that to every set (or better, every
subclass of the domain of quantification) corresponds a predicate.

>
> [...] You

> do NOT have two predicates OR two sets. You have ONE predicate and NO
> sets. The pub IS THE DOMAIN OF DISCOURSE,

That is what I have been trying to tell Dan.