How to draw the tableau of an inference

Question

I apologise if this may sound like a stupid question (I have searched online but couldn't find an answer) Is there a way to draw the tableau of an inference? For example if I have the following inference, how can I show using the tableau that the inference is true or not?

∀x,∀y(P(x, y)→P(y, x)), P(a, b) ⊢P(b, b)

Answer 1

There are some beautiful books :

• Raymond Smullyan, First-Order Logic (1968)

and

• Peter Smith, An Introduction to Formal Logic (2003),

but also :

• Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012).

---

In order to show if : $∀x∀y(P(x,y) → P(y,x)), P(a,b) ⊢ P(b,b)$ holds or not, we have to proceeed as for the propositional case, considering (for signed tableau) the set :

$S = \{ T \ ∀x∀y(P(x,y) → P(y,x)), T \ P(a,b), F \ P(b,b) \}$;

if it closes, then the set is unsatisfiable and thus the formula $P(b,b)$ is logical consequence of the premises.

The only rule we can apply to start with is $T \ \forall$ (twice) [see : R.Smullyan, page 54].