Barber's Paradox (in Coq)

[Julio Di Egidio]

This is the Barber's Paradox in Coq, in fact, a couple of equivalent
takes on it.

I am taking it to be the prototypical example of a *false hypothesis*:
it does not have a "yes" answer, it does not have a "no" answer, at
best it has a "yes and no" answer!

I challenge you to make it even more concise (not necessarily in Coq).

```coq
(**
Barber's Paradox.

Proposition:
There is a barber who lives on an island.
The barber shaves all and only those men
on the island who do not shave themselves.
Question:
Does the barber shave himself?
Answer:
There is no such Barber!
*)

Module BarberParadox.

Parameter T : Set.

Parameter shaves : T -> T -> Prop.

Definition exists_barber : Prop :=
exists b : T,
forall x : T,
shaves b x <-> ~ shaves x x.

Theorem no_such_barber :
~ exists_barber.
Proof.
intros B.
unfold exists_barber in B.
destruct B as [b B].
destruct (B b) as [PN NP].
assert (N : ~ shaves b b).
{
intros P.
apply (PN P P).
}
assert (P : shaves b b).
{
apply (NP N).
}
apply (N P).
Qed.

End BarberParadox.

Module BarberParadox'.

Parameter T : Set.

Parameter shaves : T -> T -> Prop.

Definition the_barber (b : T) : Prop :=
forall x : T,
shaves b x <-> ~ shaves x x.

Theorem no_such_barber :
~ exists x : T,
the_barber x.
Proof.
intros [b B].
unfold the_barber in B.
destruct (B b) as [PN NP].
assert (N : ~ shaves b b).
{
intros P.
apply (PN P P).
}
assert (P : shaves b b).
{
apply (NP N).
}
apply (N P).
Qed.

End BarberParadox'.
```

(I am not a Coq expert and not even a mathematical logic expert.
Serious feedback welcome.)

Julio

[Dan Christensen]

On Wednesday, March 22, 2023 at 9:50:31 AM UTC-4, Julio Di Egidio wrote:
> This is the Barber's Paradox in Coq, in fact, a couple of equivalent
> takes on it.
>
> I am taking it to be the prototypical example of a *false hypothesis*:
> it does not have a "yes" answer, it does not have a "no" answer, at
> best it has a "yes and no" answer!
>
> I challenge you to make it even more concise (not necessarily in Coq).
>

[snip]

I have 2 versions of the Barber Paradox:

Version 1 (the "original"): The non-existence of the barber

Suppose we define the Shaves relation as follows where Shaves(barber,a) means the barber shaves a.

1. ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
Premise

Apply Universal Specifcation setting a=barber to obtain the contradiction...

2. Shaves(barber,barber) <=> ~Shaves(barber,barber)
U Spec, 1

We conclude that no such barber can exist.

3. ~EXIST(barber):ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
Conclusion, 1

Version 2: An upgraded set-theoretic version that times up some "loose ends." It that proves:

In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man.

http://www.dcproof.com/BP12.htm (100 lines)

Dan

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

[Julio Di Egidio]

On Wednesday, 22 March 2023 at 17:03:33 UTC+1, Dan Christensen wrote:
> On Wednesday, March 22, 2023 at 9:50:31 AM UTC-4, Julio Di Egidio wrote:
> > This is the Barber's Paradox in Coq, in fact, a couple of equivalent
> > takes on it.
> >
> > I am taking it to be the prototypical example of a *false hypothesis*:
> > it does not have a "yes" answer, it does not have a "no" answer, at
> > best it has a "yes and no" answer!
> >
> > I challenge you to make it even more concise (not necessarily in Coq).
> >
> [snip]
>
> I have 2 versions of the Barber Paradox:
>
> Version 1 (the "original"): The non-existence of the barber
>
> Suppose we define the Shaves relation as follows where Shaves(barber,a) means the barber shaves a.
>
> 1. ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
> Premise
>
> Apply Universal Specifcation setting a=barber to obtain the contradiction...
>
> 2. Shaves(barber,barber) <=> ~Shaves(barber,barber)
> U Spec, 1
>
> We conclude that no such barber can exist.
>
> 3. ~EXIST(barber):ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
> Conclusion, 1

That, if I am not missing anything, is equivalent to mine.
I am just showing the elementary steps explicitly, I could
have written "intros, destruct, tauto" and be done with it.

> Version 2: An upgraded set-theoretic version that times up some "loose ends." It that proves:
>
> In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man.
>
> http://www.dcproof.com/BP12.htm (100 lines)

Of course, this one is (neither to the point, IMO, nor)
apparently less concise, plus I immediately find two
applications of "Suppose to the contrary...", so it is
even less satisfactory re what we apparently can do.

That said, thanks for the feedback: I'll look into your
other post.

Julio

[Dan Christensen]

On Wednesday, March 22, 2023 at 12:30:09 PM UTC-4, Julio Di Egidio wrote:
> On Wednesday, 22 March 2023 at 17:03:33 UTC+1, Dan Christensen wrote:
> > On Wednesday, March 22, 2023 at 9:50:31 AM UTC-4, Julio Di Egidio wrote:
> > > This is the Barber's Paradox in Coq, in fact, a couple of equivalent
> > > takes on it.
> > >
> > > I am taking it to be the prototypical example of a *false hypothesis*:
> > > it does not have a "yes" answer, it does not have a "no" answer, at
> > > best it has a "yes and no" answer!
> > >
> > > I challenge you to make it even more concise (not necessarily in Coq).
> > >
> > [snip]
> >
> > I have 2 versions of the Barber Paradox:
> >
> > Version 1 (the "original"): The non-existence of the barber
> >
> > Suppose we define the Shaves relation as follows where Shaves(barber,a) means the barber shaves a.
> >
> > 1. ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
> > Premise
> >
> > Apply Universal Specifcation setting a=barber to obtain the contradiction...
> >
> > 2. Shaves(barber,barber) <=> ~Shaves(barber,barber)
> > U Spec, 1
> >
> > We conclude that no such barber can exist.
> >
> > 3. ~EXIST(barber):ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
> > Conclusion, 1

> That, if I am not missing anything, is equivalent to mine.

Yes.

> I am just showing the elementary steps explicitly, I could
> have written "intros, destruct, tauto" and be done with it.

> > Version 2: An upgraded set-theoretic version that times up some "loose ends." It that proves:
> >
> > In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man.
> >
> > http://www.dcproof.com/BP12.htm (100 lines)

> Of course, this one is (neither to the point, IMO, nor)
> apparently less concise, plus I immediately find two
> applications of "Suppose to the contrary...", so it is
> even less satisfactory re what we apparently can do.

Like I said, it ties up some "loose ends." It gives some important insight into the root of the "problem." It is not, as many claim, due to "self-reference." It turns out that the paradox can eliminated by simply relaxing the requirement that the barber be a man.

[Julio Di Egidio]

On Wednesday, 22 March 2023 at 18:43:37 UTC+1, Dan Christensen wrote:
> On Wednesday, March 22, 2023 at 12:30:09 PM UTC-4, Julio Di Egidio wrote:
> > On Wednesday, 22 March 2023 at 17:03:33 UTC+1, Dan Christensen wrote:

<snip>

> > > Version 2: An upgraded set-theoretic version that times up some "loose ends." It that proves:
> > >
> > > In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man.
> > >
> > > http://www.dcproof.com/BP12.htm (100 lines)
>
> > Of course, this one is (neither to the point, IMO, nor)
> > apparently less concise, plus I immediately find two
> > applications of "Suppose to the contrary...", so it is
> > even less satisfactory re what we apparently can do.
>
> Like I said, it ties up some "loose ends." It gives some
> important insight into the root of the "problem." It is not,
> as many claim, due to "self-reference."

What "loose ends" and what "problem" and who's ever
claimed this is due to self-reference?? Keep in mind we
both have it in three lines of FOL, mine is even provably
constructive, and the result is *totally unproblematic*.

> It turns out that the paradox can eliminated by simply
> relaxing the requirement that the barber be a man.

How if at all the statement you prove there is related
to the original one is the only remaining question there,
and one that, given the other shortcomings, I am not
really inclined to investigate.

Julio

[Dan Christensen]

On Wednesday, March 22, 2023 at 1:49:38 PM UTC-4, Julio Di Egidio wrote:
> On Wednesday, 22 March 2023 at 18:43:37 UTC+1, Dan Christensen wrote:
> > On Wednesday, March 22, 2023 at 12:30:09 PM UTC-4, Julio Di Egidio wrote:
> > > On Wednesday, 22 March 2023 at 17:03:33 UTC+1, Dan Christensen wrote:
> <snip>
> > > > Version 2: An upgraded set-theoretic version that times up some "loose ends." It that proves:
> > > >
> > > > In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves IF AND ONLY IF that barber is not a man.
> > > >
> > > > http://www.dcproof.com/BP12.htm (100 lines)
> >
> > > Of course, this one is (neither to the point, IMO, nor)
> > > apparently less concise, plus I immediately find two
> > > applications of "Suppose to the contrary...", so it is
> > > even less satisfactory re what we apparently can do.
> >
> > Like I said, it ties up some "loose ends." It gives some
> > important insight into the root of the "problem." It is not,
> > as many claim, due to "self-reference."

> What "loose ends" and what "problem"

Loose ends such the domain(s) of discussion: Is it the set of all villagers? Is it just the men in the village? Should we consider more than one domain within the village? etc.

> and who's ever
> claimed this is due to self-reference??

[snip]

See https://en.wikipedia.org/wiki/Barber_paradox

It begins, "This article is about a paradox of self-reference."

As you now know, this is NOT the case!

[Julio Di Egidio]

On Wednesday, 22 March 2023 at 19:41:02 UTC+1, Dan Christensen wrote:
> On Wednesday, March 22, 2023 at 1:49:38 PM UTC-4, Julio Di Egidio wrote:

<snip>

> > What "loose ends" and what "problem"
>
> Loose ends such the domain(s) of discussion:
> Is it the set of all villagers?
> Is it just the men in the village?
> Should we consider more than one domain within the village? etc.

Of course it is, what else?
Of course they are, who else (would shave)?
Of course not, why ever?

What is there is there and what is not there does not
count! (Note: not what is not there may be there...)

The issue you raise has more to do with how we
read, and even before that write, the informal part.
But of course "the village" stands for any one domain
of discourse, and "the man" and "whaat man shaves
what man" is any binary relation on the one domain,
and whether there are women or not in that village,
or cats, or what-not, is imply immaterial to the problem
and what the problem, together with its solution, is in
fact meant to exemplify.

> > and who's ever
> > claimed this is due to self-reference??
>

> See https://en.wikipedia.org/wiki/Barber_paradox
> It begins, "This article is about a paradox of self-reference."
> As you now know, this is NOT the case!

Now we do more than just know, now we have *evidence*
that it is so.

That said, that article starts with "The barber paradox is a
puzzle derived from Russell's paradox", and I should read
it before saying anything else...

Julio

[Dan Christensen]

On Wednesday, March 22, 2023 at 3:06:59 PM UTC-4, Julio Di Egidio wrote:
> On Wednesday, 22 March 2023 at 19:41:02 UTC+1, Dan Christensen wrote:
> > On Wednesday, March 22, 2023 at 1:49:38 PM UTC-4, Julio Di Egidio wrote:
> <snip>
> > > What "loose ends" and what "problem"
> >
> > Loose ends such the domain(s) of discussion:
> > Is it the set of all villagers?
> > Is it just the men in the village?
> > Should we consider more than one domain within the village? etc.

> Of course it is, what else?
> Of course they are, who else (would shave)?
> Of course not, why ever?
>

It is reasonable to consider the men to be a proper subset of the villagers. It is not a monastery.

> What is there is there and what is not there does not
> count! (Note: not what is not there may be there...)
>
> The issue you raise has more to do with how we
> read, and even before that write, the informal part.
> But of course "the village" stands for any one domain
> of discourse, and "the man" and "whaat man shaves
> what man" is any binary relation on the one domain,
> and whether there are women or not in that village,
> or cats, or what-not, is imply immaterial to the problem
> and what the problem, together with its solution, is in
> fact meant to exemplify.

[snip]

Again, if the barber is a female resident of the village, then it is possible that she could indeed shave those and only those men in the village who do not shave themselves, avoiding any contradictions. I find that interesting.

[Julio Di Egidio]

On Wednesday, 22 March 2023 at 21:14:53 UTC+1, Dan Christensen wrote:
> On Wednesday, March 22, 2023 at 3:06:59 PM UTC-4, Julio Di Egidio wrote:
> > On Wednesday, 22 March 2023 at 19:41:02 UTC+1, Dan Christensen wrote:
> > > On Wednesday, March 22, 2023 at 1:49:38 PM UTC-4, Julio Di Egidio wrote:
> > <snip>
> > > > What "loose ends" and what "problem"
> > >
> > > Loose ends such the domain(s) of discussion:
> > > Is it the set of all villagers?
> > > Is it just the men in the village?
> > > Should we consider more than one domain within the village? etc.
>
> > Of course it is, what else?
> > Of course they are, who else (would shave)?
> > Of course not, why ever?
>
> It is reasonable to consider the men to be a proper
> subset of the villagers. It is not a monastery.

The explicit rule is what I have written below, and it
is common practice since the dawn of logic proper
with Euclid. Indeed "reasonable" per se is irrelevant,
you are given a question and to that and only to that
you should be replying. Extending the domain of
discourse just because you read "man" is a mistake,
not a problem, and a misunderstanding, about what
doing it with logic is even about.

> > What is there is there and what is not there does not
> > count! (Note: not what is not there may be there...)

EOD.

Julio

[Mostowski Collapse]

Pitty Coq doesn't have a proof renderer. Some of these
Proof Assistants even cannot return proof terms, they
erase them. What you show is some proof script,

i.e. maybe tactics maybe instructions, submitted to
the proof assistant, so that it solves a given goal, maybe
does it is even able to present and ask for subgoals,

based on an intial goal. But where is the proof? Similar
problem in Isabelle/HOL btw. In as far DC Proof has a
clear advantage. Common proof display strategies include:
- Fitch style (for Natural Deduction)
- Tableaux (works also for Sequent Systems!)
- Hilbert style (for example Metamath)
- What else?

They don't use much space. A less optimal example is here:
- http://pravda.irisa.fr/naturaldeduction.html
- What else?

Is there no way to force Coq to show a proof?

[Dan Christensen]

In summary, if the barber is a female resident of the village, then it is possible that she could indeed shave those and only those men in the village who do not shave themselves, avoiding any contradictions.

By simply relaxing the requirement that the barber be a man, the contradiction vanishes. I find that to be an interesting insight. It is strange that you do not see it that way, Julio. Why is that?

[Julio Di Egidio]

Not before simply deleting the supposed rule and ignoring
any point of objection.

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

It seems Burse has not yet managed to prove your system
unsound, but your math blog I wouldn't recommend to my
worst enemy.

Have fun,

Julio

[Mostowski Collapse]

Currently I am building an alternative to DC Proof.
Step by step, it will be open source, unlike DC Proof,
and it will be more intelligent, nevertheless tactis

and stuff like Coq. But not like Coq, it will show
proofs. About Coq ability to show proofs. Is there
nothing around? Do not people use such tools and

then generate LaTeX from it, like here:

LaTeX macros for Fitch style natural deduction
https://www.mathstat.dal.ca/~selinger/fitch/

To post on sci.logic, you don't need LaTeX generation
rather ASCII. The same out that DC Poop can do.
I just generate HTML, and then use copy paste,

get rid of all the HTML dressing, and ASCII lands here.

[Mostowski Collapse]

Coq, Isabelle/HOL, etc.. all these tools that
cannot produce proof objects, will soon become
meme stocks, and disappear like Credit Suisse.

I mean to be fair and square, who wants to
use nonsense tools like Coq, Isabelle/HOL, etc...
in teaching or as a mathematician, if you

cannot communicate proofs? Only via their
idiosincratic instruction and tactic language.
Thats maybe something for unix freaks, that

are anyway use to bash all day in and out.

[Dan Christensen]

On Wednesday, March 22, 2023 at 5:07:59 PM UTC-4, Mostowski Collapse wrote:
> Currently I am building an alternative to DC Proof.

Good for you! Maybe will come to understand the real issues in the foundations of logic and mathematics.

> Step by step, it will be open source, unlike DC Proof,
> and it will be more intelligent, nevertheless tactis
>
> and stuff like Coq. But not like Coq, it will show
> proofs. About Coq ability to show proofs. Is there
> nothing around? Do not people use such tools and
>
> then generate LaTeX from it, like here:
>
> LaTeX macros for Fitch style natural deduction

Give some thought to alternatives to those silly lines. They don't work well for longer proofs. Also, you want to be able to insert comments on each line for readability. Give some thought to the use of different fonts and colors. Use sufficient white space.

> https://www.mathstat.dal.ca/~selinger/fitch/
>
> To post on sci.logic, you don't need LaTeX generation
> rather ASCII. The same out that DC Poop can do.
> I just generate HTML, and then use copy paste,
>

Good luck with that.

> get rid of all the HTML dressing, and ASCII lands here.

I found the parser, the line deletion function and the Conclusion Rule were the most complicated parts of DC Proof. Maybe some generic parsers are available now.

Decide who your audience is to be. If undergrads, don't think the usual notation used to define various axioms or rules of inference in philosophy books will work for them.

Review some of your old textbooks in real analysis, group theory or number theory. Reacquaint yourself with how mathematicians actually write proofs, especially how they make generalizations. Sorry, it won't be all standard FOL and ZFC set theory. I think you will find books on "mathematical logic" will be quite useless for your project. You will have to improvise A LOT. Your highest priority should be simplicity and ease of use. Beware of feature creep.

Have fun.

Dan

[Dan Christensen]

On Wednesday, March 22, 2023 at 5:37:28 PM UTC-4, Mostowski Collapse wrote:
> Coq, Isabelle/HOL, etc.. all these tools that
> cannot produce proof objects, will soon become
> meme stocks, and disappear like Credit Suisse.
>
> I mean to be fair and square, who wants to
> use nonsense tools like Coq, Isabelle/HOL, etc...
> in teaching or as a mathematician, if you
>
> cannot communicate proofs? Only via their
> idiosincratic instruction and tactic language.
> Thats maybe something for unix freaks, that
>
> are anyway use to bash all day in and out.

Well said!

Dan

[olcott]

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

I created Minimal Type Theory as very simple syntax that can represent
any order of logical expression by simply slightly augmenting FOL
syntax. I provide an example of encoding a second order logic expression
using this FOL syntax.

--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[Julio Di Egidio]

On Wednesday, 22 March 2023 at 20:06:59 UTC+1, Julio Di Egidio wrote:
> On Wednesday, 22 March 2023 at 19:41:02 UTC+1, Dan Christensen wrote:
> > On Wednesday, March 22, 2023 at 1:49:38 PM UTC-4, Julio Di Egidio wrote:
<snip>

> > > and who's ever
> > > claimed this is due to self-reference??
> >
> > See https://en.wikipedia.org/wiki/Barber_paradox
> > It begins, "This article is about a paradox of self-reference."
> > As you now know, this is NOT the case!
>
> Now we do more than just know, now we have *evidence*
> that it is so.
>
> That said, that article starts with "The barber paradox is a
> puzzle derived from Russell's paradox", and I should read
> it before saying anything else...

WP quotes Russell: << The question is, does the barber
shave himself? In this form the contradiction is not very
difficult to solve. But in our previous form I think it is clear
that you can only get around it by observing that the whole
question whether a class is or is not a member of itself
is nonsense, i.e. that no class either is or is not a member
of itself, and that it is not even true to say that, because
the whole form of words is just noise without meaning. >>

Unfortunately they don't say what the previous form is, but
immediately I notice at least two things: that *there exist
non-well-founded theories*, so apparently that argument is
false, indeed I'd say the two issues are rather orthogonal;
and that it is incorrect to call our proposition "meaningless",
since, to say that it does or does not denote, we must have
parsed its meaning: "arura notch ari moog" is meaningless,
"there exists (no) such thing" is either true or false, perhaps
identically so.

Julio

[Mostowski Collapse]

Dan Christensen schrieb am Donnerstag, 23. März 2023 um 04:28:56 UTC+1:
> > To post on sci.logic, you don't need LaTeX generation
> > rather ASCII. The same out that DC Poop can do.
> > I just generate HTML, and then use copy paste,
> Good luck with that.

What do you mean by good luck with that? Do you
have another function in DC Proof than Make HTML File?
The usual copy paste doesn't work. I cannot select

the proof and use some copy menu item, and would
get the proof as ASCII in a copy paste buffer. So one
has to proceed in DC proof:
- Make HTML File
- Open HTML File
- Do copy there

Or do you say there is another way in DC Poop?
Thats how posted on sci.logic for example:

EXIST(x):x=x => EXIST(x):[D(x) => ALL(y):D(y)]

------------------ begin proof ---------------------------------

1 EXIST(x):x=x
Premise

2 ~EXIST(x):[D(x) => ALL(y):D(y)]
Premise

3 ~~ALL(x):~[D(x) => ALL(y):D(y)]
Quant, 2

4 ALL(x):~[D(x) => ALL(y):D(y)]
Rem DNeg, 3

5 u=u
E Spec, 1

6 ~[D(u) => ALL(y):D(y)]
U Spec, 4

7 ~~[D(u) & ~ALL(y):D(y)]
Imply-And, 6

8 D(u) & ~ALL(y):D(y)
Rem DNeg, 7

9 D(u)
Split, 8

10 ~ALL(y):D(y)
Split, 8

11 ~~EXIST(y):~D(y)
Quant, 10

12 EXIST(y):~D(y)
Rem DNeg, 11

13 ~D(v)
E Spec, 12

14 ~[D(v) => ALL(y):D(y)]
U Spec, 4

15 ~~[D(v) & ~ALL(y):D(y)]
Imply-And, 14

16 D(v) & ~ALL(y):D(y)
Rem DNeg, 15

17 D(v)
Split, 16

18 ~ALL(y):D(y)
Split, 16

19 ~D(v) & D(v)
Join, 13, 17

20 ~~EXIST(x):[D(x) => ALL(y):D(y)]
Conclusion, 2

21 EXIST(x):[D(x) => ALL(y):D(y)]
Rem DNeg, 20

22 EXIST(x):x=x => EXIST(x):[D(x) => ALL(y):D(y)]
Conclusion, 1

------------------ end proof ---------------------------------

[Mostowski Collapse]

On Windows this function is broken:
- Select the Proof in the DC Proof window
- Use menu item "Copy Ctrl-C"
- Open NotePad
- Try to Paste, doesn't work.

Its pretty dead. DC Poop doesn't write
into the Windows Clipboard. Doesn't have Visual
Basic, or whatever you use for DC Poop, something like that:

https://learn.microsoft.com/en-us/windows/win32/api/winuser/nf-winuser-setclipboarddata

Anyway, it would be much better if you would
make DC Poop open source, so that people
could add missing functionality.

[Dan Christensen]

On Thursday, March 23, 2023 at 12:53:18 PM UTC-4, Mostowski Collapse wrote:
> On Windows this function is broken:
> - Select the Proof in the DC Proof window

On Edit menu, uncheck Rich Text Mode.

> - Use menu item "Copy Ctrl-C"
> - Open NotePad

Should then be able to paste to NotePad.

Dan