Is A unsatisfiable if there is a completed tableau with all branches closed?

209 Views Asked by At

I am having troubles wrapping my head around unsatisfiability and satisfiability. I understand that A is said to be satisfiable if there exists at least one case where the formula A is true. But when it comes to tableaux i don't understand how conclusions are drawn with regards to unsatisfiability. I understand the mechanism of it but cant draw conclusions. I would appreciate any help or guidance. If you could provide an answer and example to the question it would be greatly appreciated.

1

There are 1 best solutions below

0
On BEST ANSWER

Short answer: yes, A is indeed unsatisfiable if there is a completed tableau with all branches closed!

For a longer answer which explains why, check out the opening pages of these notes on (propositional) truth-trees.

(These notes form a freely available appendix to the second ed. of my Introduction to Formal Logic. The main text is natural-deduction based, but this appendix covers tableaux as an alternative proof system.)