# Proving non satisfiability of the barbers paradox with tableau method

In a town there is only one barber. For every man in town, either the barber shaves him or he shaves him self.

I need to formalize this: The barber shaves exactely those who doesn't shave themselfes.

So I have formalized the problem in predicate logic as: ∀x(B(x,x)↔ ¬B(b,x))

Where the domain is all men in town, the B is for "_ shaves _" and b is the constant symbol for the barber.

I'm not totally sure that I have formalized it the right way. But anyway, I need to show that the formula is not satisfiable using the tableau method. That should be the same as showing that the negation of the formula is not valid (?) And in that case, I should make the tableau close.. (?)

I can't make the tableau close, and I think I might either have the formula written wrong, or I have misunderstanding of how to prove the satisfiability of a formula using the tableau method.

-

In your scenario, you have not required the barber to be a man in town. (Even the late, great Martin Gardner made this mistake!) The correct formalization of this scenario (using your notation) would be:

$\exists x \forall y (M(y) \rightarrow (B(x,y)\leftrightarrow \neg B(x,x))$

where $M(y)$ means $y$ is a man in town.

If you assume $M(x)$, then you would obtain a contradiction. Therefore, you must have $\neg M(x)$. Then the above requirement would be satisfied by several combination of shavers and shaved including, among other possibilities, the barber shaving every man in town, or every man shaving himself.

The usual formulation of the Barber Paradox has a man in town (the barber) who is required to shave those and only those men in town who do not shave themselves. Using your notation, that scenario would be formalized as:

$\exists x (M(x) \wedge \forall y (M(y) \rightarrow (B(x,y)\leftrightarrow \neg B(x,x)))$

In this case, there would be no combination of shavers and shaved that satisfied this requirement.

For a set-theoretic resolution of the Barber Paradox, see the video at my website at http://www.dcproof.com

-
But if the domain is all men in town, isn't it implied that x and b then is a man? Do I still need to include M(y) and M(x)? –  user1419999 Nov 25 '12 at 7:06
The scenario you describe in words and your formalism are inconsistent in this regard. In words, you mention nothing about the barber being a man in town. –  Dan Christensen Nov 25 '12 at 15:04
If you had said that the barber is a man in town, then strictly speaking, you wouldn't need the predicate $M$. But by not including $M$ and simply saying informally that the domain of is all men in town, you could easily miss out on the insight that it is actually the requirement that the barber be a man in town that is problematic, not his very existence. A set-theoretic analysis allows even further insights (see my link). –  Dan Christensen Nov 25 '12 at 15:32
The central issue is that for any man in town there cannot exist a binary relation defined on the set of those men that satisfies the requirements given. $\forall b\in M \neg \exists S \forall x\in M ((b,x)\in S \leftrightarrow \neg (x,x)\in S)$ It is impossible to arrive at this insight without set theory or higher order logic. –  Dan Christensen Nov 25 '12 at 18:26

General observation. Suppose you start a tableau with $\varphi$, and then apply the tableau unpacking rules (which, putting it crudely, reveal other things which need to be true if what's higher up a branch is true, considering branching options where necessary). If every branch ends in contradiction, then there is indeed no way of making $\varphi$ true, i.e. $\varphi$ is unsatisfiable.

[Compare: to show every interpretation makes $\varphi$ true, you proceed by showing that a tree starting $\neg\varphi$ closes, so $\neg\varphi$ is unsatisfiable.]

The Barber The problematic supposition is that there is such a man as the barber, i.e. that $$\exists x\forall y(Bxy \leftrightarrow \neg Byy)$$ where of course $Bxy$ says that $x$ shaves $y$, and the quantifier runs over the relevant people (men in the village, or whatever).

It is readily seen that this supposition leads to contradiction. For given that supposition, there must be a witness for the existential quantifier: dub it $b$ to get

$$\forall y(Bby \leftrightarrow \neg Byy)$$

But then, instantiating the universal, we'd in particular have

$$(Bbb \leftrightarrow \neg Bbb)$$

and to now show that this has to be false is trivial (just continue the tableau!).

-
It is easy to see that the statement can never be true. But how is the correct way to use the tableau method to show a formula is not satisfiable? I think I might be getting that part wrong... –  user1419999 Nov 25 '12 at 7:08
@user1419999 I've added a general comment about the use of tableaux. –  Peter Smith Nov 25 '12 at 12:29