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?