Relational Theory and the Russell Paradox
Quote from Erwin on December 21, 2019, 6:59 pmQuote from AntC on December 21, 2019, 11:22 amQuote from dandl on December 20, 2019, 12:36 amQuote from Hugh on December 19, 2019, 12:18 pmQuote from dandl on December 19, 2019, 12:27 amQuote from AntC on December 18, 2019, 9:57 amQuote from Erwin on December 15, 2019, 8:43 pmQuote from Dave Voorhis on December 12, 2019, 1:49 pmHere's my Tutorial D equivalent:
I remain puzzled why it takes so much code to tackle such a small problem, but may I suggest a slightly different approach.
There's many possible formulations (and it seems Russell himself airily dismissed the whole thing, so never gave any precise formulation). There's no need to follow wikipedia  and indeed their formulation adds unnecessary assumptions IMO. But I agree with your implication that Erwin's OP formulation adds rather more assumptions, along with relvars to hold their content.
From Wikipedia, the problem is this:
You can define the barber as "one who shaves all those, and those only, who do not shave themselves". The question is, does the barber shave himself?
"the barber" [definite singular] is going to be problematic, because it carries a presupposition of existence. I'll start in the plural at "barbers shave all and only those who do not shave themselves". That is "barbers if any ...".
There are no constraints other than valid keys.
Let's not assume we need keys. Let's not assume anybody shaves atall; nor if they do shave they always shave themselves or always go to the same barber.
So I won't have a relation PERSON. There might be in the domain of discourse women and/or men who grow beards. I'll have a relation SHAVES that talks only about those who do shave. Presumably the purpose of a BARBER relation is to identify those qualified to shave others  we don't want random strangers waving sharp implements about near people's faces. I'll merely require anybody who does shave others to themselves be shaven. (This'll provide mutual quality control amongst barbers; and avoid wriggling out via women barbers.)
I want to allow scenarios:
 Nobody shaves/gets shaved. The empty database, as allowed by OP.
 All who get shaved, shave themselves. As allowed by OP.
 People might both shave themselves sometimes and get shaved other times. (So a given shavee might have several entries in the SHAVES relation.)
 The same person might go to a variety of barbers. (So ditto.)
 Two barbers who shave each other. (At least, up to a guild of barbers mutually maintaining quality control.)
 Some barbers might have no customers.
And then later impose a constraint there is at most one barber. That is, of the last two barbers, one quits business.
Code to follow.
Thanks for spokesmanning me. I just want to point out that your point three eliminates the paradox. It allows "the" barber to shave himself.
Quote from AntC on December 21, 2019, 11:22 amQuote from dandl on December 20, 2019, 12:36 amQuote from Hugh on December 19, 2019, 12:18 pmQuote from dandl on December 19, 2019, 12:27 amQuote from AntC on December 18, 2019, 9:57 amQuote from Erwin on December 15, 2019, 8:43 pmQuote from Dave Voorhis on December 12, 2019, 1:49 pmHere's my Tutorial D equivalent:
I remain puzzled why it takes so much code to tackle such a small problem, but may I suggest a slightly different approach.
There's many possible formulations (and it seems Russell himself airily dismissed the whole thing, so never gave any precise formulation). There's no need to follow wikipedia  and indeed their formulation adds unnecessary assumptions IMO. But I agree with your implication that Erwin's OP formulation adds rather more assumptions, along with relvars to hold their content.
From Wikipedia, the problem is this:
You can define the barber as "one who shaves all those, and those only, who do not shave themselves". The question is, does the barber shave himself?
"the barber" [definite singular] is going to be problematic, because it carries a presupposition of existence. I'll start in the plural at "barbers shave all and only those who do not shave themselves". That is "barbers if any ...".
There are no constraints other than valid keys.
Let's not assume we need keys. Let's not assume anybody shaves atall; nor if they do shave they always shave themselves or always go to the same barber.
So I won't have a relation PERSON. There might be in the domain of discourse women and/or men who grow beards. I'll have a relation SHAVES that talks only about those who do shave. Presumably the purpose of a BARBER relation is to identify those qualified to shave others  we don't want random strangers waving sharp implements about near people's faces. I'll merely require anybody who does shave others to themselves be shaven. (This'll provide mutual quality control amongst barbers; and avoid wriggling out via women barbers.)
I want to allow scenarios:
 Nobody shaves/gets shaved. The empty database, as allowed by OP.
 All who get shaved, shave themselves. As allowed by OP.
 People might both shave themselves sometimes and get shaved other times. (So a given shavee might have several entries in the SHAVES relation.)
 The same person might go to a variety of barbers. (So ditto.)
 Two barbers who shave each other. (At least, up to a guild of barbers mutually maintaining quality control.)
 Some barbers might have no customers.
And then later impose a constraint there is at most one barber. That is, of the last two barbers, one quits business.
Code to follow.
Thanks for spokesmanning me. I just want to point out that your point three eliminates the paradox. It allows "the" barber to shave himself.
Quote from AntC on December 23, 2019, 12:42 amQuote from Erwin on December 21, 2019, 6:59 pmQuote from AntC on December 21, 2019, 11:22 amQuote from dandl on December 20, 2019, 12:36 amQuote from Hugh on December 19, 2019, 12:18 pmQuote from dandl on December 19, 2019, 12:27 amQuote from AntC on December 18, 2019, 9:57 amQuote from Erwin on December 15, 2019, 8:43 pmQuote from Dave Voorhis on December 12, 2019, 1:49 pmHere's my Tutorial D equivalent:
I remain puzzled why it takes so much code to tackle such a small problem, but may I suggest a slightly different approach.
There's many possible formulations (and it seems Russell himself airily dismissed the whole thing, so never gave any precise formulation). There's no need to follow wikipedia  and indeed their formulation adds unnecessary assumptions IMO. But I agree with your implication that Erwin's OP formulation adds rather more assumptions, along with relvars to hold their content.
From Wikipedia, the problem is this:
You can define the barber as "one who shaves all those, and those only, who do not shave themselves". The question is, does the barber shave himself?
"the barber" [definite singular] is going to be problematic, because it carries a presupposition of existence. I'll start in the plural at "barbers shave all and only those who do not shave themselves". That is "barbers if any ...".
There are no constraints other than valid keys.
Let's not assume we need keys. Let's not assume anybody shaves atall; nor if they do shave they always shave themselves or always go to the same barber.
So I won't have a relation PERSON. There might be in the domain of discourse women and/or men who grow beards. I'll have a relation SHAVES that talks only about those who do shave. Presumably the purpose of a BARBER relation is to identify those qualified to shave others  we don't want random strangers waving sharp implements about near people's faces. I'll merely require anybody who does shave others to themselves be shaven. (This'll provide mutual quality control amongst barbers; and avoid wriggling out via women barbers.)
I want to allow scenarios:
 Nobody shaves/gets shaved. The empty database, as allowed by OP.
 All who get shaved, shave themselves. As allowed by OP.
 People might both shave themselves sometimes and get shaved other times. (So a given shavee might have several entries in the SHAVES relation.)
 The same person might go to a variety of barbers. (So ditto.)
 Two barbers who shave each other. (At least, up to a guild of barbers mutually maintaining quality control.)
 Some barbers might have no customers.
And then later impose a constraint there is at most one barber. That is, of the last two barbers, one quits business.
Code to follow.
Thanks for spokesmanning me. I just want to point out that your point three eliminates the paradox. It allows "the" barber to shave himself.
Remember we're exploring the space. Also remember the Barber case is not a "paradox"  at least in one sense
2a: a statement that is seemingly contradictory or opposed to common sense and yet is perhaps trueb: a selfcontradictory statement that at first seems true[MerriamWebster]
The Barber case is not just 2a's "seemingly contradictory" but actually contradictory; the narrative is told in such an obfuscated way that it 2b's "at first seem true". (Older dictionaries I looked at didn't give the 2b sense; I wonder what sense was intended at the time it got called a paradox? Note Russell 1901 does not use "paradox" at all, but only "contradiction"; neither does he concede it "at first seems true".)
Also note Russell's is sometimes called an ''antinomy": Russell explained it as natural language befuddling us; using the same term in two incompatible senses. (But then the Logical Positivists were always fond of claiming ordinary mortals didn't understand language, and shouldn't be trusted with it.)
I see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
BTW, to explain why the "code to follow" hasn't yet followed (aside from the usual festive distractions) ... I'm using two tools
 The Prover when asked to prove no sole Barber could exist sometimes just barfs. This seems to be when the axioms are so tightly contradictory it doesn't get as far as inferring assertions about barbers.
 The Counterexample search when asked to find a sole Barber is supposed to stop/give up after a specified time. When the axioms are too tightly contradictory, it seems to get itself into a loop that doesn't come up for air to check if its time is exhausted.
Quote from Erwin on December 21, 2019, 6:59 pmQuote from AntC on December 21, 2019, 11:22 amQuote from dandl on December 20, 2019, 12:36 amQuote from Hugh on December 19, 2019, 12:18 pmQuote from dandl on December 19, 2019, 12:27 amQuote from AntC on December 18, 2019, 9:57 amQuote from Erwin on December 15, 2019, 8:43 pmQuote from Dave Voorhis on December 12, 2019, 1:49 pmHere's my Tutorial D equivalent:
I remain puzzled why it takes so much code to tackle such a small problem, but may I suggest a slightly different approach.
There's many possible formulations (and it seems Russell himself airily dismissed the whole thing, so never gave any precise formulation). There's no need to follow wikipedia  and indeed their formulation adds unnecessary assumptions IMO. But I agree with your implication that Erwin's OP formulation adds rather more assumptions, along with relvars to hold their content.
From Wikipedia, the problem is this:
You can define the barber as "one who shaves all those, and those only, who do not shave themselves". The question is, does the barber shave himself?
"the barber" [definite singular] is going to be problematic, because it carries a presupposition of existence. I'll start in the plural at "barbers shave all and only those who do not shave themselves". That is "barbers if any ...".
There are no constraints other than valid keys.
Let's not assume we need keys. Let's not assume anybody shaves atall; nor if they do shave they always shave themselves or always go to the same barber.
So I won't have a relation PERSON. There might be in the domain of discourse women and/or men who grow beards. I'll have a relation SHAVES that talks only about those who do shave. Presumably the purpose of a BARBER relation is to identify those qualified to shave others  we don't want random strangers waving sharp implements about near people's faces. I'll merely require anybody who does shave others to themselves be shaven. (This'll provide mutual quality control amongst barbers; and avoid wriggling out via women barbers.)
I want to allow scenarios:
 Nobody shaves/gets shaved. The empty database, as allowed by OP.
 All who get shaved, shave themselves. As allowed by OP.
 People might both shave themselves sometimes and get shaved other times. (So a given shavee might have several entries in the SHAVES relation.)
 The same person might go to a variety of barbers. (So ditto.)
 Two barbers who shave each other. (At least, up to a guild of barbers mutually maintaining quality control.)
 Some barbers might have no customers.
And then later impose a constraint there is at most one barber. That is, of the last two barbers, one quits business.
Code to follow.
Thanks for spokesmanning me. I just want to point out that your point three eliminates the paradox. It allows "the" barber to shave himself.
Remember we're exploring the space. Also remember the Barber case is not a "paradox"  at least in one sense
2a: a statement that is seemingly contradictory or opposed to common sense and yet is perhaps trueb: a selfcontradictory statement that at first seems true[MerriamWebster]
The Barber case is not just 2a's "seemingly contradictory" but actually contradictory; the narrative is told in such an obfuscated way that it 2b's "at first seem true". (Older dictionaries I looked at didn't give the 2b sense; I wonder what sense was intended at the time it got called a paradox? Note Russell 1901 does not use "paradox" at all, but only "contradiction"; neither does he concede it "at first seems true".)
Also note Russell's is sometimes called an ''antinomy": Russell explained it as natural language befuddling us; using the same term in two incompatible senses. (But then the Logical Positivists were always fond of claiming ordinary mortals didn't understand language, and shouldn't be trusted with it.)
I see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
BTW, to explain why the "code to follow" hasn't yet followed (aside from the usual festive distractions) ... I'm using two tools
 The Prover when asked to prove no sole Barber could exist sometimes just barfs. This seems to be when the axioms are so tightly contradictory it doesn't get as far as inferring assertions about barbers.
 The Counterexample search when asked to find a sole Barber is supposed to stop/give up after a specified time. When the axioms are too tightly contradictory, it seems to get itself into a loop that doesn't come up for air to check if its time is exhausted.
Quote from dandl on December 23, 2019, 1:34 amQuote from AntC on December 23, 2019, 12:42 amRemember we're exploring the space. Also remember the Barber case is not a "paradox"  at least in one sense
Exploring is good, but remember that:
 Russell himself stated the Barber problem in precisely the words quoted, before setting out to distinguish it from a 'real' paradox
 You added a spray of other dimensions to explore, but at some point you're going to have to pick your horse and back it with a problem stated as clearly stated as Russell's.
2a: a statement that is seemingly contradictory or opposed to common sense and yet is perhaps trueb: a selfcontradictory statement that at first seems true[MerriamWebster]
The Barber case is not just 2a's "seemingly contradictory" but actually contradictory; the narrative is told in such an obfuscated way that it 2b's "at first seem true". (Older dictionaries I looked at didn't give the 2b sense; I wonder what sense was intended at the time it got called a paradox? Note Russell 1901 does not use "paradox" at all, but only "contradiction"; neither does he concede it "at first seems true".)
I disagree. The Barber case presents no great difficulty, as Russell himself said. It simply is not a paradox at all.
Also note Russell's is sometimes called an ''antinomy": Russell explained it as natural language befuddling us; using the same term in two incompatible senses. (But then the Logical Positivists were always fond of claiming ordinary mortals didn't understand language, and shouldn't be trusted with it.)
I see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
So this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
Quote from AntC on December 23, 2019, 12:42 am
Remember we're exploring the space. Also remember the Barber case is not a "paradox"  at least in one sense
Exploring is good, but remember that:
 Russell himself stated the Barber problem in precisely the words quoted, before setting out to distinguish it from a 'real' paradox
 You added a spray of other dimensions to explore, but at some point you're going to have to pick your horse and back it with a problem stated as clearly stated as Russell's.
2a: a statement that is seemingly contradictory or opposed to common sense and yet is perhaps trueb: a selfcontradictory statement that at first seems true[MerriamWebster]
The Barber case is not just 2a's "seemingly contradictory" but actually contradictory; the narrative is told in such an obfuscated way that it 2b's "at first seem true". (Older dictionaries I looked at didn't give the 2b sense; I wonder what sense was intended at the time it got called a paradox? Note Russell 1901 does not use "paradox" at all, but only "contradiction"; neither does he concede it "at first seems true".)
I disagree. The Barber case presents no great difficulty, as Russell himself said. It simply is not a paradox at all.
Also note Russell's is sometimes called an ''antinomy": Russell explained it as natural language befuddling us; using the same term in two incompatible senses. (But then the Logical Positivists were always fond of claiming ordinary mortals didn't understand language, and shouldn't be trusted with it.)
I see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
So this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
Quote from AntC on December 25, 2019, 10:41 amQuote from dandl on December 23, 2019, 1:34 amQuote from AntC on December 23, 2019, 12:42 amI see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
So this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
% BarbarMin: Barber 'paradox' with minimum assumptions, and a single base relation % [quote from Russell 1901] 'You can define the barber as % "one who shaves all those, and those only, who do not shave themselves".' % but problematic to use "the"/"one" singular. % prefer a more general definition that allows more than one barber. % "Barbers shave all those, and those only, who do not shave themselves." % Furthermore split into two axioms: "shave all those" C12; "shave those only" C14. % shaves(x, y) ==> "x shaves y". % barber(x) ==> "x is a barber" virtual: "x shaves any who don't shave themselves". (shaves(x, y) & x != y) > barber(x). % C12 "barbers shave all those who do not shave themselves".". barber(x) > (shaves(x, y) > x != y). % C14 "barbers shave only those who don't ditto". barber(x) > (exists z shaves(z, x)). % C13 "barbers must be shaved". % C12, C13, C14 without C15 below have models: % * nobody atall shaves/shaved (empty database per OP) % * all who shave are selfshavers; disproves shaves(x, y). % * the population is two barbers, who shave each other; disproves shaves(x, y) > x = y. % * the population is three: one shelfshaver, two mutuallyshaving barbers. % * the population is three: one nonbarber shaved by a barber, two mutuallyshaving barbers. % * the population is three: one nonbarber sometimes shaves self, sometimes shaved by a barber, % two mutuallyshaving barbers; disproves (exists y (shaves(y,y) & (exists x (x != y & shaves(x, y))))). barber(x) > (all z (barber(z) <> x = z)). % C15 at most one barber. % goal (exists x barber(x)). % "there are no barbers" without C15 has countermodel. % with C15 proven (and the proof uses all of C12  C15).)Yes providing there's at least two barbers, we have valid scenarios where barbers shave each other but not themselves. (As opposed to the population at large who might not shave, or might selfshave only, or might visit multiple barbers, or might both selfshave and visit multiple barbers.)
When the penultimate barber retires  i.e. axiom C15 is added  the engine proves there can be no barbers at all. (The remaining person who used to be a barber might take to shaving themselves; but since it's only themselves they shave, they have ceased to be a barber.)
The only one of my objectives I didn't meet was
Some barbers might have no customers.
that's because I define barber as anyone who shaves another. You could have
barber(x)
be a base relation instead of a virtual: "x is a member of the guild of barbers".Note the effect of axioms C12, C14 together is that no barbers can selfshave. (C13 merely requires barbers to get shaved somehow.) So the contradiction is already lurking before we cut down to the last barber cutting.
Quote from dandl on December 23, 2019, 1:34 amQuote from AntC on December 23, 2019, 12:42 am
I see no elimination of the paradox by allowing people to be sometimes selfshaving, sometimes shaved possibly by different barbers at different times. Your OP showed that selfshavers must be allowed but aren't critical to causing the contradiction. All I'm going to require is that on occasions of nonselfshaving, the shaver must be a barber. Furthermore that all barbers must get shaved. If to arrive at the contradiction we further require barbers be sometimes shaved by a different barber (but sometimes can be selfshaving), we still have a valid scenario. It's only at the nexttolast barber quitting business that gives a contradiction.
So this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
% BarbarMin: Barber 'paradox' with minimum assumptions, and a single base relation % [quote from Russell 1901] 'You can define the barber as % "one who shaves all those, and those only, who do not shave themselves".' % but problematic to use "the"/"one" singular. % prefer a more general definition that allows more than one barber. % "Barbers shave all those, and those only, who do not shave themselves." % Furthermore split into two axioms: "shave all those" C12; "shave those only" C14. % shaves(x, y) ==> "x shaves y". % barber(x) ==> "x is a barber" virtual: "x shaves any who don't shave themselves". (shaves(x, y) & x != y) > barber(x). % C12 "barbers shave all those who do not shave themselves".". barber(x) > (shaves(x, y) > x != y). % C14 "barbers shave only those who don't ditto". barber(x) > (exists z shaves(z, x)). % C13 "barbers must be shaved". % C12, C13, C14 without C15 below have models: % * nobody atall shaves/shaved (empty database per OP) % * all who shave are selfshavers; disproves shaves(x, y). % * the population is two barbers, who shave each other; disproves shaves(x, y) > x = y. % * the population is three: one shelfshaver, two mutuallyshaving barbers. % * the population is three: one nonbarber shaved by a barber, two mutuallyshaving barbers. % * the population is three: one nonbarber sometimes shaves self, sometimes shaved by a barber, % two mutuallyshaving barbers; disproves (exists y (shaves(y,y) & (exists x (x != y & shaves(x, y))))). barber(x) > (all z (barber(z) <> x = z)). % C15 at most one barber. % goal (exists x barber(x)). % "there are no barbers" without C15 has countermodel. % with C15 proven (and the proof uses all of C12  C15).)
Yes providing there's at least two barbers, we have valid scenarios where barbers shave each other but not themselves. (As opposed to the population at large who might not shave, or might selfshave only, or might visit multiple barbers, or might both selfshave and visit multiple barbers.)
When the penultimate barber retires  i.e. axiom C15 is added  the engine proves there can be no barbers at all. (The remaining person who used to be a barber might take to shaving themselves; but since it's only themselves they shave, they have ceased to be a barber.)
The only one of my objectives I didn't meet was

Some barbers might have no customers.
that's because I define barber as anyone who shaves another. You could have barber(x)
be a base relation instead of a virtual: "x is a member of the guild of barbers".
Note the effect of axioms C12, C14 together is that no barbers can selfshave. (C13 merely requires barbers to get shaved somehow.) So the contradiction is already lurking before we cut down to the last barber cutting.
Quote from Dave Voorhis on December 25, 2019, 12:34 pmIt occurred to me that this is exactly the sort of thing Prologophiles (Prologistas?) probably waste time on. Sure enough, it appears as an example in something rather definitively named "Prolog: The Standard", thusly:
shave(barber,X) : \+ shave(X,X).Evaluating...
shave(barber, 'Dave')...or "Does the barber shave Dave?" returns true.
Evaluating...
shave(barber, barber)...or "Does the barber shave the barber?" returns:
Stack limit (0.2Gb) exceeded Stack sizes: local: 0.2Gb, global: 13Kb, trail: 2Kb Stack depth: 1,562,047, lastcall: 0%, Choice points: 1,562,027 Probable infinite recursion (cycle): [1,562,047] shave(barber, barber) [1,562,046] shave(barber, barber)I used the online SWIProlog implementation at https://swish.swiprolog.org
It occurred to me that this is exactly the sort of thing Prologophiles (Prologistas?) probably waste time on. Sure enough, it appears as an example in something rather definitively named "Prolog: The Standard", thusly:
shave(barber,X) : \+ shave(X,X).
Evaluating...
shave(barber, 'Dave')
...or "Does the barber shave Dave?" returns true.
Evaluating...
shave(barber, barber)
...or "Does the barber shave the barber?" returns:
Stack limit (0.2Gb) exceeded Stack sizes: local: 0.2Gb, global: 13Kb, trail: 2Kb Stack depth: 1,562,047, lastcall: 0%, Choice points: 1,562,027 Probable infinite recursion (cycle): [1,562,047] shave(barber, barber) [1,562,046] shave(barber, barber)
I used the online SWIProlog implementation at https://swish.swiprolog.org
Quote from dandl on December 25, 2019, 1:13 pmQuote from AntC on December 25, 2019, 10:41 amSo this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
% BarbarMin: Barber 'paradox' with minimum assumptions, and a single base relation % [quote from Russell 1901] 'You can define the barber as % "one who shaves all those, and those only, who do not shave themselves".' % but problematic to use "the"/"one" singular. % prefer a more general definition that allows more than one barber. % "Barbers shave all those, and those only, who do not shave themselves." % Furthermore split into two axioms: "shave all those" C12; "shave those only" C14. % shaves(x, y) ==> "x shaves y". % barber(x) ==> "x is a barber" virtual: "x shaves any who don't shave themselves". (shaves(x, y) & x != y) > barber(x). % C12 "barbers shave all those who do not shave themselves".". barber(x) > (shaves(x, y) > x != y). % C14 "barbers shave only those who don't ditto". barber(x) > (exists z shaves(z, x)). % C13 "barbers must be shaved". % C12, C13, C14 without C15 below have models: % * nobody atall shaves/shaved (empty database per OP) % * all who shave are selfshavers; disproves shaves(x, y). % * the population is two barbers, who shave each other; disproves shaves(x, y) > x = y. % * the population is three: one shelfshaver, two mutuallyshaving barbers. % * the population is three: one nonbarber shaved by a barber, two mutuallyshaving barbers. % * the population is three: one nonbarber sometimes shaves self, sometimes shaved by a barber, % two mutuallyshaving barbers; disproves (exists y (shaves(y,y) & (exists x (x != y & shaves(x, y))))). barber(x) > (all z (barber(z) <> x = z)). % C15 at most one barber. % goal (exists x barber(x)). % "there are no barbers" without C15 has countermodel. % with C15 proven (and the proof uses all of C12  C15).)Yes providing there's at least two barbers, we have valid scenarios where barbers shave each other but not themselves. (As opposed to the population at large who might not shave, or might selfshave only, or might visit multiple barbers, or might both selfshave and visit multiple barbers.)
Makes sense. In RM terms, you can construct populations as per your examples and query for barbers(s), and each query will return 2 barbers.
When the penultimate barber retires  i.e. axiom C15 is added  the engine proves there can be no barbers at all. (The remaining person who used to be a barber might take to shaving themselves; but since it's only themselves they shave, they have ceased to be a barber.)
Yup. Remove a single barber and the other disappears too, the query now finds none. No paradox, but the poor grunt who did nothing wrong except lose a competitor, just lost his barber status.
The only one of my objectives I didn't meet was
Some barbers might have no customers.
that's because I define barber as anyone who shaves another. You could have
barber(x)
be a base relation instead of a virtual: "x is a member of the guild of barbers".That would be a different problem statement.
Note the effect of axioms C12, C14 together is that no barbers can selfshave. (C13 merely requires barbers to get shaved somehow.) So the contradiction is already lurking before we cut down to the last barber cutting.
Quote from AntC on December 25, 2019, 10:41 amSo this is your restatement of the problem to consider? I get the sense that you hope to construct a set of rules that allow multiple barbers, but trigger a paradoxic when the penultimate barber retires. I'm not sure you're there yet.
% BarbarMin: Barber 'paradox' with minimum assumptions, and a single base relation % [quote from Russell 1901] 'You can define the barber as % "one who shaves all those, and those only, who do not shave themselves".' % but problematic to use "the"/"one" singular. % prefer a more general definition that allows more than one barber. % "Barbers shave all those, and those only, who do not shave themselves." % Furthermore split into two axioms: "shave all those" C12; "shave those only" C14. % shaves(x, y) ==> "x shaves y". % barber(x) ==> "x is a barber" virtual: "x shaves any who don't shave themselves". (shaves(x, y) & x != y) > barber(x). % C12 "barbers shave all those who do not shave themselves".". barber(x) > (shaves(x, y) > x != y). % C14 "barbers shave only those who don't ditto". barber(x) > (exists z shaves(z, x)). % C13 "barbers must be shaved". % C12, C13, C14 without C15 below have models: % * nobody atall shaves/shaved (empty database per OP) % * all who shave are selfshavers; disproves shaves(x, y). % * the population is two barbers, who shave each other; disproves shaves(x, y) > x = y. % * the population is three: one shelfshaver, two mutuallyshaving barbers. % * the population is three: one nonbarber shaved by a barber, two mutuallyshaving barbers. % * the population is three: one nonbarber sometimes shaves self, sometimes shaved by a barber, % two mutuallyshaving barbers; disproves (exists y (shaves(y,y) & (exists x (x != y & shaves(x, y))))). barber(x) > (all z (barber(z) <> x = z)). % C15 at most one barber. % goal (exists x barber(x)). % "there are no barbers" without C15 has countermodel. % with C15 proven (and the proof uses all of C12  C15).)Yes providing there's at least two barbers, we have valid scenarios where barbers shave each other but not themselves. (As opposed to the population at large who might not shave, or might selfshave only, or might visit multiple barbers, or might both selfshave and visit multiple barbers.)
Makes sense. In RM terms, you can construct populations as per your examples and query for barbers(s), and each query will return 2 barbers.
When the penultimate barber retires  i.e. axiom C15 is added  the engine proves there can be no barbers at all. (The remaining person who used to be a barber might take to shaving themselves; but since it's only themselves they shave, they have ceased to be a barber.)
Yup. Remove a single barber and the other disappears too, the query now finds none. No paradox, but the poor grunt who did nothing wrong except lose a competitor, just lost his barber status.
The only one of my objectives I didn't meet was
Some barbers might have no customers.
that's because I define barber as anyone who shaves another. You could have
barber(x)
be a base relation instead of a virtual: "x is a member of the guild of barbers".
That would be a different problem statement.
Note the effect of axioms C12, C14 together is that no barbers can selfshave. (C13 merely requires barbers to get shaved somehow.) So the contradiction is already lurking before we cut down to the last barber cutting.
Quote from johnwcowan on February 13, 2020, 1:31 amWhat makes the barber paradox different from Russell's is that we are not fundamentally surprised that no such barber can exist. Certainly we don't know any such barber! But naive set theory does hold that a function of one variable determines a set, so when we find out that {x  x is not a member of x} is not a set, we are surprised or in fact shocked, and we have to find a comprehension axiom that isn't subject to the paradox.
What makes the barber paradox different from Russell's is that we are not fundamentally surprised that no such barber can exist. Certainly we don't know any such barber! But naive set theory does hold that a function of one variable determines a set, so when we find out that {x  x is not a member of x} is not a set, we are surprised or in fact shocked, and we have to find a comprehension axiom that isn't subject to the paradox.
Quote from dandl on February 13, 2020, 7:03 amRussell's paradox places limits on naive set theory. All kinds of interesting things happen in theories that allow for selfreference, resulting in a whole range of identified contradictions: Epimenides, Berry, Grelling, Richard's: there are even those who study this topic quite seriously. These paradoxes are highly satisfying, because they lead to better theories.
But the Barber paradox is really a misnomer. The point is that under the terms set out by Russell there is no barber, so the question about who shaves the barber never arises. The result of the query headed {Barber, ShavedBy } is empty. This paradox is unsatisfying, because it is simply a sleight of hand. Nothing better comes of it.
Russell's paradox places limits on naive set theory. All kinds of interesting things happen in theories that allow for selfreference, resulting in a whole range of identified contradictions: Epimenides, Berry, Grelling, Richard's: there are even those who study this topic quite seriously. These paradoxes are highly satisfying, because they lead to better theories.
But the Barber paradox is really a misnomer. The point is that under the terms set out by Russell there is no barber, so the question about who shaves the barber never arises. The result of the query headed {Barber, ShavedBy } is empty. This paradox is unsatisfying, because it is simply a sleight of hand. Nothing better comes of it.
Quote from johnwcowan on February 13, 2020, 11:25 pmThere's a threefold division of paradoxes: the veridical, which are true when you don't expect it (the pirate's apprentice is only having his fifth birthday even though he's 21), the falsidical, which are untrue when you don't expect it), the falsidical, which are false and you expect it even though the argument seems sound but is subtly fallacious (proof that 1 = 2 by differentiation), and antinomies, in which there are equally sound arguments pro and con. I think they are all interesting.
The proof I mentioned is this:
x * y = x + x + x ... + x (y times), in particular:
x *x = x + x + x ... + x (x times), taking the derivative of both sides:
2x = 1 + 1 + 1 ... + 1 (x times), summing:
2x = x, dividing by x:
2 = 1
There's a threefold division of paradoxes: the veridical, which are true when you don't expect it (the pirate's apprentice is only having his fifth birthday even though he's 21), the falsidical, which are untrue when you don't expect it), the falsidical, which are false and you expect it even though the argument seems sound but is subtly fallacious (proof that 1 = 2 by differentiation), and antinomies, in which there are equally sound arguments pro and con. I think they are all interesting.
The proof I mentioned is this:
x * y = x + x + x ... + x (y times), in particular:
x *x = x + x + x ... + x (x times), taking the derivative of both sides:
2x = 1 + 1 + 1 ... + 1 (x times), summing:
2x = x, dividing by x:
2 = 1