Tableaux — Read

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

How to use Read

This page follows Tableaux in source order. Equations are native, unflattened MathML. Tableaux and proof trees have linear descriptions, exercises remain unsolved, and every source coordinate is available offline.

Seven disclosed reader corrections

The frozen source remains unchanged. These reviewed reader interventions are visible wherever the affected material is presented.

TR012-SOURCE-FORMULA-001: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch. Open the affected occurrence.
TR012-SOURCE-FORMULA-006: The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions. Open the affected occurrence.
TR012-SOURCE-FORMULA-007: The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument. Open the affected occurrence.
TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering. Open the affected occurrence.
TR012-SOURCE-PROSE-002: The reader removes the duplicated word in the source phrase 'left left.'
TR012-SOURCE-PROSE-003: The reader corrects the source phrase 'we can applying' to 'we can apply.' Open the affected occurrence.
TR012-SOURCE-TABLEAU-004: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.

Rules and tableau

A tableau is a systematic survey of the possible ways a sentence can be true or false in a structure. The building blocks of a tableau are signed formulas: sentences plus a truth value “sign,” either $T$ source 18 or $F$ source 18. These signed formulas are arranged in a (downward growing) tree.

Definition of a signed formula

A signed formula is a pair consisting of a truth value and a sentence, i.e., either: $T A or F A .$ source 24

source 21

Intuitively, we might read $T A$ source 29 as “ $A$ source 29 might be true” and $F A$ source 30 as “ $A$ source 30 might be false” (in some structure).

Each signed formula in the tree is either an assumption (which are listed at the very top of the tree), or it is obtained from a signed formula above it by one of a number of rules of inference. There are two rules for each possible main operator of the preceding formula, one for the case where the sign is $T$ source 37, and one for the case where the sign is $F$ source 38. Some rules allow the tree to branch, and some only add signed formulas to the branch. A rule may be (and often must be) applied not to the immediately preceding signed formula, but to any signed formula in the branch from the root to the place the rule is applied.

A branch is closed when it contains both $T A$ source 44 and $F A$ source 45. A closed tableau is one where every branch is closed. Under the intuitive interpretation, any branch describes a joint possibility, but $T A$ source 47 and $F A$ source 47 are not jointly possible. In other words, if a branch is closed, the possibility it describes has been ruled out. In particular, that means that a closed tableau rules out all possibilities of simultaneously making every assumption of the form $T A$ source 51 true and every assumption of the form $F A$ source 52 false.

A closed tableau for $A$ source 54 is a closed tableau with root $F A$ source 55. If such a closed tableau exists, all possibilities for $A$ source 56 being false have been ruled out; i.e., $A$ source 56 must be true in every structure.

Propositional Rules

Rules for $\neg$

Heading formula source: source 15

Definition of the negation tableau rules

Proof Tree: True-negation tableau rule

Premise: the complete formula not A, carrying the true sign. Apply the true-negation tableau rule. Continue the same branch with the complete formula A, carrying the false sign.

Premise: the complete formula not A, carrying the true sign.
Apply the true-negation tableau rule.
Continue the same branch with the complete formula A, carrying the false sign.

Source formula occurrences in object order

source 18

Proof Tree: False-negation tableau rule

Premise: the complete formula not A, carrying the false sign. Apply the false-negation tableau rule. Continue the same branch with the complete formula A, carrying the true sign.

Premise: the complete formula not A, carrying the false sign.
Apply the false-negation tableau rule.
Continue the same branch with the complete formula A, carrying the true sign.

Source formula occurrences in object order

source 23

source 17

Rules for $\land$

Heading formula source: source 29

Definition of the conjunction tableau rules

Proof Tree: True-conjunction tableau rule

Premise: the complete conjunction A and B, carrying the true sign. Apply the true-conjunction tableau rule. On the same branch, add A carrying the true sign, followed by B carrying the true sign.

Premise: the complete conjunction A and B, carrying the true sign.
Apply the true-conjunction tableau rule.
On the same branch, add A carrying the true sign, followed by B carrying the true sign.

Source formula occurrences in object order

source 32

Proof Tree: False-conjunction branching tableau rule

Premise: the complete conjunction A and B, carrying the false sign. Apply the false-conjunction tableau rule. Split the branch: the left child contains A carrying the false sign, and the right child contains B carrying the false sign.

Premise: the complete conjunction A and B, carrying the false sign.
Apply the false-conjunction tableau rule.
Split the branch: the left child contains A carrying the false sign, and the right child contains B carrying the false sign.

Source formula occurrences in object order

$F A ∣ F B$ source 41

source 39

source 31

Rules for $\lor$

Heading formula source: source 45

Definition of the disjunction tableau rules

Proof Tree: True-disjunction branching tableau rule

Premise: the complete disjunction A or B, carrying the true sign. Apply the true-disjunction tableau rule. Split the branch: the left child contains A carrying the true sign, and the right child contains B carrying the true sign.

Premise: the complete disjunction A or B, carrying the true sign.
Apply the true-disjunction tableau rule.
Split the branch: the left child contains A carrying the true sign, and the right child contains B carrying the true sign.

Source formula occurrences in object order

$T A ∣ T B$ source 50

source 48

Proof Tree: False-disjunction tableau rule

Premise: the complete disjunction A or B, carrying the false sign. Apply the false-disjunction tableau rule. On the same branch, add A carrying the false sign, followed by B carrying the false sign.

Premise: the complete disjunction A or B, carrying the false sign.
Apply the false-disjunction tableau rule.
On the same branch, add A carrying the false sign, followed by B carrying the false sign.

Source formula occurrences in object order

source 53

source 47

Rules for $\to$

Heading formula source: source 61

Definition of the conditional tableau rules

Proof Tree: True-conditional branching tableau rule

Premise: the complete conditional from A to B, carrying the true sign. Apply the true-conditional tableau rule. Split the branch: the left child contains A carrying the false sign, and the right child contains B carrying the true sign.

Premise: the complete conditional from A to B, carrying the true sign.
Apply the true-conditional tableau rule.
Split the branch: the left child contains A carrying the false sign, and the right child contains B carrying the true sign.

Source formula occurrences in object order

$F A ∣ T B$ source 66

source 64

Proof Tree: False-conditional tableau rule

Premise: the complete conditional from A to B, carrying the false sign. Apply the false-conditional tableau rule. On the same branch, add A carrying the true sign, followed by B carrying the false sign.

Premise: the complete conditional from A to B, carrying the false sign.
Apply the false-conditional tableau rule.
On the same branch, add A carrying the true sign, followed by B carrying the false sign.

Source formula occurrences in object order

source 69

source 63

The Cut Rule

Definition of the cut tableau rule

Proof Tree: Cut branching rule

The cut rule has no formula premise at the current branch node. Choose a formula A and split the current branch. The left child contains A carrying the true sign; the right child contains A carrying the false sign.

The cut rule has no formula premise at the current branch node.
Choose a formula A and split the current branch.
The left child contains A carrying the true sign; the right child contains A carrying the false sign.

Source formula occurrences in object order

$T A ∣ F A$ source 82

source 80

source 79

The cut tableau rule is not applied “to” a previous signed formula; rather, it allows every branch in a tableau to be split in two, one branch containing $T A$ source 88, the other $F A$ source 88. It is not necessary—any set of signed formulas with a closed tableau has one not using cut tableau rule—but it allows us to combine tableaus in a convenient way.

tableau

Definition of a tableau derivation

A tableau for assumptions $S_{1} A_{1}$ source 24, …, $S_{n} A_{n}$ source 25 (where each $S_{i}$ source 25 is either $T$ source 25 or $F$ source 25) is a finite tree of signed formulas satisfying the following conditions:

The $n$ source 28 topmost signed formulas of the tree are $S_{i} A_{i}$ source 29, one below the other.
Every signed formula in the tree that is not one of the assumptions results from a correct application of an inference rule to a signed formula in the branch above it.

A branch of a tableau is closed iff it contains both $T A$ source 35 and $F A$ source 35, and open otherwise. A tableau in which every branch is closed is a closed tableau (for its set of assumptions). If a tableau is not closed, i.e., if it contains at least one open branch, it is open.

source 23

Example of extending a tableau derivation

Every set of assumptions on its own is a tableau, but it will generally not be closed. (Obviously, it is closed only if the assumptions already contain a pair of signed formulas $T A$ source 46 and $F A$ source 46.)

From a tableau (open or closed) we can obtain a new, larger one by applying one of the rules of inference to a signed formula $A$ source 49 in it. The rule will append one or more signed formulas to the end of any branch containing the occurrence of $A$ source 51 to which we apply the rule.

For instance, consider the assumption $T A \land \neg A$ source 54. Here is the (open) tableau consisting of just that assumption:

Tableau: Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign

This source tableau has one node and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption.

Source formula occurrences in object order

source 58

We obtain a new tableau from it by applying the $\land T$ source 62 rule to the assumption. That rule allows us to add two new lines to the tableau, $T A$ source 64 and $T \neg A$ source 64:

Tableau: Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign, later construction stage two

This source tableau has three nodes and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule one.
Node three, continuing the branch below node two: the complete formula not A, carrying the true sign. Printed justification: true-conjunction tableau rule one.

Source formula occurrences in object order

source 66

When we write down tableaus, we record the rules we've applied on the right (e.g., $\land T 1$ source 76 means that the signed formula on that line is the result of applying the $\land T$ source 78 rule to the signed formula on line $1$ source 78). This new tableau now contains additional signed formulas, but to only one ( $T \neg A$ source 80) can we apply a rule (in this case, the $\neg T$ source 81 rule). This results in the closed tableau

Tableau: Closed tableau beginning with the complete formula A and not A, carrying the true sign

This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule one.
Node three, continuing the branch below node two: the complete formula not A, carrying the true sign. Printed justification: true-conjunction tableau rule one.
Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule three. The branch closes at this node.

Source formula occurrences in object order

source 84

source 42

Examples of tableau

Example proving that if A and B then A

Let's find a closed tableau for the sentence $(A \land B) \to A$ source 16.

We begin by writing the corresponding assumption at the top of the tableau.

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign

Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption.

Source formula occurrences in object order

source 20

There is only one assumption, so only one signed formula to which we can apply a rule. (For every signed formula, there is always at most one rule that can be applied: it's the rule for the corresponding sign and main operator of the sentence.) In this case, this means, we must apply $\to F$ source 29.

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign, later construction stage two

Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: false-conditional tableau rule one.
Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-conditional tableau rule one.

Source formula occurrences in object order

source 30

To keep track of which signed formulas we have applied their corresponding rules to, we write a checkmark next to the sentence. However, only write a checkmark if the rule has been applied to all open branches. Once a signed formula has had the corresponding rule applied in every open branch, we will not have to return to it and apply the rule again. In this case, there is only one branch, so the rule only has to be applied once. (Note that checkmarks are only a convenience for constructing tableaux and are not officially part of the syntax of tableaux.)

There is one new signed formula to which we can apply a rule: the $T A \land B$ source 50 on line $2$ source 50. Applying the $\land T$ source 51 rule results in:

Tableau: Closed tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign

This source tableau has five nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-conditional tableau rule one.
Node four, continuing the branch below node three: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule two.
Node five, continuing the branch below node four: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node.

Source formula occurrences in object order

source 52

Since the branch now contains both $T A$ source 66 (on line $4$ source 66) and $F A$ source 67 (on line $3$ source 67), the branch is closed. Since it is the only branch, the tableau is closed. We have found a closed tableau for $(A \land B) \to A$ source 69.

source 15

Example proving a nested conditional by tableau

Now let's find a closed tableau for $(\neg A \lor B) \to (A \to B)$ source 73.

We begin with the corresponding assumption:

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption.

Source formula occurrences in object order

source 77

The one signed formula in this tableau has main operator $\to$ source 81 and sign $F$ source 82, so we apply the $\to F$ source 82 rule to it to obtain:

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage two

Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one.
Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one.

Source formula occurrences in object order

source 84

We now have a choice as to whether to apply $\lor T$ source 95 to line $2$ source 96 or $\to F$ source 96 to line $3$ source 96. It actually doesn't matter which order we pick, as long as each signed formula has its corresponding rule applied in every branch. So let's pick the first one. The $\lor T$ source 99 rule allows the tableau to branch, and the two conclusions of the rule will be the new signed formulas added to the two new branches. This results in:

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage three

This source tableau has five nodes and two terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two.
Node five, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two.

Source formula occurrences in object order

source 102

We have not applied the $\to F$ source 115 rule to line $3$ source 115 yet: let's do that now. To save time, we apply it to both branches. Recall that we write a checkmark next to a signed formula only if we have applied the corresponding rule in every open branch. So it's a good idea to apply a rule at the end of every branch that contains the signed formula the rule applies to. That way we won't have to return to that signed formula lower down in the various branches.

Tableau: Partially closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

This source tableau has nine nodes and two terminal branches; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two.
Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three.
Node seven, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two.
Node eight, continuing the branch below node seven: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three.
Node nine, continuing the branch below node eight: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. The branch closes at this node.

Source formula occurrences in object order

source 122

The right branch is now closed. On the left branch, we can still apply the $\neg T$ source 144 rule to line $4$ source 144. This results in $F A$ source 145 and closes the left branch:

Tableau: Closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

This source tableau has ten nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. This node is marked checked.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two.
Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three.
Node seven, continuing the branch below node six: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule four. The branch closes at this node.
Node eight, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two.
Node nine, continuing the branch below node eight: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three.
Node ten, continuing the branch below node nine: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. The branch closes at this node.

Source formula occurrences in object order

source 146

source 72

Example closing a branching tableau

We can give tableaus for any number of signed formulas as assumptions. Often it is also necessary to apply more than one rule that allows branching; and in general a tableau can have any number of branches. For instance, consider a tableau for ${T A \lor (B \land C), F (A \lor B) \land (A \lor C)}$ source 178. We start by applying the $\lor T$ source 179 to the first assumption:

Tableau: Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

This source tableau has four nodes and two terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node four, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.

Source formula occurrences in object order

source 181

Now we can apply the $\land F$ source 192 rule to line $2$ source 192. We do this on both branches simultaneously, and can therefore check off line $2$ source 194:

Tableau: Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

This source tableau has eight nodes and four terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two.
Node five, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.
Node six, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node six splits into two branches.
Node seven, on the left branch below node six: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two.
Node eight, on the right branch below node six: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.

Source formula occurrences in object order

source 195

Now we can apply $\lor F$ source 216 to all the branches containing $A \lor B$ source 217:

Tableau: Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

This source tableau has twelve nodes and four terminal branches; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.
Node eight, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node eight splits into two branches.
Node nine, on the left branch below node eight: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node ten, continuing the branch below node nine: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node eleven, continuing the branch below node ten: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node twelve, on the right branch below node eight: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.

Source formula occurrences in object order

source 218

The leftmost branch is now closed. Let's now apply $\lor F$ source 250 to $A \lor C$ source 250:

Tableau: Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

This source tableau has sixteen nodes and four terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity.
Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node ten splits into two branches.
Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node fourteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node fifteen, continuing the branch below node fourteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity.
Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four.

Source formula occurrences in object order

source 251

Note that we moved the result of applying $\lor F$ source 297 a second time below for clarity. In this instance it would not have been needed, since the justifications would have been the same.

Two branches remain open, and $T B \land C$ source 301 on line $3$ source 301 remains unchecked. We apply $\land T$ source 302 to it to obtain a closed tableau:

Tableau: Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

This source tableau has twenty nodes and four terminal branches; four terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
Node ten splits into two branches.
Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node fourteen, continuing the branch below node thirteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three.
Node fifteen, continuing the branch below node fourteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node.
Node sixteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node seventeen, continuing the branch below node sixteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node eighteen, continuing the branch below node seventeen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four.
Node nineteen, continuing the branch below node eighteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three.
Node twenty, continuing the branch below node nineteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node.

Source formula occurrences in object order

source 304

For comparison, here's a closed tableau for the same set of assumptions in which the rules are applied in a different order:

Tableau: Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

This source tableau has sixteen nodes and four terminal branches; four terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two splits into two branches.
Node three, on the left branch below node two: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three.
Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule three.
Node five splits into two branches.
Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
Node seven, on the right branch below node five: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
Node eight, continuing the branch below node seven: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six.
Node nine, continuing the branch below node eight: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node.
Node ten, on the right branch below node two: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
Node eleven, continuing the branch below node ten: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three.
Node twelve, continuing the branch below node eleven: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule three.
Node twelve splits into two branches.
Node thirteen, on the left branch below node twelve: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
Node fourteen, on the right branch below node twelve: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
Node fifteen, continuing the branch below node fourteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six.
Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node.

Source formula occurrences in object order

source 366

source 173

Exercise on associativity and double negation tableaux

Unsolved exercise. The source supplies the prompt only; no solution is added.

Give closed tableaus of the following:

$T A \land (B \land C), F (A \land B) \land C$ source 421.
$T A \lor (B \lor C), F (A \lor B) \lor C$ source 422.
$T A \to (B \to C), F B \to (A \to C)$ source 423.
$T A, F \neg \neg A$ source 424.

source 418

Exercise on equivalences and De Morgan tableaux

Unsolved exercise. The source supplies the prompt only; no solution is added.

Give closed tableaus of the following:

$T (A \lor B) \to C, F A \to C$ source 431.
$T (A \to C) \land (B \to C), F (A \lor B) \to C$ source 432.
$F \neg (A \land \neg A)$ source 433.
$T B \to A, F \neg A \to \neg B$ source 434.
$F (A \to \neg A) \to \neg A$ source 435.
$F \neg (A \to B) \to \neg B$ source 436.
$T A \to C, F \neg (A \land \neg C)$ source 437.
$T A \land \neg C, F \neg (A \to C)$ source 438.
$T A \lor B, T \neg B, F A$ source 439Reader correction: The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions..
$T \neg A \lor \neg B, F \neg (A \land B)$ source 440.
$F (\neg A \land \neg B) \to \neg (A \lor B)$ source 441.
$F \neg (A \lor B) \to (\neg A \land \neg B)$ source 442.

source 428

Exercise on conditional and negation tableaux

Unsolved exercise. The source supplies the prompt only; no solution is added.

Give closed tableaus of the following:

$T \neg (A \to B), F A$ source 449.
$T \neg (A \land B), F \neg A \lor \neg B$ source 450.
$T A \to B, F \neg A \lor B$ source 451.
$F \neg \neg A \to A$ source 452.
$T A \to B, T \neg A \to B, F B$ source 453.
$T (A \land B) \to C, F (A \to C) \lor (B \to C)$ source 454.
$T (A \to B) \to A, F A$ source 455.
$F (A \to B) \lor (B \to C)$ source 456.

source 446

Proof-Theoretic Notions

Definition of tableau theoremhood

A sentence $A$ source 32 is a theorem if there is a closed tableau for $F A$ source 33. We write $⊢ A$ source 33 if $A$ source 33 is a theorem and $⊬ A$ source 34 if it is not.

source 31

Definition of tableau derivability

A sentence $A$ source 38 is derivable from a set of sentences $Γ$ source 39, $Γ ⊢ A$ source 39 iff there is a finite set ${B_{1}, \dots, B_{n}} \subseteq Γ$ source 40 and a closed tableau for the set ${F A, T B_{1}, \dots, T B_{n}} .$ source 42 If $A$ source 49 is not derivable from $Γ$ source 49 we write $Γ ⊬ A$ source 49.

source 37

Definition of tableau consistency

A set of sentences $Γ$ source 54 is inconsistent iff there is a finite set ${B_{1}, \dots, B_{n}} \subseteq Γ$ source 55 and a closed tableau for the set ${T B_{1}, \dots, T B_{n}} .$ source 57 If $Γ$ source 63 is not inconsistent, we say it is consistent.

source 53

Proposition: reflexivity of tableau derivability

If $A \in Γ$ source 68, then $Γ ⊢ A$ source 68.

source 66

Proof

If $A \in Γ$ source 72, ${A}$ source 72 is a finite subset of $Γ$ source 72 and the tableau

Tableau: Closed tableau beginning with the complete formula A, carrying the false sign

This source tableau has two nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: assumption. The branch closes at this node.

Source formula occurrences in object order

source 73

is closed.

End of proof.

Proposition: monotonicity of tableau derivability

If $Γ \subseteq Δ$ source 84 and $Γ ⊢ A$ source 84, then $Δ ⊢ A$ source 84.

source 82

Proof

Any finite subset of $Γ$ source 89 is also a finite subset of $Δ$ source 89.

End of proof.

Proposition: transitivity of tableau derivability

If $Γ ⊢ A$ source 94 and ${A} \cup Δ ⊢ B$ source 94, then $Γ \cup Δ ⊢ B$ source 95.

source 92

Proof

If ${A} \cup Δ ⊢ B$ source 99, then there is a finite subset $Δ_{0} = {C_{1}, \dots, C_{n}} \subseteq Δ$ source 99 such that $\begin{matrix} {F B, & T A, T C_{1}, \dots, T C_{n}} \\ has a closed tableau . If Γ ⊢ A then there is a finite set {D 1, \dots, D m} \subseteq Γ such that \\ {F A, & T D_{1}, \dots, T D_{m}} \end{matrix}$ source 101Reader correction: The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument. has a closed tableau.

Now consider the tableau with assumptions $F B, T C_{1}, \dots, T C_{n}, T D_{1}, \dots, T D_{m} .$ source 112 Apply the cut tableau rule on $A$ source 117. This generates two branches, one has $T A$ source 118 in it, the other $F A$ source 118. Thus, on the one branch, all of ${F B, T A, T C_{1}, \dots, T C_{n}}$ source 120 are available. Since there is a closed tableau for these assumptions, we can attach it to that branch; every branch through $T A$ source 126 closes. On the other branch, all of ${F A, T D_{1}, \dots, T D_{m}}$ source 127 are available, so we can also complete the other side to obtain a closed tableau. This shows $Γ \cup Δ ⊢ B$ source 132.

End of proof.

Note that this means that in particular if $Γ ⊢ A$ source 135 and $A ⊢ B$ source 135, then $Γ ⊢ B$ source 136. It follows also that if $A_{1}, \dots, A_{n} ⊢ B$ source 136 and $Γ ⊢ A_{i}$ source 137 for each $i$ source 137, then $Γ ⊢ B$ source 138.

Proposition characterizing inconsistency by derivability

$Γ$ source 142 is inconsistent iff $Γ ⊢ A$ source 142 for every sentence $A$ source 143.

source 140

Proof

Exercise.

End of proof.

Exercise proving the inconsistency characterization

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Proposition characterizing inconsistency by derivability

source 157

Proposition: compactness of tableau derivability and consistency

If $Γ ⊢ A$ source 165 then there is a finite subset $Γ_{0} \subseteq Γ$ source 165 such that $Γ_{0} ⊢ A$ source 166.
If every finite subset of $Γ$ source 167 is consistent, then $Γ$ source 168 is consistent.

source 162

Proof

If $Γ ⊢ A$ source 174, then there is a finite subset $Γ_{0} = {B_{1}, \dots, B_{n}}$ source 175 and a closed tableau for ${F A, T B_{1}, \dots, T B_{n}}$ source 176 This tableau also shows $Γ_{0} ⊢ A$ source 179.
If $Γ$ source 180 is inconsistent, then for some finite subset $Γ_{0} = {B_{1}, \dots, B_{n}}$ source 181 there is a closed tableau for ${T B_{1}, \dots, T B_{n}}$ source 183 This closed tableau shows that $Γ_{0}$ source 186 is inconsistent.

End of proof.

derivability and Consistency

We will now establish a number of properties of the derivability relation. They are independently interesting, but each will play a role in the proof of the completeness theorem.

Proposition combining derivability with inconsistency

If $Γ ⊢ A$ source 20 and $Γ \cup {A}$ source 20 is inconsistent, then $Γ$ source 21 is inconsistent.

source 19

Proof

There are finite $Γ_{0} = {B_{1}, \dots, B_{n}}$ source 25 and $Γ_{1} = {C_{1}, \dots, C_{n}} \subseteq Γ$ source 25Reader correction: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch. such that $\begin{matrix} {F A, & T B_{1}, \dots, T B_{n}} \\ {T A, & T C_{1}, \dots, T C_{m}} \end{matrix}$ source 27Reader correction: The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch. have closed tableaus. Using the cut tableau rule on $A$ source 33 we can combine these into a single closed tableau that shows $Γ_{0} \cup Γ_{1}$ source 34 is inconsistent. Since $Γ_{0} \subseteq Γ$ source 35 and $Γ_{1} \subseteq Γ$ source 36, $Γ_{0} \cup Γ_{1} \subseteq Γ$ source 36, hence $Γ$ source 37 is inconsistent.

End of proof.

Proposition relating derivability to inconsistency after adding not A

$Γ ⊢ A$ source 42 iff $Γ \cup {\neg A}$ source 42 is inconsistent.

source 40

Proof

First suppose $Γ ⊢ A$ source 46, i.e., there is a closed tableau for ${F A, T B_{1}, \dots, T B_{n}}$ source 48 Using the $\neg T$ source 52 rule, this can be turned into a closed tableau for ${T \neg A, T B_{1}, \dots, T B_{n}} .$ source 54

On the other hand, if there is a closed tableau for the latter, we can turn it into a closed tableau of the former by removing every formula that results from true-not tableau rule applied to the first assumption $T \neg A$ source 62 as well as that assumption, and adding the assumption $F A$ source 63. For if a branch was closed before because it contained the conclusion of true-not tableau rule applied to $T \neg A$ source 65, i.e., $F A$ source 65, the corresponding branch in the new tableau is also closed. If a branch in the old tableau was closed because it contained the assumption $T \neg A$ source 68 as well as $F \neg A$ source 68 we can turn it into a closed branch by applying $\neg F$ source 70 to $F \neg A$ source 70 to obtain $T A$ source 71. This closes the branch since we added $F A$ source 72 as an assumption.

End of proof.

Exercise proving the dual inconsistency equivalence

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove that $Γ ⊢ \neg A$ source 76 iff $Γ \cup {A}$ source 76 is inconsistent.

source 75

Proposition deriving inconsistency from A and not A

If $Γ ⊢ A$ source 80 and $\neg A \in Γ$ source 80, then $Γ$ source 80 is inconsistent.

source 79

Proof

Suppose $Γ ⊢ A$ source 85 and $\neg A \in Γ$ source 85. Then there are $B_{1}$ source 86, …, $B_{n} \in Γ$ source 86 such that \ ${F A, T B_{1}, \dots, T B_{n}}$ source 87 has a closed tableau. Replace the assumption false-signed A by true-signed not A, and insert the conclusion of the true-negation tableau rule applied to the replacement assumption, true-signed not A Reader correction TR012-SOURCE-PROOF-005: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering. after the assumptions. Any sentence in the tableau justified by appeal to line $1$ source 94 in the old tableau is now justified by appeal to line $n + 1$ source 95Reader correction: The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.. So if the old tableau was closed, the new one is. It shows that $Γ$ source 96 is inconsistent, since all assumptions are in $Γ$ source 97.

End of proof.

Proposition combining two inconsistent extensions of Gamma

If $Γ \cup {A}$ source 101 and $Γ \cup {\neg A}$ source 101 are both inconsistent, then $Γ$ source 102 is inconsistent.

source 100

Proof

If there are $B_{1}$ source 106, …, $B_{n} \in Γ$ source 106 and $C_{1}$ source 106, …, $C_{m} \in Γ$ source 107 such that $\begin{matrix} {T A, & T B_{1}, \dots, T B_{n}} and \\ {T \neg A, & T C_{1}, \dots, T C_{m}} \end{matrix}$ source 108 both have closed tableaus, we can construct a single, combined tableau that shows that $Γ$ source 115 is inconsistent by using as assumptions $T B_{1}$ source 116, …, $T B_{n}$ source 116 together with $T C_{1}$ source 117, …, $T C_{m}$ source 117, followed by an application of the cut tableau rule. This yields two branches, one starting with $T A$ source 119, the other with $F A$ source 120.

On the left Reader correction TR012-SOURCE-PROSE-002: The reader removes the duplicated word in the source phrase 'left left.' side, add the part of the first tableau below its assumptions. Here, every rule application is still correct, since each of the assumptions of the first tableau, including $T A$ source 125, is available. Thus, every branch below $T A$ source 126 closes.

On the right side, add the part of the second tableau below its assumption, with the results of any applications of $\neg T$ source 130 to $T \neg A$ source 130 removed. The conclusion of $\neg T$ source 131 to $T \neg A$ source 131 is $F A$ source 132, which is nevertheless available, as it is the conclusion of the cut tableau rule on the right side of the combined tableau.

If a branch in the second tableau was closed because it contained the assumption $T \neg A$ source 136 (which no longer appears as an assumption in the combined tableau) as well as $F \neg A$ source 138Reader correction: The reader corrects the source phrase 'we can applying' to 'we can apply.', we can apply Reader correction TR012-SOURCE-PROSE-003: The reader corrects the source phrase 'we can applying' to 'we can apply.' $\neg F$ source 138Reader correction: The reader corrects the source phrase 'we can applying' to 'we can apply.' to $F \neg A$ source 139 to obtain $T A$ source 139. Now the corresponding branch in the combined tableau also closes, because it contains the right-hand conclusion of the cut tableau rule, $F A$ source 142. If a branch in the second tableau closed for any other reason, the corresponding branch in the combined tableau also closes, since any signed formulas other than $T \neg A$ source 145 occurring on the branch in the old, second tableau also occur on the corresponding branch in the combined tableau.

End of proof.

derivability and the Propositional Connectives

Proposition: tableau derivability rules for conjunction

Both $A \land B ⊢ A$ source 28 and $A \land B ⊢ B$ source 29.
$A, B ⊢ A \land B$ source 30.

source 26

Proof

Both ${F A, T A \land B}$ source 37 and ${F B, T A \land B}$ source 38 have closed tableaus
Tableau: Closed tableau beginning with the complete formula A, carrying the false sign, later construction stage two
This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule two.
4. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node.
Source formula occurrences in object order
source 40
Reader correction: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
Tableau: Closed tableau beginning with the complete formula B, carrying the false sign
This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule two.
4. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node.
Source formula occurrences in object order
source 50
Reader correction: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
Here is a closed tableau for ${T A, T B, F A \land B}$ source 60:
Tableau: Closed tableau beginning with the complete formula A and B, carrying the false sign
This source tableau has five nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A and B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula B, carrying the true sign. Printed justification: assumption.
4. Node three splits into two branches.
5. Node four, on the left branch below node three: the complete formula A, carrying the false sign. Printed justification: false-conjunction tableau rule one. The branch closes at this node.
6. Node five, on the right branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conjunction tableau rule one. The branch closes at this node.
Source formula occurrences in object order
source 62

End of proof.

Proposition: tableau derivability rules for disjunction

${A \lor B, \neg A, \neg B}$ source 77 is inconsistent.
Both $A ⊢ A \lor B$ source 78 and $B ⊢ A \lor B$ source 78.

source 75

Proof

We give a closed tableau of ${T A \lor B, T \neg A, T \neg B}$ source 84:
Tableau: Closed tableau beginning with the complete formula A or B, carrying the true sign
This source tableau has seven nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A or B, carrying the true sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula not A, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula not B, carrying the true sign. Printed justification: assumption.
4. Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule two.
5. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: true-negation tableau rule three.
6. Node five splits into two branches.
7. Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
8. Node seven, on the right branch below node five: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
Source formula occurrences in object order
source 86
Both ${F A \lor B, T A}$ source 100 and ${F A \lor B, T B}$ source 101 have closed tableaus:
Tableau: Closed tableau beginning with the complete formula A or B, carrying the false sign
This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A or B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node.
Source formula occurrences in object order
source 103
Reader correction: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.
Tableau: Closed tableau beginning with the complete formula A or B, carrying the false sign, later construction stage two
This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A or B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node.
Source formula occurrences in object order
source 113
Reader correction: Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.

End of proof.

Proposition: tableau derivability rules for conditionals

$A, A \to B ⊢ B$ source 128.
Both $\neg A ⊢ A \to B$ source 130 and $B ⊢ A \to B$ source 130.

source 126

Proof

${F B, T A \to B, T A}$ source 136 has a closed tableau:
Tableau: Closed tableau beginning with the complete formula B, carrying the false sign, later construction stage two
This source tableau has five nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula A implies B, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: assumption.
4. Node three splits into two branches.
5. Node four, on the left branch below node three: the complete formula A, carrying the false sign. Printed justification: true-conditional tableau rule two. The branch closes at this node.
6. Node five, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conditional tableau rule two. The branch closes at this node.
Source formula occurrences in object order
source 138
Both ${F A \to B, T \neg A}$ source 148 and ${F A \to B, T B}$ source 149 have closed tableaus:
Tableau: Closed tableau beginning with the complete formula A implies B, carrying the false sign
This source tableau has five nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A implies B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula not A, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one.
5. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule two. The branch closes at this node.
Source formula occurrences in object order
source 151
Tableau: Closed tableau beginning with the complete formula A implies B, carrying the false sign, later construction stage two
This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula A implies B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one. The branch closes at this node.
Source formula occurrences in object order
source 162

End of proof.

Soundness

Explanation

A derivation system, such as tableaux, is sound if it cannot derive things that do not actually hold. Soundness is thus a kind of guaranteed safety property for derivation systems. Depending on which proof theoretic property is in question, we would like to know for instance, that

every derivable $A$ source 22 is a tautology;
if a sentence is derivable from some others, it is also a consequence of them;
if a set of sentences is inconsistent, it is unsatisfiable.

These are important properties of a derivation system. If any of them do not hold, the derivation system is deficient—it would derive too much. Consequently, establishing the soundness of a derivation system is of the utmost importance.

Because all these proof-theoretic properties are defined via closed tableaus of some kind or other, proving (1)–(3) above requires proving something about the semantic properties of closed tableaus. We will first define what it means for a signed formula to be satisfied in a structure, and then show that if a tableau is closed, no structure satisfies all its assumptions. (1)–(3) then follow as corollaries from this result.

Definition of satisfaction for signed formulas and branches

A valuation $v$ source 42 satisfies a signed formula $T A$ source 43 iff $v ⊨ A$ source 44, and it satisfies $F A$ source 45 iff $v ⊭ A$ source 46. $v$ source 46 satisfies a set of signed formulas $Γ$ source 47 iff it satisfies every $S A \in Γ$ source 48. $Γ$ source 48 is satisfiable if there is a valuation that satisfies it, and unsatisfiable otherwise.

source 41

Theorem: a closed tableau has no satisfying valuation

If $Γ$ source 55 has a closed tableau, $Γ$ source 55 is unsatisfiable.

source 53

Proof

Let's call a branch of a tableau satisfiable iff the set of signed formulas on it is satisfiable, and let's call a tableau satisfiable if it contains at least one satisfiable branch.

We show the following: Extending a satisfiable tableau by one of the rules of inference always results in a satisfiable tableau. This will prove the theorem: any closed tableau results by applying rules of inference to the tableau consisting only of assumptions from $Γ$ source 67. So if $Γ$ source 67 were satisfiable, any tableau for it would be satisfiable. A closed tableau, however, is clearly not satisfiable: every branch contains both $T A$ source 70 and $F A$ source 70, and no structure can both satisfy and not satisfy $A$ source 71.

Suppose we have a satisfiable tableau, i.e., a tableau with at least one satisfiable branch. Applying a rule of inference either adds signed formulas to a branch, or splits a branch in two. If the tableau has a satisfiable branch which is not extended by the rule application in question, it remains a satisfiable branch in the extended tableau, so the extended tableau is satisfiable. So we only have to consider the case where a rule is applied to a satisfiable branch.

Let $Γ$ source 82 be the set of signed formulas on that branch, and let $S A \in Γ$ source 83 be the signed formula to which the rule is applied. If the rule does not result in a split branch, we have to show that the extended branch, i.e., $Γ$ source 85 together with the conclusions of the rule, is still satisfiable. If the rule results in a split branch, we have to show that at least one of the two resulting branches is satisfiable.

First, we consider the possible inferences that do not result in a split branch.

The branch is expanded by applying $\neg T$ source 92 to $T \neg B \in Γ$ source 93. Then the extended branch contains the signed formulas $Γ \cup {F B}$ source 94. Suppose $v ⊨ Γ$ source 96. In particular, $v ⊨ \neg B$ source 97. Thus, $v ⊭ B$ source 98, i.e., $v$ source 99 satisfies $F B$ source 100.
The branch is expanded by applying $\neg F$ source 101 to $F \neg B \in Γ$ source 102: Exercise.
The branch is expanded by applying $\land T$ source 103 to $T B \land C \in Γ$ source 104, which results in two new signed formulas on the branch: $T B$ source 105 and $T C$ source 106. Suppose $v ⊨ Γ$ source 107, in particular $v ⊨ B \land C$ source 108. Then $v ⊨ B$ source 109 and $v ⊨ C$ source 110. This means that $v$ source 111 satisfies both $T B$ source 112 and $T C$ source 112.
The branch is expanded by applying $\lor F$ source 113 to $F B \lor C \in Γ$ source 114: Exercise.
The branch is expanded by applying $\to F$ source 115 to $F B \to C \in Γ$ source 116: This results in two new signed formulas on the branch: $T B$ source 117 and $F C$ source 118. Suppose $v ⊨ Γ$ source 119, in particular $v ⊭ B \to C$ source 120. Then $v ⊨ B$ source 121 and $v ⊭ C$ source 122. This means that $v$ source 123 satisfies both $T B$ source 124 and $F C$ source 124.

Now let's consider the possible inferences that result in a split branch.

The branch is expanded by applying $\land F$ source 164 to $F B \land C \in Γ$ source 165, which results in two branches, a left one continuing through $F B$ source 166 and a right one through $F C$ source 167. Suppose $v ⊨ Γ$ source 168, in particular $v ⊭ B \land C$ source 169. Then $v ⊭ B$ source 170 or $v ⊭ C$ source 171. In the former case, $v$ source 172 satisfies $F B$ source 173, i.e., $v$ source 173 satisfies the formulas on the left branch. In the latter, $v$ source 175 satisfies $F C$ source 176, i.e., $v$ source 176 satisfies the formulas on the right branch.
The branch is expanded by applying $\lor T$ source 178 to $T B \lor C \in Γ$ source 179: Exercise.
The branch is expanded by applying $\to T$ source 180 to $T B \to C \in Γ$ source 181: Exercise.
The branch is expanded by cut tableau rule: This results in two branches, one containing $T B$ source 183, the other containing $F B$ source 184. Since $v ⊨ Γ$ source 184 and either $v ⊨ B$ source 185 or $v ⊭ B$ source 186, $v$ source 187 satisfies either the left or the right branch.

End of proof.

Exercise completing omitted soundness cases

Unsolved exercise. The source supplies the prompt only; no solution is added.

Complete the proof of Theorem: a closed tableau has no satisfying valuation.

source 199

Corollary: tableau theorems are tautologies

If $⊢ A$ source 206 then $A$ source 206 is a tautology.

source 204

Corollary: tableau derivability implies semantic entailment

If $Γ ⊢ A$ source 211 then $Γ ⊨ A$ source 211.

source 209

Proof

If $Γ ⊢ A$ source 215 then for some $B_{1}$ source 215, …, $B_{n} \in Γ$ source 215, ${F A, T B_{1}, \dots, T B_{n}}$ source 216 has a closed tableau. By Theorem: a closed tableau has no satisfying valuation, every valuation $v$ source 219 either makes some $B_{i}$ source 220 false or makes $A$ source 220 true. Hence, if $v ⊨ Γ$ source 221 then also $v ⊨ A$ source 222.

End of proof.

Corollary: satisfiable formula sets are consistent

If $Γ$ source 227 is satisfiable, then it is consistent.

source 225

Proof

We prove the contrapositive. Suppose that $Γ$ source 231 is not consistent. Then there are $B_{1}$ source 232, …, $B_{n} \in Γ$ source 232 and a closed tableau for ${T B_{1}, \dots, T B_{n}}$ source 233. By Theorem: a closed tableau has no satisfying valuation, there is no $v$ source 235 such that $v ⊨ B_{i}$ source 236 for all $i = 1$ source 236, …, $n$ source 236. But then $Γ$ source 237 is not satisfiable.

End of proof.

Reading preferences

How to use Read

Rules and tableau

Definition of a signed formula

Propositional Rules

Rules for ¬

Definition of the negation tableau rules

Proof Tree: True-negation tableau rule

Proof Tree: False-negation tableau rule

Rules for ∧

Definition of the conjunction tableau rules

Proof Tree: True-conjunction tableau rule

Proof Tree: False-conjunction branching tableau rule

Rules for ∨

Definition of the disjunction tableau rules

Proof Tree: True-disjunction branching tableau rule

Proof Tree: False-disjunction tableau rule

Rules for →

Definition of the conditional tableau rules

Proof Tree: True-conditional branching tableau rule

Proof Tree: False-conditional tableau rule

The Cut Rule

Definition of the cut tableau rule

Proof Tree: Cut branching rule

tableau

Definition of a tableau derivation

Example of extending a tableau derivation

Tableau: Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign

Tableau: Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign, later construction stage two

Tableau: Closed tableau beginning with the complete formula A and not A, carrying the true sign

Examples of tableau

Example proving that if A and B then A

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign, later construction stage two

Tableau: Closed tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign

Example proving a nested conditional by tableau

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage two

Tableau: Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage three

Tableau: Partially closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

Tableau: Closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign

Example closing a branching tableau

Tableau: Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

Tableau: Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

Tableau: Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

Tableau: Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

Tableau: Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign

Tableau: Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two

Exercise on associativity and double negation tableaux

Exercise on equivalences and De Morgan tableaux

Exercise on conditional and negation tableaux

Proof-Theoretic Notions

Definition of tableau theoremhood

Definition of tableau derivability

Definition of tableau consistency

Proposition: reflexivity of tableau derivability

Proof

Tableau: Closed tableau beginning with the complete formula A, carrying the false sign

Proposition: monotonicity of tableau derivability

Proof

Proposition: transitivity of tableau derivability

Proof

Proposition characterizing inconsistency by derivability

Proof

Exercise proving the inconsistency characterization

Proposition: compactness of tableau derivability and consistency

Proof

derivability and Consistency

Proposition combining derivability with inconsistency

Proof

Proposition relating derivability to inconsistency after adding not A

Proof

Exercise proving the dual inconsistency equivalence

Proposition deriving inconsistency from A and not A

Proof

Proposition combining two inconsistent extensions of Gamma

Proof

derivability and the Propositional Connectives

Proposition: tableau derivability rules for conjunction

Proof

Rules for $\neg$

Rules for $\land$

Rules for $\lor$

Rules for $\to$