Tableaux — Read

Reading preferences

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

How to use Read

This page follows the accepted First-order Tableaux projection in source order. All 589 formula occurrences use native, unflattened MathML. Fifty tableaux and seventeen proof trees retain complete ordered semantic descriptions and terminal-path linearizations.

Seven preserved source defects; twenty exact anchors

The reader preserves the source bytes without silent correction and gives an explicit reader correction at every applicable surface.

TR022-SOURCE-FORMULA-001: Gamma one ends at C sub n, but the next displayed tableau row ends at C sub m — 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. Source anchors: line 26, line 31.
TR022-SOURCE-FORMULA-006: The source places comma not B inside the formula argument carrying the true sign, then separately gives false-signed A. — 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. Source anchors: line 439.
TR022-SOURCE-FORMULA-007: The frozen source prints D sub one, through D sub m is a subset of Gamma; grammatically, only D sub m is placed to the left of the subset relation, although D sub m is a formula rather than a set. — 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. Source anchors: line 105.
TR022-SOURCE-PROOF-005: After replacing false-signed A by true-signed not A, the source says to apply the true-negation rule to false-signed A and identifies the derived false-signed A as line n plus one. — 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. Source anchors: line 90, line 91, line 92, line 93, line 94, line 95.
TR022-SOURCE-PROSE-002: left left — The reader removes the duplicated word in the source phrase 'left left.' Source anchors: line 122.
TR022-SOURCE-PROSE-003: we can applying — The reader corrects the source phrase 'we can applying' to 'we can apply.' Source anchors: line 138.
TR022-SOURCE-TABLEAU-004: The truth-value sign macro encloses the formula where sFmla expects separate sign and formula arguments. — 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. Source anchors: line 43, line 44, line 53, line 54, line 106, line 107, line 116, line 117.

Two preserved source-semantic discrepancies; nineteen exact anchors

The formulas and printed source remain unchanged. These notices identify two internal source inconsistencies so the reader does not silently harmonize them.

TR022-READER-DISCREPANCY-SCHEMATIC-LETTER-001: The frozen source uses schematic B in the quantified premises but switches to schematic A in the stated conclusions and proof steps. The edition preserves both schematic letters and explicitly discloses the switch; it does not silently harmonize the formulas. Exact affected source lines: line 128, line 129, line 131, line 132, line 133, line 136, line 137, line 140, line 141, line 144, line 145, line 152, line 153, line 154, line 155, line 156.
TR022-READER-DISCREPANCY-IDENTITY-SIGN-001: The frozen source prints generic sign S for the added identity conclusion inside a case whose rule statement and proof use the true sign. The edition preserves the generic sign and the true-sign rule context and explicitly discloses their mismatch; it does not silently harmonize them. Exact affected source lines: line 30, line 31, line 32.

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$ source 15

Definition of the negation tableau rules

Proof diagram: 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 21

Proof diagram: 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 26

source 17

Rules for $\land$ source 29

Definition of the conjunction tableau rules

Proof diagram: 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 37

Proof diagram: 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.

Additional native source formulas in object order

$F A ∣ F B$ source 41

source 42

source 31

Rules for $\lor$ source 45

Definition of the disjunction tableau rules

Proof diagram: 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.

Additional native source formulas in object order

$T A ∣ T B$ source 50

source 51

Proof diagram: 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 58

source 47

Rules for $\to$ source 61

Definition of the conditional tableau rules

Proof diagram: 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.

Additional native source formulas in object order

$F A ∣ T B$ source 66

source 67

Proof diagram: 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 74

source 63

The Cut Rule

Definition of the cut tableau rule

Proof diagram: 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.

Additional native source formulas in object order

$T A ∣ F A$ source 82

source 83

source 79

The cut rule 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 rule—but it allows us to combine tableaus in a convenient way.

Quantifier Rules

Rules for $\forall$ source 13

Definition of the universal-quantifier tableau rules

Proof diagram: True-universal tableau rule

Premise: every x satisfies A of x, carrying the true sign. Apply the true-universal tableau rule, choosing any closed term t. Continue the branch with A of t carrying the true sign.

Premise: every x satisfies A of x, carrying the true sign.
Apply the true-universal tableau rule, choosing any closed term t.
Continue the branch with A of t carrying the true sign.

source 19

Proof diagram: False-universal tableau rule

Premise: every x satisfies A of x, carrying the false sign. Apply the false-universal tableau rule with a new constant a that does not occur earlier on the branch. Continue the branch with A of a carrying the false sign.

Premise: every x satisfies A of x, carrying the false sign.
Apply the false-universal tableau rule with a new constant a that does not occur earlier on the branch.
Continue the branch with A of a carrying the false sign.

source 24

source 15

In true-signed universal-quantifier tableau rule, $t$ source 27 is a closed term (i.e., one without variables). In false-signed universal-quantifier tableau rule, $a$ source 28 is a constant which must not occur anywhere in the branch above false-signed universal-quantifier tableau rule. We call $a$ source 30 the eigenvariable of the false-signed universal-quantifier tableau rule inference.We use the term “eigenvariable” even though $a$ source 32 in the above rule is a constant. This has historical reasons.

Rules for $\exists$ source 35

Definition of the existential-quantifier tableau rules

Proof diagram: True-existential tableau rule

Premise: there exists an x satisfying A of x, carrying the true sign. Apply the true-existential tableau rule with a new constant a that does not occur earlier on the branch. Continue the branch with A of a carrying the true sign.

Premise: there exists an x satisfying A of x, carrying the true sign.
Apply the true-existential tableau rule with a new constant a that does not occur earlier on the branch.
Continue the branch with A of a carrying the true sign.

source 41

Proof diagram: False-existential tableau rule

Premise: there exists an x satisfying A of x, carrying the false sign. Apply the false-existential tableau rule, choosing any closed term t. Continue the branch with A of t carrying the false sign.

Premise: there exists an x satisfying A of x, carrying the false sign.
Apply the false-existential tableau rule, choosing any closed term t.
Continue the branch with A of t carrying the false sign.

source 46

source 37

Again, $t$ source 49 is a closed term, and $a$ source 49 is a constant which does not occur in the branch above the true-signed existential-quantifier tableau rule. We call $a$ source 51 the eigenvariable of the true-signed existential-quantifier tableau rule inference.

The condition that an eigenvariable not occur in the branch above the false-signed universal-quantifier tableau rule or true-signed existential-quantifier tableau rule inference is called the eigenvariable condition.

Explanation

Recall the convention that when $A$ source 58 is a formula with the variable $x$ source 59 free, we indicate this by writing $A (x)$ source 59. In the same context, $A (t)$ source 60 then is short for $A [t / x]$ source 60. So we could also write the false-signed existential-quantifier tableau rule as:

Proof diagram: False-existential rule written with explicit substitution

Premise: there exists an x satisfying A, carrying the false sign. Apply the false-existential tableau rule, choosing a closed term t. Continue the branch with the result of substituting t for x in A, carrying the false sign.

Premise: there exists an x satisfying A, carrying the false sign.
Apply the false-existential tableau rule, choosing a closed term t.
Continue the branch with the result of substituting t for x in A, carrying the false sign.

source 62

Note that $t$ source 67 may already occur in $A$ source 67, e.g., $A$ source 67 might be $P (t, x)$ source 68. Thus, inferring $F P (t, t)$ source 68 from $F \exists x P (t, x)$ source 69 is a correct application of false-signed existential-quantifier tableau rule. However, the eigenvariable conditions in false-signed universal-quantifier tableau rule and true-signed existential-quantifier tableau rule require that the constant $a$ source 72 does not occur in $A$ source 73. So, you cannot correctly infer $F P (a, a)$ source 74 from $F \forall x P (a, x)$ source 75 using $\forall F$ source 76.

Explanation

In true-signed universal-quantifier tableau rule and false-signed existential-quantifier tableau rule there are no restrictions on the term $t$ source 81. On the other hand, in the true-signed existential-quantifier tableau rule and false-signed universal-quantifier tableau rule rules, the eigenvariable condition requires that the constant $a$ source 83 does not occur anywhere in the branches above the respective inference. It is necessary to ensure that the system is sound. Without this condition, the following would be a closed tableau for $\exists x A (x) \to \forall x A (x)$ source 87:

Tableau: Closed tableau beginning with the complete formula the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is for every variable x, formula A with argument variable x, carrying the false sign

This source tableau has five formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, formula A with argument variable x, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one.
Node three, continuing the branch below node two: the complete formula for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.
Node four, continuing the branch below node three: the complete formula A with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula A with argument constant a, carrying the false sign. Printed justification: false-universal quantifier tableau rule, applied to line three. The branch closes at this node.

Closed tableau beginning with the complete formula the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is for every variable x, formula A with argument variable x, carrying the false sign

Path 1, closed. the complete formula the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula for some variable x, formula A with argument variable x, carrying the true sign Then the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula A with argument constant a, carrying the true sign Then the complete formula A with argument constant a, carrying the false sign

source 89

However, $\exists x A (x) \to \forall x A (x)$ source 105 is not valid.

tableau

Definition of a tableau derivation

Tableau

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 the conjunction of formula A and the negation of formula A, carrying the true sign

This source tableau has one formula nodes and one terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

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

Open or intermediate tableau beginning with the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign

Path 1, open-or-intermediate. the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign

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 the conjunction of formula A and the negation of formula A, carrying the true sign, later construction stage two

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

Node one, at the root: the complete formula the conjunction of formula A and the negation of formula 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, applied to line one.
Node three, continuing the branch below node two: the complete formula the negation of formula A, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line one.

Open or intermediate tableau beginning with the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign, later construction stage two

Path 1, open-or-intermediate. the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula the negation of formula A, carrying the true sign

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 the conjunction of formula A and the negation of formula A, carrying the true sign

This source tableau has four formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conjunction of formula A and the negation of formula 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, applied to line one.
Node three, continuing the branch below node two: the complete formula the negation of formula A, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line one.
Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule, applied to line three. The branch closes at this node.

Closed tableau beginning with the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign

Path 1, closed. the complete formula the conjunction of formula A and the negation of formula A, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula A, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign. Printed justification: assumption.

Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign, later construction stage two

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula the conjunction of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one.
Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign Then the complete formula the conjunction of formula A and formula B, carrying the true sign Then the complete formula A, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula the conjunction of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line 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, applied to line one.
Node four, continuing the branch below node three: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line two. The branch closes at this node.

Closed tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Path 1, closed. the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign Then the complete formula the conjunction of formula A and formula B, carrying the true sign Then the complete formula A, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign

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 the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign. Printed justification: assumption.

Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign, later construction stage two

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula 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 the disjunction of the negation of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one.
Node three, continuing the branch below node two: the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign, later construction stage three

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

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula 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 the disjunction of the negation of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the negation of formula A, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line two.
Node five, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line two.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the negation of formula A, carrying the true sign
Path 2, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula B, carrying the true sign

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 the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

This source tableau has nine formula nodes and two terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula 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 the disjunction of the negation of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the negation of formula A, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line three.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line three.
Node seven, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line two.
Node eight, continuing the branch below node seven: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line three.
Node nine, continuing the branch below node eight: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line three. The branch closes at this node.

Partially closed tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign
Path 2, closed. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign

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 the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

This source tableau has ten formula nodes and two terminal paths; two are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula 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 the disjunction of the negation of formula A and formula B, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the negation of formula A, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line three.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line three.
Node seven, continuing the branch below node six: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule, applied to line 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, applied to line two.
Node nine, continuing the branch below node eight: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line three.
Node ten, continuing the branch below node nine: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line three. The branch closes at this node.

Closed tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign

Path 1, closed. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign Then the complete formula A, carrying the false sign
Path 2, closed. the complete formula the conditional whose antecedent is open parenthesis, the disjunction of the negation of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula the disjunction of the negation of formula A and formula B, carrying the true sign Then the complete formula open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign

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

Node one, at the root: the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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 the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula 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, applied to line one.
Node four, on the right branch below node two: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line one.

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

Path 1, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign
Path 2, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign, later construction stage two

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

Node one, at the root: the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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 the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula 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, applied to line one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.
Node five, on the right branch below node three: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.
Node six, on the right branch below node two: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line one.
Node six splits into two branches.
Node seven, on the left branch below node six: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.
Node eight, on the right branch below node six: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.

Path 1, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign
Path 2, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign
Path 3, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign
Path 4, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign

This source tableau has twelve formula nodes and four terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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 the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula 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, applied to line one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line four.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line four. The branch closes at this node.
Node seven, on the right branch below node three: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.
Node eight, on the right branch below node two: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line one.
Node eight splits into two branches.
Node nine, on the left branch below node eight: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line four.
Node eleven, continuing the branch below node ten: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line four.
Node twelve, on the right branch below node eight: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line two.

Partially closed tableau beginning with the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign

Path 1, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
Path 2, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign
Path 3, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
Path 4, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign, later construction stage two

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

Node one, at the root: the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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 the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula 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, applied to line one.
Node three splits into two branches.
Node four, on the left branch below node three: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line four.
Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line four. The branch closes at this node.
Node seven, on the right branch below node three: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line 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, applied to line four. The branch closes at this node.
Node ten, on the right branch below node two: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line one.
Node ten splits into two branches.
Node eleven, on the left branch below node ten: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line four.
Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line four.
Node fourteen, on the right branch below node ten: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line 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, applied to line four.

Partially closed tableau beginning with the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign, later construction stage two

Path 1, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
Path 2, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign
Path 3, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
Path 4, open-or-intermediate. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign

This source tableau has twenty formula nodes and four terminal paths; four are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

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

Closed tableau beginning with the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign

Path 1, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
Path 2, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign
Path 3, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula C, carrying the true sign
Path 4, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula C, carrying the true sign

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 the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign, later construction stage two

This source tableau has sixteen formula nodes and four terminal paths; four are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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 the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula 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 the disjunction of formula A and formula B, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line three.
Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line 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, applied to line one. The branch closes at this node.
Node seven, on the right branch below node five: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line 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, applied to line six.
Node nine, continuing the branch below node eight: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line six. The branch closes at this node.
Node ten, on the right branch below node two: the complete formula the disjunction of formula A and formula C, carrying the false sign. Printed justification: false-conjunction tableau rule, applied to line 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, applied to line three.
Node twelve, continuing the branch below node eleven: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line 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, applied to line one. The branch closes at this node.
Node fourteen, on the right branch below node twelve: the complete formula the conjunction of formula B and formula C, carrying the true sign. Printed justification: true-disjunction tableau rule, applied to line 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, applied to line six.
Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line six. The branch closes at this node.

Closed tableau beginning with the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign, later construction stage two

Path 1, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign Then the complete formula A, carrying the true sign
Path 2, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula B, carrying the true sign Then the complete formula C, carrying the true sign
Path 3, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign Then the complete formula A, carrying the true sign
Path 4, closed. the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis, carrying the true sign Then the complete formula the conjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and open parenthesis, the disjunction of formula A and formula C, close parenthesis, carrying the false sign Then the complete formula the disjunction of formula A and formula C, carrying the false sign Then the complete formula A, carrying the false sign Then the complete formula C, carrying the false sign Then the complete formula the conjunction of formula B and formula C, carrying the true sign Then the complete formula B, carrying the true sign Then the complete formula C, carrying the true sign

source 366

source 173

Exercise on associativity and double negation tableaux

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

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 439.
$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

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

tableau with Quantifiers

Example closing a quantified conditional tableau

When dealing with quantifiers, we have to make sure not to violate the eigenvariable condition, and sometimes this requires us to play around with the order of carrying out certain inferences. In general, it helps to try and take care of rules subject to the eigenvariable condition first (they will be higher up in the finished tableau).

Let's see how we'd give a tableau for the sentence $\exists x \neg A (x) \to \neg \forall x A (x)$ source 21. Starting as usual, we start by recording the assumption,

Tableau: Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption.

Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

source 23

Since the main operator is $\to$ source 27, we apply the $\to F$ source 28:

Tableau: Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign, later construction stage two

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one.
Node three, continuing the branch below node two: the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign Then the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign

source 29

The next line to deal with is $2$ source 39. We use $\exists T$ source 40. This requires a new constant; since no constants yet occur, we can pick any one, say, $a$ source 41.

Tableau: Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign, later construction stage three

This source tableau has four formula nodes and one terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.
Node four, continuing the branch below node three: the complete formula the negation of formula A with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign Then the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula the negation of formula A with argument constant a, carrying the true sign

source 42

Now we apply $\neg F$ source 54 to line $3$ source 54:

Tableau: Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign, later construction stage four

This source tableau has five formula nodes and one terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node four, continuing the branch below node three: the complete formula the negation of formula A with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: false-negation tableau rule, applied to line three.

Path 1, open-or-intermediate. the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign Then the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula the negation of formula A with argument constant a, carrying the true sign Then the complete formula for every variable x, formula A with argument variable x, carrying the true sign

source 55

We obtain a closed tableau by applying $\neg T$ source 71 to line $4$ source 72, followed by $\forall T$ source 72 to line $5$ source 72.

Tableau: Closed tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

This source tableau has seven formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption. This node is marked checked.
Node two, continuing the branch below node one: the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one. This node is marked checked.
Node four, continuing the branch below node three: the complete formula the negation of formula A with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: false-negation tableau rule, applied to line three.
Node six, continuing the branch below node five: the complete formula A with argument constant a, carrying the false sign. Printed justification: true-negation tableau rule, applied to line four.
Node seven, continuing the branch below node six: the complete formula A with argument constant a, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line five. The branch closes at this node.

Closed tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

Path 1, closed. the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula for some variable x, the negation of formula A with argument variable x, carrying the true sign Then the complete formula the negation of for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula the negation of formula A with argument constant a, carrying the true sign Then the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula A with argument constant a, carrying the false sign Then the complete formula A with argument constant a, carrying the true sign

source 73

source 13

Example closing a three-assumption quantifier tableau

Let's see how we'd give a tableau for the set $F \exists x C (x, b), T \exists x (A (x) \land B (x)), T \forall x (B (x) \to C (x, b)) .$ source 98 Starting as usual, we start with the assumptions:

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Node one, at the root: the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign. Printed justification: assumption.

Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Path 1, open-or-intermediate. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign

source 104

We should always apply a rule with the eigenvariable condition first; in this case that would be $\exists T$ source 114 to line $2$ source 115. Since the assumptions contain the constant $b$ source 115, we have to use a different one; let's pick $a$ source 116 again.

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage two

Node one, at the root: the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.

Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage two

Path 1, open-or-intermediate. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign Then the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign

source 117

If we now apply $\exists F$ source 129 to line $1$ source 129 or $\forall T$ source 130 to line $3$ source 130, we have to decide which term $t$ source 130 to substitute for $x$ source 131. Since there is no eigenvariable condition for these rules, we can pick any term we like. In some cases we may even have to apply the rule several times with different $t$ source 133s. But as a general rule, it pays to pick one of the terms already occurring in the tableau—in this case, $a$ source 135 and $b$ source 135—and in this case we can guess that $a$ source 136 will be more likely to result in a closed branch.

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage three

This source tableau has six formula nodes and one terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two.
Node five, continuing the branch below node four: the complete formula C with arguments constant a and constant b, carrying the false sign. Printed justification: false-existential quantifier tableau rule, applied to line one.
Node six, continuing the branch below node five: the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line three.

Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage three

Path 1, open-or-intermediate. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign Then the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign Then the complete formula C with arguments constant a and constant b, carrying the false sign Then the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign

source 137

We don't check the signed formulas in lines $1$ source 153 and $3$ source 153, since we may have to use them again. Now apply $\land T$ source 154 to line $4$ source 154:

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage four

This source tableau has eight formula nodes and one terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two. This node is marked checked.
Node five, continuing the branch below node four: the complete formula C with arguments constant a and constant b, carrying the false sign. Printed justification: false-existential quantifier tableau rule, applied to line one.
Node six, continuing the branch below node five: the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line three.
Node seven, continuing the branch below node six: the complete formula A with argument constant a, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line four.
Node eight, continuing the branch below node seven: the complete formula B with argument constant a, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line four.

Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage four

Path 1, open-or-intermediate. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign Then the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign Then the complete formula C with arguments constant a and constant b, carrying the false sign Then the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign Then the complete formula A with argument constant a, carrying the true sign Then the complete formula B with argument constant a, carrying the true sign

source 155

If we now apply $\to T$ source 176 to line $6$ source 176, the tableau closes:

Tableau: Closed tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Node one, at the root: the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line two. This node is marked checked.
Node five, continuing the branch below node four: the complete formula C with arguments constant a and constant b, carrying the false sign. Printed justification: false-existential quantifier tableau rule, applied to line one.
Node six, continuing the branch below node five: the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line three. This node is marked checked.
Node seven, continuing the branch below node six: the complete formula A with argument constant a, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line four.
Node eight, continuing the branch below node seven: the complete formula B with argument constant a, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line four.
Node eight splits into two branches.
Node nine, on the left branch below node eight: the complete formula B with argument constant a, carrying the false sign. Printed justification: true-conditional tableau rule, applied to line six. The branch closes at this node.
Node ten, on the right branch below node eight: the complete formula C with arguments constant a and constant b, carrying the true sign. Printed justification: true-conditional tableau rule, applied to line six. The branch closes at this node.

Closed tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Path 1, closed. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign Then the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign Then the complete formula C with arguments constant a and constant b, carrying the false sign Then the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign Then the complete formula A with argument constant a, carrying the true sign Then the complete formula B with argument constant a, carrying the true sign Then the complete formula B with argument constant a, carrying the false sign
Path 2, closed. the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign Then the complete formula for some variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis, carrying the true sign Then the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula B with argument variable x; and whose consequent is formula C with arguments variable x and constant b, close parenthesis, carrying the true sign Then the complete formula the conjunction of formula A with argument constant a and formula B with argument constant a, carrying the true sign Then the complete formula C with arguments constant a and constant b, carrying the false sign Then the complete formula the conditional whose antecedent is formula B with argument constant a; and whose consequent is formula C with arguments constant a and constant b, carrying the true sign Then the complete formula A with argument constant a, carrying the true sign Then the complete formula B with argument constant a, carrying the true sign Then the complete formula C with arguments constant a and constant b, carrying the true sign

source 177

source 96

Example coordinating eigenvariable and repeatable quantifier rules

We construct a tableau for the set $T \forall x A (x), T \forall x A (x) \to \exists y B (y), T \neg \exists y B (y) .$ source 214 Starting as usual, we write down the assumptions:

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption.

Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Path 1, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign

source 219

We begin by applying the $\neg T$ source 228 rule to line $3$ source 228. A corollary to the rule “always apply rules with eigenvariable conditions first” is “defer applying quantifier rules without eigenvariable conditions until needed.” Also, defer rules that result in a split.

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage two

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node four, continuing the branch below node three: the complete formula for some variable y, formula B with argument variable y, carrying the false sign. Printed justification: true-negation tableau rule, applied to line three.

Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage two

Path 1, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign

source 233

The new line $4$ source 243 requires $\exists F$ source 243, a quantifier rule without the eigenvariable condition. So we defer this in favor of using $\to T$ source 245 on line $2$ source 245.

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage three

This source tableau has six formula nodes and two terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node four, continuing the branch below node three: the complete formula for some variable y, formula B with argument variable y, carrying the false sign. Printed justification: true-negation tableau rule, applied to line three.
Node four splits into two branches.
Node five, on the left branch below node four: the complete formula for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: true-conditional tableau rule, applied to line two.
Node six, on the right branch below node four: the complete formula for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: true-conditional tableau rule, applied to line two.

Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage three

Path 1, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for every variable x, formula A with argument variable x, carrying the false sign
Path 2, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for some variable y, formula B with argument variable y, carrying the true sign

source 246

Both new signed formulas require rules with eigenvariable conditions, so these should be next:

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage four

This source tableau has eight formula nodes and two terminal paths; zero are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node four, continuing the branch below node three: the complete formula for some variable y, formula B with argument variable y, carrying the false sign. Printed justification: true-negation tableau rule, applied to line three.
Node four splits into two branches.
Node five, on the left branch below node four: the complete formula for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: true-conditional tableau rule, applied to line two. This node is marked checked.
Node six, continuing the branch below node five: the complete formula A with argument constant b, carrying the false sign. Printed justification: false-universal quantifier tableau rule, applied to line five.
Node seven, on the right branch below node four: the complete formula for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: true-conditional tableau rule, applied to line two. This node is marked checked.
Node eight, continuing the branch below node seven: the complete formula B with argument constant c, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line five.

Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage four

Path 1, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula A with argument constant b, carrying the false sign
Path 2, open-or-intermediate. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula B with argument constant c, carrying the true sign

source 262

To close the branches, we have to use the signed formulas on lines $1$ source 280 and $3$ source 281. The corresponding rules (true-signed universal-quantifier tableau rule and false-signed existential-quantifier tableau rule) don't have eigenvariable conditions, so we are free to pick whichever terms are suitable. In this case, that's $b$ source 284 and $c$ source 284, respectively.

Tableau: Closed tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node three, continuing the branch below node two: the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: assumption. This node is marked checked.
Node four, continuing the branch below node three: the complete formula for some variable y, formula B with argument variable y, carrying the false sign. Printed justification: true-negation tableau rule, applied to line three.
Node four splits into two branches.
Node five, on the left branch below node four: the complete formula for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: true-conditional tableau rule, applied to line two. This node is marked checked.
Node six, continuing the branch below node five: the complete formula A with argument constant b, carrying the false sign. Printed justification: false-universal quantifier tableau rule, applied to line five.
Node seven, continuing the branch below node six: the complete formula A with argument constant b, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line one. The branch closes at this node.
Node eight, on the right branch below node four: the complete formula for some variable y, formula B with argument variable y, carrying the true sign. Printed justification: true-conditional tableau rule, applied to line two. This node is marked checked.
Node nine, continuing the branch below node eight: the complete formula B with argument constant c, carrying the true sign. Printed justification: true-existential quantifier tableau rule, applied to line five.
Node ten, continuing the branch below node nine: the complete formula B with argument constant c, carrying the false sign. Printed justification: false-existential quantifier tableau rule, applied to line four. The branch closes at this node.

Closed tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Path 1, closed. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula A with argument constant b, carrying the false sign Then the complete formula A with argument constant b, carrying the true sign
Path 2, closed. the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula the negation of for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula for some variable y, formula B with argument variable y, carrying the false sign Then the complete formula for some variable y, formula B with argument variable y, carrying the true sign Then the complete formula B with argument constant c, carrying the true sign Then the complete formula B with argument constant c, carrying the false sign

source 285

source 212

Exercise on six quantified tableau problems

Give closed tableaus of the following:

$F (\forall x A (x) \land \forall y B (y)) \to \forall z (A (z) \land B (z))$ source 320.
$F (\exists x A (x) \lor \exists y B (y)) \to \exists z (A (z) \lor B (z))$ source 322.
$T \forall x (A (x) \to B), F \exists y A (y) \to B$ source 324.
$T \forall x \neg A (x), F \neg \exists x A (x)$ source 326.
$F \neg \exists x A (x) \to \forall x \neg A (x)$ source 328.
$F \neg \exists x \forall y ((A (x, y) \to \neg A (y, y)) \land (\neg A (y, y) \to A (x, y)))$ source 330.

source 317

Exercise on three further quantified tableau problems

Give closed tableaus of the following:

$F \neg \forall x A (x) \to \exists x \neg A (x)$ source 338.
$T (\forall x A (x) \to B), F \exists y (A (y) \to B)$ source 339.
$F \exists x (A (x) \to \forall y A (y))$ source 340.

source 335

Proof-Theoretic Notions

Definition of tableau theoremhood

Theorems

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

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

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

Reflexivity

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 formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, 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.

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

Path 1, closed. the complete formula A, carrying the false sign Then the complete formula A, carrying the true sign

source 73

is closed.

End of proof.

Proposition: monotonicity of tableau derivability

Monotonicity

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

Transitivity

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

Display formula: Two closed-tableau assumption sets used for transitivity

The first displayed assumption set contains B carrying the false sign, A carrying the true sign, and C sub one through C sub n carrying the true sign; the source says this set has a closed tableau. The source next assumes A is tableau-derivable from Gamma and literally prints that D sub m is a subset of Gamma. That relation is malformed because D sub m is one formula. The disclosed reader interpretation is that the finite set containing D sub one through D sub m is a subset of Gamma. Under that interpretation, the second displayed assumption set contains A carrying the false sign and D sub one through D sub m carrying the true sign, and it has a closed tableau.

\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 101

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 rule 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

Prove the proposition characterizing inconsistency by derivability of every sentence

source 151

Proposition: compactness of tableau derivability and consistency

Compactness

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 25 such that

Display formula: Paired closed-tableau assumptions in the combination proof

The first displayed tableau row contains A carrying the false sign and B sub one through B sub n carrying the true sign. The second displayed tableau row contains A carrying the true sign and C sub one through C sub m carrying the true sign. The bound source correction discloses that the preceding definition of Gamma sub one ends its C-family at C sub n, while this second row ends it at C sub m; both frozen indices are preserved.

\begin{matrix} {F A, & T B_{1}, \dots, T B_{n}} \\ {T A, & T C_{1}, \dots, T C_{m}} \end{matrix}

source 27

have closed tableaus. Using the cut rule 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-signed negation 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-signed negation 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

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 true-signed negation tableau rule applied to false-signed A 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 95. 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

Display formula: Two closed-tableau rows for the cut construction

The first displayed closed-tableau row contains A carrying the true sign and B sub one through B sub n carrying the true sign. The second displayed closed-tableau row contains not A carrying the true sign and C sub one through C sub m carrying the true sign.

\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 rule rule. This yields two branches, one starting with $T A$ source 119, the other with $F A$ source 120.

On the 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 rule 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 138, we can applying $\neg F$ source 138 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 rule 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 formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, 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 the conjunction of formula A and 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: true-conjunction tableau rule, applied to line two.
4. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line two. The branch closes at this node.
5. Source correction disclosure: 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.
Closed tableau beginning with the complete formula A, carrying the false sign, later construction stage two
1. Path 1, closed. the complete formula A, carrying the false sign Then the complete formula the conjunction of formula A and formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign
source 40
Tableau: Closed tableau beginning with the complete formula B, carrying the false sign
This source tableau has four formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, 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 the conjunction of formula A and 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: true-conjunction tableau rule, applied to line two.
4. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule, applied to line two. The branch closes at this node.
5. Source correction disclosure: 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.
Closed tableau beginning with the complete formula B, carrying the false sign
1. Path 1, closed. the complete formula B, carrying the false sign Then the complete formula the conjunction of formula A and formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign
source 50
Here is a closed tableau for ${T A, T B, F A \land B}$ source 60:
Tableau: Closed tableau beginning with the complete formula the conjunction of formula A and formula B, carrying the false sign
This source tableau has five formula nodes and two terminal paths; two are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the conjunction of formula A and formula 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, applied to line 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, applied to line one. The branch closes at this node.
Closed tableau beginning with the complete formula the conjunction of formula A and formula B, carrying the false sign
1. Path 1, closed. the complete formula the conjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign Then the complete formula A, carrying the false sign
2. Path 2, closed. the complete formula the conjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign Then the complete formula B, carrying the false sign
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 the disjunction of formula A and formula B, carrying the true sign
This source tableau has seven formula nodes and two terminal paths; two are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the disjunction of formula A and formula B, carrying the true sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula the negation of formula A, carrying the true sign. Printed justification: assumption.
3. Node three, continuing the branch below node two: the complete formula the negation of formula 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, applied to line two.
5. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: true-negation tableau rule, applied to line 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, applied to line 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, applied to line one. The branch closes at this node.
Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the true sign
1. Path 1, closed. the complete formula the disjunction of formula A and formula B, carrying the true sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula the negation of formula B, carrying the true sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign Then the complete formula A, carrying the true sign
2. Path 2, closed. the complete formula the disjunction of formula A and formula B, carrying the true sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula the negation of formula B, carrying the true sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign Then the complete formula B, carrying the true sign
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 the disjunction of formula A and formula B, carrying the false sign
This source tableau has four formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the disjunction of formula A and formula 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, applied to line one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line one. The branch closes at this node.
5. Source correction disclosure: 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.
Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the false sign
1. Path 1, closed. the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula A, carrying the true sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
source 103
Tableau: Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the false sign, later construction stage two
This source tableau has four formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the disjunction of formula A and formula 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, applied to line one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule, applied to line one. The branch closes at this node.
5. Source correction disclosure: 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.
Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the false sign, later construction stage two
1. Path 1, closed. the complete formula the disjunction of formula A and formula B, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula A, carrying the false sign Then the complete formula B, carrying the false sign
source 113

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 formula nodes and two terminal paths; two are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, 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 the conditional whose antecedent is formula A; and whose consequent is 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: 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, applied to line 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, applied to line two. The branch closes at this node.
Closed tableau beginning with the complete formula B, carrying the false sign, later construction stage two
1. Path 1, closed. the complete formula B, carrying the false sign Then the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula A, carrying the false sign
2. Path 2, closed. the complete formula B, carrying the false sign Then the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the true sign
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 the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign
This source tableau has five formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign. Printed justification: assumption.
2. Node two, continuing the branch below node one: the complete formula the negation of formula 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, applied to line one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one.
5. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule, applied to line two. The branch closes at this node.
Closed tableau beginning with the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign
1. Path 1, closed. the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign Then the complete formula the negation of formula A, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign Then the complete formula A, carrying the false sign
source 151
Tableau: Closed tableau beginning with the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign, later construction stage two
This source tableau has four formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.
1. Node one, at the root: the complete formula the conditional whose antecedent is formula A; and whose consequent is formula 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, applied to line one.
4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule, applied to line one. The branch closes at this node.
Closed tableau beginning with the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign, later construction stage two
1. Path 1, closed. the complete formula the conditional whose antecedent is formula A; and whose consequent is formula B, carrying the false sign Then the complete formula B, carrying the true sign Then the complete formula A, carrying the true sign Then the complete formula B, carrying the false sign
source 162

End of proof.

derivability and the Quantifiers

Theorem: strong generalization for tableau derivability

If $c$ source 18 is a constant not occurring in $Γ$ source 19 or $A (x)$ source 19 and $Γ ⊢ A (c)$ source 19, then $Γ ⊢ \forall x A (x)$ source 19.

source 17

Proof

Suppose $Γ ⊢ A (c)$ source 24, i.e., there are $B_{1}$ source 24, …, $B_{n} \in Γ$ source 24 and a closed tableau for

Display formula: The two assumption sets in the strong-generalization proof

The first displayed assumption set contains A of c carrying the false sign and B sub one through B sub n carrying the true sign; the proof assumes it has a closed tableau. The required second assumption set replaces false-signed A of c by the universal formula every x satisfying A of x carrying the false sign, while retaining true-signed B sub one through B sub n. The surrounding proof inserts false-signed A of c by the false-universal rule, whose eigenvariable condition is met because c occurs neither in the retained assumptions nor in the universal formula.

\begin{matrix} {F A (c), & T B_{1}, \dots, T B_{n}} . \\ We have to show that there is also a closed tableau for \\ {F \forall x A (x), & T B_{1}, \dots, T B_{n}} . \end{matrix}

source 26

Take the closed tableau and replace the first assumption with $F \forall x A (x)$ source 34, and insert $F A (c)$ source 35 after the assumptions.

Tableau: Schematic tableau beginning with the complete formula A with argument constant c, carrying the false sign

This schematic source tableau has four explicit formula nodes, three omitted-subtree placeholders, and zero explicitly closed terminal paths. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula A with argument constant c, carrying the false sign. Printed justification: no printed justification.
Node two, continuing the branch below node one: the complete formula B sub one, carrying the true sign. Printed justification: no printed justification.
Node three, continuing the branch below node two: vertical dots indicating omitted intermediate assumptions. Printed justification: no printed justification.
Node four, continuing the branch below node three: the complete formula B sub n, carrying the true sign. Printed justification: no printed justification.
Node four splits into three branches.
On branch one below node four: the source prints an empty bracket as an omitted-subtree placeholder.
On branch two below node four: the source prints an empty bracket as an omitted-subtree placeholder.
On branch three below node four: the source prints an empty bracket as an omitted-subtree placeholder.

Schematic tableau beginning with the complete formula A with argument constant c, carrying the false sign

Path 1, omitted-subtree. the complete formula A with argument constant c, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then Source marks an omitted subtree.
Path 2, omitted-subtree. the complete formula A with argument constant c, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then Source marks an omitted subtree.
Path 3, omitted-subtree. the complete formula A with argument constant c, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then Source marks an omitted subtree.

source 37

Tableau: Schematic tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the false sign

This schematic source tableau has five explicit formula nodes, three omitted-subtree placeholders, and zero explicitly closed terminal paths. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for every variable x, formula A with argument variable x, carrying the false sign. Printed justification: no printed justification.
Node two, continuing the branch below node one: the complete formula B sub one, carrying the true sign. Printed justification: no printed justification.
Node three, continuing the branch below node two: vertical dots indicating omitted intermediate assumptions. Printed justification: no printed justification.
Node four, continuing the branch below node three: the complete formula B sub n, carrying the true sign. Printed justification: no printed justification.
Node five, continuing the branch below node four: the complete formula A with argument constant c, carrying the false sign. Printed justification: no printed justification.
Node five splits into three branches.
On branch one below node five: the source prints an empty bracket as an omitted-subtree placeholder.
On branch two below node five: the source prints an empty bracket as an omitted-subtree placeholder.
On branch three below node five: the source prints an empty bracket as an omitted-subtree placeholder.

Schematic tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the false sign

Path 1, omitted-subtree. the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then the complete formula A with argument constant c, carrying the false sign Then Source marks an omitted subtree.
Path 2, omitted-subtree. the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then the complete formula A with argument constant c, carrying the false sign Then Source marks an omitted subtree.
Path 3, omitted-subtree. the complete formula for every variable x, formula A with argument variable x, carrying the false sign Then the complete formula B sub one, carrying the true sign Then vertical dots indicating omitted intermediate assumptions Then the complete formula B sub n, carrying the true sign Then the complete formula A with argument constant c, carrying the false sign Then Source marks an omitted subtree.

source 44

The tableau is still closed, since all sentences available as assumptions before are still available at the top of the tableau. The inserted line is the result of a correct application of $\forall F$ source 56, since the constant $c$ source 56 does not occur in $B_{1}$ source 57, …, $B_{n}$ source 57 or $\forall x A (x)$ source 57, i.e., it does not occur above the inserted line in the new tableau.

End of proof.

Proposition: tableau derivability rules for quantifiers

$A (t) ⊢ \exists x A (x)$ source 64. $\forall x A (x) ⊢ A (t)$ source 65.

source 61

Proof

A closed tableau for $F \exists x A (x), T A (t)$ source 72 is:

Tableau: Closed tableau beginning with the complete formula for some variable x, formula A with argument variable x, carrying the false sign

This source tableau has three formula nodes and one terminal paths; one are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, layout-only move, omitted-subtree marker, and closure marker in deterministic preorder.

Node one, at the root: the complete formula for some variable x, formula A with argument variable x, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula A with argument term t, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula A with argument term t, carrying the false sign. Printed justification: false-existential quantifier tableau rule, applied to line one. The branch closes at this node.

Closed tableau beginning with the complete formula for some variable x, formula A with argument variable x, carrying the false sign

Path 1, closed. the complete formula for some variable x, formula A with argument variable x, carrying the false sign Then the complete formula A with argument term t, carrying the true sign Then the complete formula A with argument term t, carrying the false sign

source 73

A closed tableau for $F A (t), T \forall x A (x),$ source 79 is:

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

Node one, at the root: the complete formula A with argument term t, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula for every variable x, formula A with argument variable x, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula A with argument term t, carrying the true sign. Printed justification: true-universal quantifier tableau rule, applied to line two. The branch closes at this node.

Closed tableau beginning with the complete formula A with argument term t, carrying the false sign

Path 1, closed. the complete formula A with argument term t, carrying the false sign Then the complete formula for every variable x, formula A with argument variable x, carrying the true sign Then the complete formula A with argument term t, carrying the true sign

source 80

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 valid;
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 structure $M$ source 42 satisfies a signed formula $T A$ source 43 iff $M ⊨ A$ source 44, and it satisfies $F A$ source 45 iff $M ⊭ A$ source 46. $M$ 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 structure that satisfies it, and unsatisfiable otherwise.

source 41

Theorem: a closed tableau has no satisfying valuation

Soundness

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 $M ⊨ Γ$ source 96. In particular, $M ⊨ \neg B$ source 97. Thus, $M ⊭ B$ source 98, i.e., $M$ 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 $M ⊨ Γ$ source 107, in particular $M ⊨ B \land C$ source 108. Then $M ⊨ B$ source 109 and $M ⊨ C$ source 110. This means that $M$ 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 $M ⊨ Γ$ source 119, in particular $M ⊭ B \to C$ source 120. Then $M ⊨ B$ source 121 and $M ⊭ C$ source 122. This means that $M$ source 123 satisfies both $T B$ source 124 and $F C$ source 124.
The branch is expanded by applying $\forall T$ source 127 to $T \forall x B (x) \in Γ$ source 128: This results in a new signed formula $T A (t)$ source 129 on the branch. Suppose $M ⊨ Γ$ source 130, in particular, $M ⊨ \forall x A (x)$ source 131. By the proposition relating substitution to the semantic value of terms, $M ⊨ A (t)$ source 132. Consequently, $M$ source 133 satisfies $T A (t)$ source 133.
The branch is expanded by applying $\forall F$ source 135 to $F \forall x B (x) \in Γ$ source 136: This results in a new signed formula $F A (a)$ source 137 where $a$ source 137 is a constant not occurring in $Γ$ source 138. Since $Γ$ source 138 is satisfiable, there is a $M$ source 139 such that $M ⊨ Γ$ source 139, in particular $M ⊭ \forall x B (x)$ source 140. We have to show that $Γ \cup {F A (a)}$ source 141 is satisfiable. To do this, we define a suitable $M'$ source 142 as follows.
By the proposition giving the satisfaction clauses for quantifiers, $M ⊭ \forall x B (x)$ source 144 iff for some $s$ source 145, $M, s ⊭ B (x)$ source 145. Now let $M'$ source 145 be just like $M$ source 146, except $a^{M'} = s (x)$ source 146. By the corollary that sentence truth is independent of variable assignment, for any $T C \in Γ$ source 148, $M' ⊨ C$ source 148, and for any $F C \in Γ$ source 149, $M' ⊭ C$ source 149, since $a$ source 149 does not occur in $Γ$ source 150.
By the proposition on extensionality of first-order evaluation, $M', s ⊭ A (x)$ source 152. By the proposition on assignment extensionality for formulas, $M', s ⊭ A (a)$ source 153. Since $A (a)$ source 154 is a sentence, by the proposition linking satisfaction of a sentence with truth in a structure, $M' ⊭ A (a)$ source 155, i.e., $M'$ source 156 satisfies $F A (a)$ source 156.
The branch is expanded by applying $\exists T$ source 157 to $T \exists x B (x) \in Γ$ source 158: Exercise.
The branch is expanded by applying $\exists F$ source 159 to $F \exists x B (x) \in Γ$ source 160: Exercise.

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 $M ⊨ Γ$ source 168, in particular $M ⊭ B \land C$ source 169. Then $M ⊭ B$ source 170 or $M ⊭ C$ source 171. In the former case, $M$ source 172 satisfies $F B$ source 173, i.e., $M$ source 173 satisfies the formulas on the left branch. In the latter, $M$ source 175 satisfies $F C$ source 176, i.e., $M$ 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 rule: This results in two branches, one containing $T B$ source 183, the other containing $F B$ source 184. Since $M ⊨ Γ$ source 184 and either $M ⊨ B$ source 185 or $M ⊭ B$ source 186, $M$ source 187 satisfies either the left or the right branch.

End of proof.

Exercise completing first-order tableau soundness

Complete the proof of the first-order tableau soundness theorem.

source 193

Corollary: tableau theorems are valid

If $⊢ A$ source 206 then $A$ source 206 is valid.

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 the first-order tableau soundness theorem, every structure $M$ source 219 either makes some $B_{i}$ source 220 false or makes $A$ source 220 true. Hence, if $M ⊨ Γ$ source 221 then also $M ⊨ 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 the first-order tableau soundness theorem, there is no $M$ source 235 such that $M ⊨ B_{i}$ source 236 for all $i = 1$ source 236, …, $n$ source 236. But then $Γ$ source 237 is not satisfiable.

End of proof.

tableau with identity

Tableaus with identity require additional inference rules. The rules for $=$ source 14 are ( $t$ source 14, $t_{1}$ source 14, and $t_{2}$ source 14 are closed terms):

Definition of the identity tableau rules

Proof diagram: Identity-reflexivity tableau rule

This rule has no formula premise at the current branch node. Choose a closed term t and apply identity reflexivity. Continue the branch with t equals t carrying the true sign.

This rule has no formula premise at the current branch node.
Choose a closed term t and apply identity reflexivity.
Continue the branch with t equals t carrying the true sign.

Additional native source formulas in object order

$=$ source 18

source 20

Proof diagram: True-identity substitution tableau rule

First premise: t one equals t two, carrying the true sign. Second premise: A of t one, carrying the true sign, on the same branch. Apply the true-identity tableau rule and continue with A of t two carrying the true sign.

First premise: t one equals t two, carrying the true sign.
Second premise: A of t one, carrying the true sign, on the same branch.
Apply the true-identity tableau rule and continue with A of t two carrying the true sign.

Additional native source formulas in object order

$= T$ source 25

source 27

Proof diagram: False-identity substitution tableau rule

First premise: t one equals t two, carrying the true sign. Second premise: A of t one, carrying the false sign, on the same branch. Apply the false-identity tableau rule and continue with A of t two carrying the false sign.

First premise: t one equals t two, carrying the true sign.
Second premise: A of t one, carrying the false sign, on the same branch.
Apply the false-identity tableau rule and continue with A of t two carrying the false sign.

Additional native source formulas in object order

$= F$ source 32

source 34

source 16

Note that in contrast to all the other rules, $= T$ source 36 and $= F$ source 37 require that two signed formulas already appear on the branch, namely both $T t_{1} = t_{2}$ source 38 and $S A (t_{1})$ source 39.

Examples of substitutability, symmetry, and transitivity of identity

If $s$ source 42 and $t$ source 42 are closed terms, then $s = t, A (s) ⊢ A (t)$ source 42:

Tableau: Closed tableau beginning with the complete formula A with argument term t, carrying the false sign, later construction stage two

Node one, at the root: the complete formula A with argument term t, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula lowercase s is identical to term t, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula A with argument lowercase s, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula A with argument term t, carrying the true sign. Printed justification: true-identity tableau rule, applied to lines two, then three. The branch closes at this node.

Closed tableau beginning with the complete formula A with argument term t, carrying the false sign, later construction stage two

Path 1, closed. the complete formula A with argument term t, carrying the false sign Then the complete formula lowercase s is identical to term t, carrying the true sign Then the complete formula A with argument lowercase s, carrying the true sign Then the complete formula A with argument term t, carrying the true sign

source 44

This may be familiar as the principle of substitutability of identicals, or Leibniz' Law.

Tableaus prove that $=$ source 56 is symmetric, i.e., that $s_{1} = s_{2} ⊢ s_{2} = s_{1}$ source 56:

Tableau: Closed tableau beginning with the complete formula term s sub two is identical to term s sub one, carrying the false sign

Node one, at the root: the complete formula term s sub two is identical to term s sub one, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula term s sub one is identical to term s sub two, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula term s sub one is identical to term s sub one, carrying the true sign. Printed justification: identity-reflexivity rule.
Node four, continuing the branch below node three: the complete formula term s sub two is identical to term s sub one, carrying the true sign. Printed justification: true-identity tableau rule, applied to lines two, then three. The branch closes at this node.

Closed tableau beginning with the complete formula term s sub two is identical to term s sub one, carrying the false sign

Path 1, closed. the complete formula term s sub two is identical to term s sub one, carrying the false sign Then the complete formula term s sub one is identical to term s sub two, carrying the true sign Then the complete formula term s sub one is identical to term s sub one, carrying the true sign Then the complete formula term s sub two is identical to term s sub one, carrying the true sign

Additional native source formulas in object order

$=$ source 61

source 58

Here, line $2$ source 67 is the first prerequisite formula $T s_{1} = s_{2}$ source 68 of $= T$ source 68. Line $3$ source 69 is the second one, of the form $T A (s_{2})$ source 69—think of $A (x)$ source 70 as $x = s_{1}$ source 71, then $A (s_{1})$ source 71 is $s_{1} = s_{1}$ source 71 and $A (s_{2})$ source 71 is $s_{2} = s_{1}$ source 71.

They also prove that $=$ source 73 is transitive, i.e., that $s_{1} = s_{2}, s_{2} = s_{3} ⊢ s_{1} = s_{3}$ source 73:

Tableau: Closed tableau beginning with the complete formula term s sub one is identical to term s sub three, carrying the false sign

Node one, at the root: the complete formula term s sub one is identical to term s sub three, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula term s sub one is identical to term s sub two, carrying the true sign. Printed justification: assumption.
Node three, continuing the branch below node two: the complete formula term s sub two is identical to term s sub three, carrying the true sign. Printed justification: assumption.
Node four, continuing the branch below node three: the complete formula term s sub one is identical to term s sub three, carrying the true sign. Printed justification: true-identity tableau rule, applied to lines three, then two. The branch closes at this node.

Closed tableau beginning with the complete formula term s sub one is identical to term s sub three, carrying the false sign

Path 1, closed. the complete formula term s sub one is identical to term s sub three, carrying the false sign Then the complete formula term s sub one is identical to term s sub two, carrying the true sign Then the complete formula term s sub two is identical to term s sub three, carrying the true sign Then the complete formula term s sub one is identical to term s sub three, carrying the true sign

source 75

In this tableau, the first prerequisite formula of $= T$ source 85 is line $3$ source 85, $T s_{2} = s_{3}$ source 85 ( $s_{2}$ source 86 plays the role of $t_{1}$ source 86, and $s_{3}$ source 86 the role of $t_{2}$ source 86). The second prerequisite, of the form $T A (s_{2})$ source 87 is line $2$ source 87. Here, think of $A (x)$ source 88 as $s_{1} = x$ source 88; that makes $A (s_{2})$ source 88 into $t_{1} = t_{2}$ source 89 (i.e., line $2$ source 89) and $A (s_{3})$ source 89 into the formula $s_{1} = s_{3}$ source 90 in the conclusion.

source 41

Exercise on quantified identity tableaux

Give closed tableaus for the following:

$F \forall x \forall y ((x = y \land A (x)) \to A (y))$ source 96
$F \exists x (A (x) \land \forall y (A (y) \to y = x))$ source 98, $T \exists x A (x) \land \forall y \forall z ((A (y) \land A (z)) \to y = z)$ source 100

source 93

Soundness with identity

Proposition: soundness of the identity tableau rules

Tableaus with rules for identity are sound: no closed tableau is satisfiable.

source 13

Proof

We just have to show as before that if a tableau has a satisfiable branch, the branch resulting from applying one of the rules for $=$ source 20 to it is also satisfiable. Let $Γ$ source 21 be the set of signed formulas on the branch, and let $M$ source 22 be a structure satisfying $Γ$ source 23.

Suppose the branch is expanded using $=$ source 25, i.e., by adding the signed formula $T t = t$ source 26. Trivially, $M ⊨ t = t$ source 27, so $M$ source 27 also satisfies $Γ \cup {T t = t}$ source 27.

If the branch is expanded using $= T$ source 30, we add a signed formula $S A (t_{2})$ source 31, but $Γ$ source 31 contains both $T t_{1} = t_{2}$ source 32 and $T A (t_{1})$ source 32. Thus we have $M ⊨ t_{1} = t_{2}$ source 33 and $M ⊨ A (t_{1})$ source 33. Let $s$ source 33 be a variable assignment with $s (x) = ⟦ t_{1} ⟧_{M}$ source 34. By the proposition linking satisfaction of a sentence with truth in a structure, $M, s ⊨ A (t_{1})$ source 35. Since $s \equiv_{x} s$ source 36, by the proposition on assignment extensionality for formulas, $M, s ⊨ A (x)$ source 37. since $M ⊨ t_{1} = t_{2}$ source 37, we have $⟦ t_{1} ⟧_{M} = ⟦ t_{2} ⟧_{M}$ source 38, and hence $s (x) = ⟦ t_{2} ⟧_{M}$ source 38. By applying the proposition on assignment extensionality for formulas again, we also have $M, s ⊨ A (t_{2})$ source 40. By the proposition linking satisfaction of a sentence with truth in a structure, $M ⊨ A (t_{2})$ source 41. The case of $= F$ source 41 is treated similarly.

End of proof.

Reading preferences

How to use Read

Rules and tableau

Definition of a signed formula

Propositional Rules

Rules for ¬source 15

Definition of the negation tableau rules

Proof diagram: True-negation tableau rule

Proof diagram: False-negation tableau rule

Rules for ∧source 29

Definition of the conjunction tableau rules

Proof diagram: True-conjunction tableau rule

Proof diagram: False-conjunction branching tableau rule

Rules for ∨source 45

Definition of the disjunction tableau rules

Proof diagram: True-disjunction branching tableau rule

Proof diagram: False-disjunction tableau rule

Rules for →source 61

Definition of the conditional tableau rules

Proof diagram: True-conditional branching tableau rule

Proof diagram: False-conditional tableau rule

The Cut Rule

Definition of the cut tableau rule

Proof diagram: Cut branching rule

Quantifier Rules

Rules for ∀source 13

Definition of the universal-quantifier tableau rules

Proof diagram: True-universal tableau rule

Proof diagram: False-universal tableau rule

Rules for ∃source 35

Definition of the existential-quantifier tableau rules

Proof diagram: True-existential tableau rule

Proof diagram: False-existential tableau rule

tableau

Definition of a tableau derivation

Example of extending a tableau derivation

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

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

Tableau: Closed tableau beginning with the complete formula the conjunction of formula A and the negation of formula 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 the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Tableau: Open or intermediate tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign, later construction stage two

Tableau: Closed tableau beginning with the complete formula the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula A, carrying the false sign

Example proving a nested conditional by tableau

Example closing a branching tableau

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

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

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

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

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

Tableau: Closed tableau beginning with the complete formula the disjunction of formula A and open parenthesis, the conjunction of formula B and formula 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

tableau with Quantifiers

Example closing a quantified conditional tableau

Tableau: Closed tableau beginning with the complete formula the conditional whose antecedent is for some variable x, the negation of formula A with argument variable x; and whose consequent is the negation of for every variable x, formula A with argument variable x, carrying the false sign

Example closing a three-assumption quantifier tableau

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage two

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage three

Tableau: Open or intermediate tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign, later construction stage four

Tableau: Closed tableau beginning with the complete formula for some variable x, formula C with arguments variable x and constant b, carrying the false sign

Example coordinating eigenvariable and repeatable quantifier rules

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage two

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage three

Tableau: Open or intermediate tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign, later construction stage four

Tableau: Closed tableau beginning with the complete formula for every variable x, formula A with argument variable x, carrying the true sign

Exercise on six quantified tableau problems

Exercise on three further quantified tableau problems

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

Rules for $\neg$ source 15

Rules for $\land$ source 29

Rules for $\lor$ source 45

Rules for $\to$ source 61

Rules for $\forall$ source 13

Rules for $\exists$ source 35