Tableaux to my knowledge are both sound and complete.
The statement: "If P is valid then tableau for -P eventually closes". Does this statement prove that tableau is sound and complete or would it only prove that tableau is complete?
Thank You.
-
Welcome to SE Philosophy! Thanks for your contribution. Please take a quick moment to take the tour or find help. You can perform searches here or seek additional clarification at the meta site. Don't forget, when someone has answered your question, you can click on the arrow to reward the contributor and the checkmark to select what you feel is the best answer. – J D Nov 16 '20 at 23:03
-
If you mean the standard FOL tableaux it states that they are sound and complete in the article you linked (FOL tableau section). – Conifold Nov 16 '20 at 23:23
If P is valid, then the tableau for -P eventually closes.
only states completeness: If P is valid, the tableau will find out. This does not rule out the possibility that the tableau will also close on the negation of some formulas that are not actually valid.
Soundness thus has to be expressed separately; it is the converse direction:
If the tableau for -P closes, then P is valid.
Again, this per se does not guarantee that the tableau will always close when P is valid.
Together, soundness and completeness are a biconditoinal statement:
The tableau for -P closes if and only if P is valid.
-
When you say it may "close on some formulas that are not actually valid", if we assumed P is valid and -P would be unsatisfiable. Surely the tableau will always close. When would it "close on formulas that are not actually valid"? Thanks a lot for your answer btw! – R2D2 Nov 17 '20 at 0:40
-
@R2D2 Sorry; I meant: The tableau will close on the negation of some formulas that are not actually valid (fixed that). That's when the tableeau calculus is unsound. – lemontree Nov 17 '20 at 13:30
