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?


If you change the rule for ∨, you are changing the meaning of the connective.

The new rule changes "OR" from inclusive into exclusive : $¬(A∧B)$. Thus, the new meaning of ∨ has the result that it is nor more compatible with $\equiv$.

As you said, applying the new rule to the truth tree with the formulae :

$\{ p \lor q \ , \ p \equiv q \}$

we get that all branches closes and this means that the two above formulae are not jointly satisfiable.

The truth-tree method is a proof system, and we say that a proof system is sound when it proves only valid formulae (i.e. tautologies for the propositional calculus); more generally (again as you said), we say that the proof system is sound when :

if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$.

If we apply the truth-tree method to a single formula $\varphi$ and all branches are closed, we conclude that $\varphi$ is unsatisfiable, and thus its negation : $\lnot \varphi$ is a tautology.

If we apply it to two (or more) formulae and all branches are closed, we conclude that the last formula is not a logical consequence of the other one (or of the remaining ones).

In your case, the "modified" rule allows us to prove :

$p \lor q \vDash \lnot (p \equiv q)$

from which we can conclude that :

$(p \lor q) \to \lnot (p \equiv q)$

is a tautology.

But this is not so : consider a valuation $v$ such that $v(p)=v(q)=$t; with it we have that : $v(p \lor q)=$t and : $v(\lnot (p \equiv q))=$f.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.