Proving non satisfiability of the barbers paradox with tableau method

Question

The barbers paradox:

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.

Can someone please help me?

Answer 1

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!).

Answer 2

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