Quote from Dave Voorhis on December 17, 2019, 11:18 am

Quote from dandl on December 17, 2019, 5:31 am

Quote from Dave Voorhis on December 16, 2019, 10:26 pm

Quote from dandl on December 16, 2019, 10:05 pm

Quote from Dave Voorhis on December 16, 2019, 10:17 am

Quote from dandl on December 15, 2019, 11:41 pm

Quote from Dave Voorhis on December 15, 2019, 9:49 pm

Line 17 is the escape clause, otherwise you couldn't insert anyone who's shaved by the barber and couldn't insert a barber. And, yes, I think C4 is questionable. I've been thinking  about ways to recast the problem, but they'll have to wait until I have some time.

[...]

How will you judge the correctness of your solution where the goals seems to be qualitative, in terms of faithfulness to the original statement of the paradox or other unstated goals? How will you judge the OP goal of a "Russell Paradox smell"?

The same way we judge the correctness of any solution that can't be automatically evaluated: Rational analysis and logical thinking.

That's a straight cop-out. It says: I have no idea what I'm looking for but if I look rationally and logically I'll know it when I see it.

Have you thought this through? Do you actually know what you're looking for?

Your question is no more or less than, "if you've solved a math problem, how do you know the answer is right?"

'Create something with a Russell smell' is hardly a maths problem. It sounds more like an exploration in the hope of finding something interesting (for some definition of interesting).

It's a math problem. "Maths" isn't just "doing sums."

In fact, it's mainly not "doing sums."

And, yes, it's an exploration in hope of finding something interesting, which is what most of doing math is.

But to be more specific, I expect problems with a "Russell Paradox smell" -- whether genuinely Russellesque or pseudo paradoxes like the Barber's Paradox -- to be inexpressible, or expressible but result in unavoidable violation of necessary constraints, or expressible but result in infinite recursion.

You wrote dozens of lines of code on the Barber and then worried about a problem with one of them. I can do the whole thing in a line or two of pseudo-code. I'm trying to understand what it is you see in the problem that takes so much code to solve, and what you expect it to do if you manage it.

I wrote a Tutorial D equivalent to Erwin's model because it looked like a fun modelling problem. It was.

My subsequent attempt at capturing something Russellesque, via something notionally self-referential, consists of a single relvar with a single OPERATOR-typed attribute and a single tuple containing an operator that checks to see if the relvar contains the operator that checks to see if the relvar contains the operator that checks to see if the relvar contains the operator that che-...

One line.

And why should it blow up? Either you admit a barber with an undecidable 'shaves self' attribute, or you do not.

For example, in playing around with this I managed a moment ago to create a horrible little pseudo paradox (at least, I think it's a pseudo paradox) that runs for a while before it blows the stack and returns null. In Rel, null isn't a thing, so returning null is... something.. .. . that is not... uh... something.

That's undefined behaviour: rainbows and unicorns.

Of course; that's the point. Winding up in undefined behaviour territory -- which infinite recursion is in Rel -- is interesting.

Quote from Erwin on December 17, 2019, 8:54 pm

Quote from Dave Voorhis on December 15, 2019, 9:49 pm

Quote from Erwin on December 15, 2019, 8:43 pm

Quote from Dave Voorhis on December 12, 2019, 1:49 pm

Here's my Tutorial D equivalent:

// All people in a Russell world...
VAR Person REAL RELATION {ID CHARACTER} KEY {ID};

// ...either shave themselves...
VAR ShavesSelf REAL RELATION {ID CHARACTER} KEY {ID};

// ...or do not shave themselves.
VAR ShavesSelfNot REAL RELATION {ID CHARACTER} KEY {ID};

// The barber
VAR Barber REAL RELATION {ID CHARACTER} KEY {};

// Who shaves who?
VAR Shaves VIRTUAL
   UNION {
     ((EXTEND ShavesSelf: {Shaver := ID, Shavee := ID}) {ALL BUT ID}),
     IF IS_EMPTY(Barber) THEN
       REL {Shaver CHAR, Shavee CHAR} {}
     ELSE
       ((EXTEND ShavesSelfNot: {Shaver := ID FROM TUPLE FROM Barber, Shavee := ID}) {ALL BUT ID})
     END IF
   };

CONSTRAINT C1_All_Persons_Shave_Or_Not
   Person = ShavesSelf UNION ShavesSelfNot;

CONSTRAINT C2_Nobody_Both_Does_And_Does_Not_Shave
   IS_EMPTY(ShavesSelf INTERSECT ShavesSelfNot);

CONSTRAINT C3_Barber_Is_A_Person
   IS_EMPTY(Barber MINUS Person);

CONSTRAINT C4_All_Who_Dont_Shave_Themselves_Are_Shaved_By_Barber
   (Barber JOIN ShavesSelfNot) = (Barber JOIN ((Shaves RENAME {Shaver AS ID})) {ID});

CONSTRAINT C5_All_Who_Shave_Themselves_Are_Shaving_Themselves
   ShavesSelf = ((Shaves WHERE Shaver = Shavee) {Shavee}) RENAME {Shavee AS ID};

// Start with two people, one who shaves and one who does not.
INSERT Person REL {TUP {ID 'Dave'}}, INSERT ShavesSelf REL {TUP {ID 'Dave'}};
INSERT Person REL {TUP {ID 'Nikki'}}, INSERT ShavesSelfNot REL {TUP {ID 'Nikki'}};

Attempting to define a barber fails thusly:

INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};

ERROR: RS0285: Update will cause CONSTRAINT C4_All_Who_Dont_Shave_Themselves_Are_Shaved_By_Barber to fail.

INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};

ERROR: RS0285: Update will cause CONSTRAINT C5_All_Who_Shave_Themselves_Are_Shaving_Themselves to fail.

How come inserting Nikki is even possible ?  We got C4 wrong.  Or incomplete.  It's due to the join with empty barber.  Seems it must be rephrased as an equality, same style as C5 : ShaveSelfNot = ...

Line 17 is the escape clause, otherwise you couldn't insert anyone who's shaved by the barber and couldn't insert a barber. And, yes, I think C4 is questionable. I've been thinking  about ways to recast the problem, but they'll have to wait until I have some time.

Seems to me like C4 and C5 on their own are not enough.

Given the vars as they are, there are 3 ways to proceed to answering "does x shave himself ?" : just look in PSO or PSN, look in SHAVES to see if there's a (B,x) tuple (answer NO if there is), look in SHAVES to see if there's a (x,x) tuple (answer YES if there is).

Enforcing consistency of the answer requires enforcing the three-way equality  PSN == (Shaves WHERE Shaver<>Shavee) {Shavee} RENAME {Shavee as id} == (Shaves MATCHING (Barber RENAME {id as Shaver}) {Shavee} RENAME {Shavee as id}   and a similar one for PSO.

I think this one will cut it to only allowing worlds without barber where everyone shaves oneself.

The curious thing I now see is that countering this kind of paradoxes within the RM can seemingly be done by violating (or is it not ???) the principle of semantic orthogonality.

Quote from Erwin on December 17, 2019, 9:16 pm

Quote from AntC on December 16, 2019, 9:33 pm

Quote from Dave Voorhis on December 16, 2019, 10:17 am

Quote from dandl on December 15, 2019, 11:41 pm

Quote from Dave Voorhis on December 15, 2019, 9:49 pm

Line 17 is the escape clause, otherwise you couldn't insert anyone who's shaved by the barber and couldn't insert a barber. And, yes, I think C4 is questionable. I've been thinking  about ways to recast the problem, but they'll have to wait until I have some time.

[...]

How will you judge the correctness of your solution where the goals seems to be qualitative, in terms of faithfulness to the original statement of the paradox or other unstated goals? How will you judge the OP goal of a "Russell Paradox smell"?

The same way we judge the correctness of any solution that can't be automatically evaluated: Rational analysis and logical thinking.

In the case of this particular paradox, we have plenty of materials criss-crossing the ground. I'll quote from wikipedia whilst also noting it's supported by plenty of heavy-duty References and External links. The "smell" is to find a set R:

In case of the Barber, we have plenty of sets to consider: people; those who shave themselves; those who don't shave themselves; those who are shaved by barber(s); barber(s) even if there's only one of them; ...

For each of those sets, the elements are people. But to get a smell of Russell's Paradox we need a set whose elements (or at least some of them) are sets. That's what the x ∉ x is doing in the formula. I see no set-of-sets in the way the Barber's paradox is formulated.

So I'm agreeing with Russell himself: the Barber paradox is expressible within FOL (and therefore within a relational model); and does not exhibit Russell's Paradox.

Rational analysis/logical thinking/case closed.

Thanks for pointing this out.

It seems to me that the 'true' Russell paradox is by definition inexpressible in TTM db designs because TTM builds on sorted logic (because it builds on type theory) but your mathematical formulation seems to relate to unsorted logic (that is, your 'x' could be replaced with really just anything in the universe (and that in itself presumes that R already exists in the universe before being defined per your formula ...) ).

(PS, yes the question was intended "as a teaching exercise", but then one of the kind where the one getting the teaching would be me, from whatever responses I'd be getting.  In that sense it certainly hasn't failed.  Thank you to all for contributing.)

(PPS And yes, it was intended as an "exploration in the hope of finding something interesting".  At the very least, it has been interesting to me.)

Quote from AntC on December 18, 2019, 3:46 am

Quote from Erwin on December 17, 2019, 9:16 pm

Quote from AntC on December 16, 2019, 9:33 pm

Quote from Dave Voorhis on December 16, 2019, 10:17 am

Quote from dandl on December 15, 2019, 11:41 pm

Quote from Dave Voorhis on December 15, 2019, 9:49 pm

Line 17 is the escape clause, otherwise you couldn't insert anyone who's shaved by the barber and couldn't insert a barber. And, yes, I think C4 is questionable. I've been thinking  about ways to recast the problem, but they'll have to wait until I have some time.

[...]

How will you judge the correctness of your solution where the goals seems to be qualitative, in terms of faithfulness to the original statement of the paradox or other unstated goals? How will you judge the OP goal of a "Russell Paradox smell"?

The same way we judge the correctness of any solution that can't be automatically evaluated: Rational analysis and logical thinking.

In the case of this particular paradox, we have plenty of materials criss-crossing the ground. I'll quote from wikipedia whilst also noting it's supported by plenty of heavy-duty References and External links. The "smell" is to find a set R:

In case of the Barber, we have plenty of sets to consider: people; those who shave themselves; those who don't shave themselves; those who are shaved by barber(s); barber(s) even if there's only one of them; ...

For each of those sets, the elements are people. But to get a smell of Russell's Paradox we need a set whose elements (or at least some of them) are sets. That's what the x ∉ x is doing in the formula. I see no set-of-sets in the way the Barber's paradox is formulated.

So I'm agreeing with Russell himself: the Barber paradox is expressible within FOL (and therefore within a relational model); and does not exhibit Russell's Paradox.

Rational analysis/logical thinking/case closed.

Thanks for pointing this out.

It seems to me that the 'true' Russell paradox is by definition inexpressible in TTM db designs because TTM builds on sorted logic (because it builds on type theory) but your mathematical formulation seems to relate to unsorted logic (that is, your 'x' could be replaced with really just anything in the universe (and that in itself presumes that R already exists in the universe before being defined per your formula ...) ).

Russell's approach to resolving the paradox does introduce, yes, sorted logic: a set 'x' of sort/level n can be an element of a set 'y', but only if 'y' is of sort/level n+1. Note that nowhere does this require some base level of elements that are not sets. The n, n+1 are relative not absolute.

There's another possible approach, see the last sentence of the first para [from wikipedia on Russell's paradox, second para on ZFC]

In 1908, two ways of avoiding the paradox were proposed, Russell's type theory and the Zermelo set theory. Zermelo's axioms went well beyond Gottlob Frege's axioms of extensionality and unlimited set abstraction; as the first constructed axiomatic set theory, it evolved into the now-standard Zermelo–Fraenkel set theory (ZFC). The essential difference between Russell's and Zermelo's solution to the paradox is that Zermelo altered the axioms of set theory while preserving the logical language in which they are expressed, while Russell altered the logical language itself. The language of ZFC, with the help of Thoralf Skolem, turned out to be first-order logic.

Zermelo–Fraenkel set theory is intended to formalize a single primitive notion, that of a hereditary well-founded set, so that all entities in the universe of discourse are such sets. Thus the axioms of Zermelo–Fraenkel set theory refer only to pure sets and prevent its models from containing urelements (elements of sets that are not themselves sets). Furthermore, proper classes (collections of mathematical objects defined by a property shared by their members which are too big to be sets) can only be treated indirectly. Specifically, Zermelo–Fraenkel set theory does not allow for the existence of a universal set (a set containing all sets) nor for unrestricted comprehension, thereby avoiding Russell's paradox.

 

... (PPS And yes, it was intended as an "exploration in the hope of finding something interesting".  At the very least, it has been interesting to me.)

That last quoted sentence about avoiding a universal set might have a bearing on TTM's IM and its universal set Alpha. If all the sets-of-values for scalar types are subsets of Alpha, declared via constraint, can we declare a type PARADOX whose values are all those that don't appear in some type? If PARADOX is not empty (as is forbidden, because only Omega can be empty), any element of PARADOX ipso facto appears in some type, so is not eligible to be in PARADOX.

Quote from AntC on December 18, 2019, 4:21 am

Quote from Erwin on December 17, 2019, 8:54 pm

Quote from Dave Voorhis on December 15, 2019, 9:49 pm

Quote from Erwin on December 15, 2019, 8:43 pm

Quote from Dave Voorhis on December 12, 2019, 1:49 pm

Here's my Tutorial D equivalent: ...

How come inserting Nikki is even possible ?  We got C4 wrong.  Or incomplete.  It's due to the join with empty barber.  Seems it must be rephrased as an equality, same style as C5 : ShaveSelfNot = ...

Line 17 is the escape clause, otherwise you couldn't insert anyone who's shaved by the barber and couldn't insert a barber. And, yes, I think C4 is questionable. I've been thinking  about ways to recast the problem, but they'll have to wait until I have some time.

...

The curious thing I now see is that countering this kind of paradoxes within the RM can seemingly be done by violating (or is it not ???) the principle of semantic orthogonality.

The constraints have a contradiction somewhere, which mean that some relvar must be empty. So the semantic predicate for the relvar is not orthogonal to the constraints. That's no different to a single constraint IS_EMPTY( R). Do we count single-relvar constraints as orthogonal to the relvar declaration, or part of them, or what ? I think the answer will count as nit-picking whatever you want to say.

Just because the overall logic of relvar declarations + constraints is obfuscated doesn't make it necessarily orthogonal or not IMO.

Note the 'certain people' with the POOD have never managed to give a coherent account of it, let alone apply it to a reasonably meaty example like the Barber paradox. And IIRC McGoveran explicitly excludes inter-relational constraints from being subject to POOD (at least in one of his pronouncements).

Quote from AntC on December 18, 2019, 9:57 am

Quote from Erwin on December 15, 2019, 8:43 pm

Quote from Dave Voorhis on December 12, 2019, 1:49 pm

Here's my Tutorial D equivalent:

// All people in a Russell world...
VAR Person REAL RELATION {ID CHARACTER} KEY {ID};

// ...either shave themselves...
VAR ShavesSelf REAL RELATION {ID CHARACTER} KEY {ID};

// ...or do not shave themselves.
VAR ShavesSelfNot REAL RELATION {ID CHARACTER} KEY {ID};

// The barber
VAR Barber REAL RELATION {ID CHARACTER} KEY {};

// Who shaves who?
VAR Shaves VIRTUAL
   UNION {
     ((EXTEND ShavesSelf: {Shaver := ID, Shavee := ID}) {ALL BUT ID}),
     IF IS_EMPTY(Barber) THEN
       REL {Shaver CHAR, Shavee CHAR} {}
     ELSE
       ((EXTEND ShavesSelfNot: {Shaver := ID FROM TUPLE FROM Barber, Shavee := ID}) {ALL BUT ID})
     END IF
   };

CONSTRAINT C1_All_Persons_Shave_Or_Not
   Person = ShavesSelf UNION ShavesSelfNot;

CONSTRAINT C2_Nobody_Both_Does_And_Does_Not_Shave
   IS_EMPTY(ShavesSelf INTERSECT ShavesSelfNot);

CONSTRAINT C3_Barber_Is_A_Person
   IS_EMPTY(Barber MINUS Person);

CONSTRAINT C4_All_Who_Dont_Shave_Themselves_Are_Shaved_By_Barber
   (Barber JOIN ShavesSelfNot) = (Barber JOIN ((Shaves RENAME {Shaver AS ID})) {ID});

CONSTRAINT C5_All_Who_Shave_Themselves_Are_Shaving_Themselves
   ShavesSelf = ((Shaves WHERE Shaver = Shavee) {Shavee}) RENAME {Shavee AS ID};

// Start with two people, one who shaves and one who does not.
INSERT Person REL {TUP {ID 'Dave'}}, INSERT ShavesSelf REL {TUP {ID 'Dave'}};
INSERT Person REL {TUP {ID 'Nikki'}}, INSERT ShavesSelfNot REL {TUP {ID 'Nikki'}};

Attempting to define a barber fails thusly:

INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelf REL {TUP {ID 'BobTheBarber'}};

ERROR: RS0285: Update will cause CONSTRAINT C4_All_Who_Dont_Shave_Themselves_Are_Shaved_By_Barber to fail.

INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};INSERT Barber REL {TUP {ID 'BobTheBarber'}}, INSERT Person REL {TUP {ID 'BobTheBarber'}}, INSERT ShavesSelfNot REL {TUP {ID 'BobTheBarber'}};

ERROR: RS0285: Update will cause CONSTRAINT C5_All_Who_Shave_Themselves_Are_Shaving_Themselves to fail.

How come inserting Nikki is even possible ?  We got C4 wrong.

Yes. (As I'm discovering trying to code this up in a theorem prover.) Look at Erwin's OP definition for C4; look at the headings of the JOINs on each side of the EQD.

Those headings are not the same. C4 is ill-typed.

  Or incomplete.  It's due to the join with empty barber.  Seems it must be rephrased as an equality, same style as C5 : ShaveSelfNot = ...

Addit: also the definition of SHAVES has wrong heading

VAR SHAVES ::= {(B,P) | B IN BAR & P IN PSN}   UNION   {(P,P) | P IN PSO}

BAR has heading with single attribute P. So B IN BAR is ill-formed(?) Or do headings not apply for IN?

Addit2: Worse than that, C4 is nonsense: the LHS of the = doesn't correspond to the gloss:

" /* C4 : all persons who don't shave themselves are shaved by the barber */"

BAR JOIN PSN is not "all persons who don't shave themselves", it's "all persons who don't shave themselves and are barbers". Should be bare PSN, not BAR JOIN PSN.

C4 should be PSN = ((BAR RENAME {B := P}) JOIN SHAVES) { P }

Quote from AntC on December 18, 2019, 11:09 am

Quote from AntC on December 18, 2019, 9:57 am

Quote from Erwin on December 15, 2019, 8:43 pm

Quote from Dave Voorhis on December 12, 2019, 1:49 pm

 

How come inserting Nikki is even possible ?  We got C4 wrong.

Yes. (As I'm discovering trying to code this up in a theorem prover.) Look at Erwin's OP definition for C4; look at the headings of the JOINs on each side of the EQD.

Those headings are not the same. C4 is ill-typed.

  Or incomplete.  It's due to the join with empty barber.  Seems it must be rephrased as an equality, same style as C5 : ShaveSelfNot = ...

Addit: also the definition of SHAVES has wrong heading

VAR SHAVES ::= {(B,P) | B IN BAR & P IN PSN}   UNION   {(P,P) | P IN PSO}

BAR has heading with single attribute P. So B IN BAR is ill-formed(?) Or do headings not apply for IN?

Addit2: Worse than that, C4 is nonsense: the LHS of the = doesn't correspond to the gloss:

" /* C4 : all persons who don't shave themselves are shaved by the barber */"

BAR JOIN PSN is not "all persons who don't shave themselves", it's "all persons who don't shave themselves and are barbers". Should be bare PSN, not BAR JOIN PSN.

C4 should be PSN = ((BAR RENAME {B := P}) JOIN SHAVES) { P }

OK having adapted/corrected C4, I can now get proofs:

• no barber can exist.
• no person who doesn't shave themselves can exist.

Here's the axioms for the record, in Prover9 format (which I don't expect anybody much will understand).

% Barber Erwin, per PO-ish.

% pers(x)       ==> x is a person.
% psn(x)        ==> x doesn't shave themselves.
% pso(x)        ==> x shaves themself.
% bar(x)        ==> x is the/a barber.

% shaves(x, y)  ==> x shaves y.

pers(x) <-> (psn(x) | pso(x)).    % C1.
-(psn(x) & pso(x)).               % C2.

-(bar(x) & -(pers(x))).           % C3.

shaves(x, y) <-> (bar(x) & psn(y)) | (x = y & pso(x)).   % def'n of shaves

psn(x) <-> (exists z (bar(z) & shaves(z, x))).   % C4 adapted/corrected.
pso(x) <-> shaves(x, x).          % C5.

% goals -- these proven

pers(x) -> pso(x).                % all persons shave themselves.

-(exists x bar(x)).               % no barbers exist.
-(exists x psn(x)).               % no persons who are shaved exist

Note on syntax: % introduces a comment up to the end of the line; - is logical not; operators have precedence such that parens are not usually needed, although I've put in a few, specifically <-> bi-implication is least-binding.

Note on semantics: there's an implicit forall binding all free variables of each formula; it's at widest scope (so outside the - if that's the outermost operator).

One thing seems weird/is puzzling me: I have no constraint to say there must be at most one barber. Then what's stopping there being two barbers who shave each other?

Quote from Erwin on December 18, 2019, 9:50 pm

Quote from AntC on December 18, 2019, 11:09 am

Quote from AntC on December 18, 2019, 9:57 am

Quote from Erwin on December 15, 2019, 8:43 pm

Quote from Dave Voorhis on December 12, 2019, 1:49 pm

 

How come inserting Nikki is even possible ?  We got C4 wrong.

Yes. (As I'm discovering trying to code this up in a theorem prover.) Look at Erwin's OP definition for C4; look at the headings of the JOINs on each side of the EQD.

Those headings are not the same. C4 is ill-typed.

  Or incomplete.  It's due to the join with empty barber.  Seems it must be rephrased as an equality, same style as C5 : ShaveSelfNot = ...

Addit: also the definition of SHAVES has wrong heading

VAR SHAVES ::= {(B,P) | B IN BAR & P IN PSN}   UNION   {(P,P) | P IN PSO}

BAR has heading with single attribute P. So B IN BAR is ill-formed(?) Or do headings not apply for IN?

Addit2: Worse than that, C4 is nonsense: the LHS of the = doesn't correspond to the gloss:

" /* C4 : all persons who don't shave themselves are shaved by the barber */"

BAR JOIN PSN is not "all persons who don't shave themselves", it's "all persons who don't shave themselves and are barbers". Should be bare PSN, not BAR JOIN PSN.

C4 should be PSN = ((BAR RENAME {B := P}) JOIN SHAVES) { P }

OK having adapted/corrected C4, I can now get proofs:

• no barber can exist.
• no person who doesn't shave themselves can exist.

Here's the axioms for the record, in Prover9 format (which I don't expect anybody much will understand).

% Barber Erwin, per PO-ish.

% pers(x)       ==> x is a person.
% psn(x)        ==> x doesn't shave themselves.
% pso(x)        ==> x shaves themself.
% bar(x)        ==> x is the/a barber.

% shaves(x, y)  ==> x shaves y.

pers(x) <-> (psn(x) | pso(x)).    % C1.
-(psn(x) & pso(x)).               % C2.

-(bar(x) & -(pers(x))).           % C3.

shaves(x, y) <-> (bar(x) & psn(y)) | (x = y & pso(x)).   % def'n of shaves

psn(x) <-> (exists z (bar(z) & shaves(z, x))).   % C4 adapted/corrected.
pso(x) <-> shaves(x, x).          % C5.

% goals -- these proven

pers(x) -> pso(x).                % all persons shave themselves.

-(exists x bar(x)).               % no barbers exist.
-(exists x psn(x)).               % no persons who are shaved exist

Note on syntax: % introduces a comment up to the end of the line; - is logical not; operators have precedence such that parens are not usually needed, although I've put in a few, specifically <-> bi-implication is least-binding.

Note on semantics: there's an implicit forall binding all free variables of each formula; it's at widest scope (so outside the - if that's the outermost operator).

One thing seems weird/is puzzling me: I have no constraint to say there must be at most one barber. Then what's stopping there being two barbers who shave each other?

From Mikito Harakiri's posts here (VT if you didn't get it), I vaguely seem to recall that your prover system is also able to print out the detailed proofs.  I'd say time to dig into one and try to debug it ...

Quote from dandl on December 18, 2019, 11:26 pm

Quote from AntC on December 18, 2019, 11:09 am

One thing seems weird/is puzzling me: I have no constraint to say there must be at most one barber. Then what's stopping there being two barbers who shave each other?

If you define the barber as "one who shaves all those, and those only, who do not shave themselves" then:

1. There cannot be two barbers if there are any non-self-shavers, unless each is shaved by both barbers.
2. Each barber may shave the other, but it remains both true and untrue that the barber shaves himself as well.

The problem statement doesn't really deal with the issues of multiple barbers and multiple shavings.