Semantic Tableaux

A semantic tableau is a tree representing all ways the conjunction of the formulas at the root of the tree can be true

Semantic Tableaux proofs for propositional logic are both sound and complete

• Decompose one compound formula into ways that the formula can be evaluated to T
• Close branches that contain contradictory formulas
• If every branch is closed, the formulas at the root are inconsistent.

Apply non-branching rules first

Ways to make truth:

Or

We can interpret as by De Morgan's law by default in Semantic Tableaux.

• A branch represents a disjunction: two ways to make the formula true
• A non-branch is a conjunction: both formulas are needed to make the conjunction true

proof

In a different order:

Show that are inconsistent

proof

Textual:

How can we prove ?

Recall that for an argument to be invalid:

• There must be a boolean valuation in which the premises are T and the conclusion is F (and we can say, the negation of the conclusion is T)
• Hence is consistent

So for an argument to be valid, is inconsistent.

Prove:

proof