# soundness and completeness of a proof method

the question : Instead of the standard rule for disjunction (where we process a disjunction A∨B with two branches—one with A and one with B) we use a rule where the result is two branches, one with A and ∼B and the other with ∼A and B.

the answer : The proof tree system with Change #1 is unsound but it is complete. Here is why the proof tree system with Change #1 is unsound. Some trees close, using these rules, which should not close. In particular, a tree for the two formulas p∨q and p≡q closes. Processing p∨q with the new rule gives us two branches, one with p and ∼q and the other with ∼p and q. Both of these are inconsistent with p≡q (processing this, the resulting branches have p and q both true, or both false) and the tree closes. But this tree should not close, as p∨q and p≡q are jointly satisfiable. They are true if p and q are both true. The system with Change #1 is still complete, because any complete open branch using the new rules just adds formulas (from the old system) rather than taking any away. The result is that any complete open branch will still determine an interpretation making every formula in the branch true. The argument for completeness still succeeds.

I don't quiet understand the answer, especially it doesn't quite define soundness and completeness. And from what I searched online, a proof system is sound if and only if every provable conclusion is logically entailed; (Σ⊢ϕ)inplies(Σ⊨ϕ) a proof system is complete if and only if every logically entailed conclusion is provable; (Σ⊨ϕ)implies(Σ⊢ϕ). But I failed to understand its meaning. Can someone give a better explanation and maybe a more detailed example?

• You may find this is a better match for the Mathematics stack exchange, because it is entirely contained in proof theory, a branch of mathematics, without calling on any philosophical argument. Hopefully they will not simply send you back here! Apr 14, 2015 at 15:19
• @CortAmmon Typically logic is considered entirely on topic here. Apr 14, 2015 at 16:22
• @jxhyc: An excellent book on this topic is "An Introduction to Non-Classical Logic" by G. Priest (ISBN-10 0521670268). Apr 14, 2015 at 18:29
• @ Moritz, thanks for the recommendation, I checked the book, it seem an interesting book. However, I doubt the question has something to do with non-classical logics Apr 14, 2015 at 19:02

Basically with a proof system, you're seeking a rule-based process that will allow you to evaluate as valid ALL and ONLY the admissible arguments that actually are valid.

• A SOUND system never characterizes any invalid argument as valid (but may throw out some of the good apples along with the bad). If your system is SOUND you can absolutely rely on any argument that makes it through the process, but you might miss some good ones.

• A COMPLETE system never fails to characterize a valid argument as valid (but may incorrectly endorse some invalid arguments). If your system is COMPLETE, you aren't missing anything, but you can't rely on what you have.

The standard proof tree system is SOUND and COMPLETE. Any open branch of the tree represents an interpretation where all the premises are in fact mutually consistent, and taken together, all the open branches cover every such interpretation. However, if you swap out that one rule, you can reach situations where some things can appear inconsistent that aren't.

What makes it tricky is that the correct way to evaluate an argument with proof trees is to see if the premises are compatible with the NEGATION of the conclusion. If so (and there are open branches on the finished tree), the argument is INVALID, if not (and all branches close), it is VALID. This is a little counterintuitive because you are checking the opposite of what you actually want to show (in fact, it took me quite a while to think through it myself while crafting this answer).

In the particular case of swapping out this rule (Change #1), you introduce times when some branches will close that shouldn't close. This will make some invalid arguments incorrectly seem valid. This makes the system no longer SOUND. However, you don't introduce any times when any branches stay open that should close, so every valid argument still seems valid, and thus the system is still COMPLETE.

• thanks,I realize where did I go wrong. As you said, proof tree is checking the opposite of what I am looking for. Apr 14, 2015 at 19:00
• Glad to help. If you found the answer useful you should be able to upvote and/or accept it by using the arrows and the checkmark next to the number on the left. Apr 14, 2015 at 19:24
• Good answer. Translated into the vocabulary of the physical sciences (which might be helpful for some readers): a complete system has the right precision. A sound system has accuracy in its evaluations. Apr 18, 2015 at 2:12