Single Idea 13612

[catalogued under 5. Theory of Logic / H. Proof Systems / 5. Tableau Proof]

Full Idea

Rules for semantic tableaus are of two kinds - non-branching rules and branching rules. The first allow the addition of further lines, and the second requires splitting the branch. A branch which assigns contradictory values to a formula is 'closed'.

Gist of Idea

Non-branching rules add lines, and branching rules need a split; a branch with a contradiction is 'closed'

Source

David Bostock (Intermediate Logic [1997], 4.1)

Book Reference

Bostock,David: 'Intermediate Logic' [OUP 1997], p.146


A Reaction

[compressed] Thus 'and' stays on one branch, asserting both formulae, but 'or' splits, checking first one and then the other. A proof succeeds when all the branches are closed, showing that the initial assumption leads only to contradictions.