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?