Single Idea 13761

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

Full Idea

In a tableau system no sequent is established until the final step of the proof, when the last branch closes, and until then we are simply exploring a hypothesis.

Gist of Idea

In a tableau proof no sequence is established until the final branch is closed; hypotheses are explored

Source

David Bostock (Intermediate Logic [1997], 7.3)

Book Reference

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


A Reaction

This compares sharply with a sequence calculus, where every single step is a conclusive proof of something. So use tableaux for exploring proofs, and then sequence calculi for writing them up?