Tableaux — Explore equations

Reading preferences

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

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.

Equation, formal-object, proof, and reference guide

2 occurrences

Expression 4

Inline MathML variant

s

Block MathML variant

s

Expression 29

Inline MathML variant

T s_{1} = s_{2}

Block MathML variant

T s_{1} = s_{2}

Conventional reading: the complete formula term s sub one is identical to term s sub two, carrying the true sign

Meaning here: The expression read 'the complete formula term s sub one is identical to term s sub two, carrying the true sign' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: identity.tex, line 68, column 13

Expression 30

Inline MathML variant

n + 1

Block MathML variant

n + 1

Conventional reading: n plus one

Meaning here: n plus one is the line number printed by the frozen source; the bound reader correction explains why the derived line is n plus two.

1 occurrence

Occurrence 1: provability-consistency.tex, line 95, column 8

Expression 31

Inline MathML variant

\land F

Block MathML variant

\land F

Occurrence 1: provability-propositional.tex, line 77, column 9

Expression 44

Inline MathML variant

F \forall x \forall y ((x = y \land A (x)) \to A (y))

Block MathML variant

F \forall x \forall y ((x = y \land A (x)) \to A (y))

Conventional reading: the complete formula for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis, carrying the false sign

Meaning here: The expression read 'the complete formula for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis, carrying the false sign' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: identity.tex, line 96, column 7

Expression 45

Inline MathML variant

\exists x \neg A (x) \to \neg \forall x A (x)

Block MathML variant

\exists x \neg A (x) \to \neg \forall x A (x)

Conventional reading: 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

Meaning here: The expression read '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' preserves every bound variable, quantifier order, connective, and scope.

1 occurrence

Occurrence 1: proving-things-quant.tex, line 21, column 1

Expression 46

Inline MathML variant

B_{n} \in Γ

Block MathML variant

B_{n} \in Γ

Conventional reading: B sub n belongs to Gamma

Meaning here: B sub n belongs to Gamma. This states membership in the displayed premise set.

5 occurrences

Expression 47

Inline MathML variant

F \neg A

Block MathML variant

F \neg A

Occurrence 1: quantifier-rules.tex, line 68, column 4

Expression 61

Inline MathML variant

{F A \lor B, T A}

Block MathML variant

{F A \lor B, T A}

Conventional reading: the set containing the complete formula A or B, carrying the false sign comma the complete formula A, carrying the true sign

Meaning here: The set containing the complete formula A or B, carrying the false sign comma the complete formula A, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-propositional.tex, line 100, column 14

Expression 62

Inline MathML variant

b

Block MathML variant

b

Meaning here: The expression read 'structure M does not satisfy formula A' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness.tex, line 46, column 1

Expression 74

Inline MathML variant

Γ \cup {F A (a)}

Block MathML variant

Γ \cup {F A (a)}

Conventional reading: the union of Gamma, and the set containing the complete formula A with argument constant a, carrying the false sign

Meaning here: The expression read 'the union of Gamma, and the set containing the complete formula A with argument constant a, carrying the false sign' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: soundness.tex, line 141, column 3

Occurrence 1: soundness-identity.tex, line 34, column 26

Expression 93

Inline MathML variant

T B \to C \in Γ

Block MathML variant

T B \to C \in Γ

Conventional reading: the complete formula B implies C, carrying the true sign belongs to Gamma

Meaning here: The complete formula B implies C, carrying the true sign belongs to Gamma. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: soundness.tex, line 181, column 3

Expression 94

Inline MathML variant

M ⊨ \neg B

Block MathML variant

M ⊨ \neg B

Conventional reading: structure M satisfies the negation of formula B

Meaning here: The expression read 'structure M satisfies the negation of formula B' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness.tex, line 97, column 3

Expression 95

Inline MathML variant

T

Block MathML variant

T

Meaning here: False-conditional tableau rule. This names the exact truth-sign and connective expansion rule used by a propositional tableau.

6 occurrences

Expression 100

Inline MathML variant

t_{2}

Block MathML variant

t_{2}

Expression 120

Inline MathML variant

F B \land C \in Γ

Block MathML variant

F B \land C \in Γ

Conventional reading: the complete formula B and C, carrying the false sign belongs to Gamma

Meaning here: The complete formula B and C, carrying the false sign belongs to Gamma. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: soundness.tex, line 165, column 3

Expression 121

Inline MathML variant

{F B, T A \land B}

Block MathML variant

{F B, T A \land B}

Conventional reading: the set containing the complete formula B, carrying the false sign comma the complete formula A and B, carrying the true sign

Meaning here: The set containing the complete formula B, carrying the false sign comma the complete formula A and B, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-propositional.tex, line 38, column 5

Expression 122

Inline MathML variant

A_{1}, \dots, A_{n} ⊢ B

Block MathML variant

A_{1}, \dots, A_{n} ⊢ B

Conventional reading: B is tableau-derivable from premises A sub one through A sub n

Meaning here: B is tableau-derivable from premises A sub one through A sub n. Derivability here is defined by existence of the corresponding closed tableau, not by the sequent-calculus or natural-deduction rules used in other chapters.

1 occurrence

Occurrence 1: proof-theoretic-notions.tex, line 136, column 64

Expression 123

Inline MathML variant

{T A \lor B, T \neg A, T \neg B}

Block MathML variant

{T A \lor B, T \neg A, T \neg B}

Conventional reading: the set containing the complete formula A or B, carrying the true sign comma the complete formula not A, carrying the true sign comma the complete formula not B, carrying the true sign

Meaning here: The set containing the complete formula A or B, carrying the true sign comma the complete formula not A, carrying the true sign comma the complete formula not B, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-propositional.tex, line 84, column 41

Expression 124

Inline MathML variant

M ⊨ \forall x A (x)

Block MathML variant

M ⊨ \forall x A (x)

Conventional reading: structure M satisfies for every variable x, formula A with argument variable x

Meaning here: The expression read 'structure M satisfies for every variable x, formula A with argument variable x' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness.tex, line 131, column 3

Expression 125

Inline MathML variant

T A ∣ T B

Block MathML variant

T A ∣ T B

Conventional reading: the complete formula A, carrying the true sign separate branch the complete formula B, carrying the true sign

Meaning here: The complete formula A, carrying the true sign separate branch the complete formula B, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: propositional-rules.tex, line 50, column 12

Expression 126

Inline MathML variant

s_{3}

Block MathML variant

s_{3}

Conventional reading: term s sub three

Meaning here: The expression read 'term s sub three' has the exact index, term, formula, sign, or structure role fixed by its source occurrence.

1 occurrence

Occurrence 1: identity.tex, line 86, column 37

Expression 127

Inline MathML variant

F (A \to B) \lor (B \to C)

Block MathML variant

F (A \to B) \lor (B \to C)

Conventional reading: the complete formula open parenthesis A implies B close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign

Meaning here: The complete formula open parenthesis A implies B close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: proving-things.tex, line 456, column 7

Expression 128

Inline MathML variant

B ⊢ A \to B

Block MathML variant

B ⊢ A \to B

Conventional reading: the conditional from A to B is tableau-derivable from premise B

Meaning here: The conditional from A to B is tableau-derivable from premise B. Derivability here is defined by existence of the corresponding closed tableau, not by the sequent-calculus or natural-deduction rules used in other chapters.

1 occurrence

Occurrence 1: provability-propositional.tex, line 130, column 44

Expression 129

Inline MathML variant

T B \land C

Block MathML variant

T B \land C

Conventional reading: the complete formula B and C, carrying the true sign

Meaning here: The complete formula B and C, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: proving-things.tex, line 301, column 31

Expression 130

Inline MathML variant

{A}

Block MathML variant

{A}

Conventional reading: the set containing A

Meaning here: This is the singleton premise set whose sole member is formula A.

1 occurrence

Occurrence 1: proof-theoretic-notions.tex, line 72, column 21

Occurrence 1: proving-things-quant.tex, line 339, column 7

Expression 134

Inline MathML variant

\neg T

Block MathML variant

\neg T

1 occurrence

Occurrence 1: proof-theoretic-notions.tex, line 57, column 1

Expression 138

Inline MathML variant

s \equiv_{x} s

Block MathML variant

s \equiv_{x} s

Conventional reading: variable assignment lowercase s agrees with variable assignment lowercase s except possibly at variable x

Meaning here: The expression read 'variable assignment lowercase s agrees with variable assignment lowercase s except possibly at variable x' denotes the exact term value, symbol interpretation, or assignment relation printed by the source.

1 occurrence

Occurrence 1: soundness-identity.tex, line 36, column 1

Expression 139

Inline MathML variant

T C

Block MathML variant

T C

2 occurrences

Expression 157

Inline MathML variant

\neg A \in Γ

Block MathML variant

\neg A \in Γ

Conventional reading: not A belongs to Gamma

Meaning here: Not A belongs to Gamma. This states membership in the displayed premise set.

2 occurrences

Expression 158

Inline MathML variant

M ⊨ A (t_{1})

Block MathML variant

M ⊨ A (t_{1})

Conventional reading: structure M satisfies formula A with argument term t sub one

Meaning here: The expression read 'structure M satisfies formula A with argument term t sub one' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness-identity.tex, line 33, column 38

Expression 159

Inline MathML variant

{B_{1}, \dots, B_{n}} \subseteq Γ

Block MathML variant

{B_{1}, \dots, B_{n}} \subseteq Γ

Conventional reading: the set containing B sub one comma through the omitted intermediate entries comma B sub n is a subset of Gamma

Meaning here: The set containing B sub one comma through the omitted intermediate entries comma B sub n is a subset of Gamma. This states the displayed finite-set inclusion.

2 occurrences

Expression 160

Inline MathML variant

T (A \to B) \to A, F A

Block MathML variant

T (A \to B) \to A, F A

Conventional reading: the complete formula open parenthesis A implies B close parenthesis implies A, carrying the true sign comma the complete formula A, carrying the false sign

Meaning here: The complete formula open parenthesis A implies B close parenthesis implies A, carrying the true sign comma the complete formula A, carrying the false sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: proving-things.tex, line 455, column 7

Expression 161

Inline MathML variant

Γ \cup {\neg A}

Block MathML variant

Γ \cup {\neg A}

Conventional reading: Gamma union the set containing not A

Meaning here: Gamma union the set containing not A. This denotes the displayed union of premise sets.

2 occurrences

Expression 162

Inline MathML variant

s_{1} = s_{1}

Block MathML variant

s_{1} = s_{1}

Conventional reading: term s sub one is identical to term s sub one

Meaning here: The expression read 'term s sub one is identical to term s sub one' preserves the two terms or metalevel quantities and the source's equality role.

1 occurrence

Occurrence 1: identity.tex, line 71, column 34

Occurrence 1: proving-things.tex, line 432, column 7

Expression 167

Inline MathML variant

A (s_{3})

Block MathML variant

A (s_{3})

Conventional reading: formula A with argument term s sub three

Meaning here: The expression read 'formula A with argument term s sub three' has the exact index, term, formula, sign, or structure role fixed by its source occurrence.

1 occurrence

Occurrence 1: identity.tex, line 89, column 38

Expression 168

Inline MathML variant

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

Block MathML variant

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

Conventional reading: two tableau assumption sets: first, true-signed A together with true-signed B sub one through B sub n; second, true-signed not A together with true-signed C sub one through C sub m

Meaning here: Two tableau assumption sets: first, true-signed A together with true-signed B sub one through B sub n; second, true-signed not A together with true-signed C sub one through C sub m. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-consistency.tex, line 108, column 3

Expression 169

Inline MathML variant

Γ_{0} \subseteq Γ

Block MathML variant

Γ_{0} \subseteq Γ

Meaning here: The complete formula A, carrying sign S belongs to Gamma. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

2 occurrences

Expression 176

Inline MathML variant

T \exists x A (x) \land \forall y \forall z ((A (y) \land A (z)) \to y = z)

Block MathML variant

T \exists x A (x) \land \forall y \forall z ((A (y) \land A (z)) \to y = z)

Conventional reading: the complete formula the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis, carrying the true sign

Meaning here: The expression read 'the complete formula the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis, carrying the true sign' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: identity.tex, line 100, column 3

Occurrence 1: soundness.tex, line 211, column 29

Expression 180

Inline MathML variant

B_{n}

Block MathML variant

B_{n}

Conventional reading: formula B sub n

Meaning here: The expression read 'formula B sub n' has the exact index, term, formula, sign, or structure role fixed by its source occurrence.

1 occurrence

Occurrence 1: provability-quantifiers.tex, line 57, column 25

Expression 181

Inline MathML variant

M, s ⊨ A (t_{1})

Block MathML variant

M, s ⊨ A (t_{1})

Conventional reading: structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub one

Meaning here: The expression read 'structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub one' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness-identity.tex, line 35, column 43

Expression 182

Inline MathML variant

M ⊨ Γ

Block MathML variant

M ⊨ Γ

1 occurrence

Occurrence 1: proof-theoretic-notions.tex, line 42, column 1

Expression 188

Inline MathML variant

T C_{m}

Block MathML variant

T C_{m}

Conventional reading: the complete formula C sub m, carrying the true sign

Meaning here: The complete formula C sub m, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-consistency.tex, line 117, column 47

Expression 189

Inline MathML variant

F \forall x A (x)

Block MathML variant

F \forall x A (x)

Conventional reading: the complete formula for every variable x, formula A with argument variable x, carrying the false sign

Meaning here: The expression read 'the complete formula for every variable x, formula A with argument variable x, carrying the false sign' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: provability-quantifiers.tex, line 34, column 1

Occurrence 1: proving-things.tex, line 422, column 7

Expression 193

Inline MathML variant

A \in Γ

Block MathML variant

A \in Γ

Meaning here: The expression read 'structure M does not satisfy formula B' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

3 occurrences

Expression 197

Inline MathML variant

s_{1} = x

Block MathML variant

s_{1} = x

Conventional reading: term s sub one is identical to variable x

Meaning here: The expression read 'term s sub one is identical to variable x' preserves the two terms or metalevel quantities and the source's equality role.

1 occurrence

Occurrence 1: identity.tex, line 88, column 27

Expression 198

Inline MathML variant

t_{1}

Block MathML variant

t_{1}

Conventional reading: term t sub one

Meaning here: The expression read 'term t sub one' has the exact index, term, formula, sign, or structure role fixed by its source occurrence.

2 occurrences

Expression 199

Inline MathML variant

M' ⊭ A (a)

Block MathML variant

M' ⊭ A (a)

Conventional reading: structure M prime does not satisfy formula A with argument constant a

Meaning here: The expression read 'structure M prime does not satisfy formula A with argument constant a' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness.tex, line 155, column 45

Expression 200

Inline MathML variant

M ⊨ t_{1} = t_{2}

Block MathML variant

M ⊨ t_{1} = t_{2}

Conventional reading: structure M satisfies the identity formula stating that term t sub one is identical to term t sub two

Meaning here: The expression read 'structure M satisfies the identity formula stating that term t sub one is identical to term t sub two' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

2 occurrences

Expression 201

Inline MathML variant

M, s ⊨ A (x)

Block MathML variant

M, s ⊨ A (x)

Conventional reading: structure M, under variable assignment lowercase s, satisfies formula A with argument variable x

Meaning here: The expression read 'structure M, under variable assignment lowercase s, satisfies formula A with argument variable x' states satisfaction or non-satisfaction in the named structure and, when printed, under the named assignment.

1 occurrence

Occurrence 1: soundness-identity.tex, line 37, column 1

Occurrence 1: proof-theoretic-notions.tex, line 34, column 18

Expression 205

Inline MathML variant

⊢ A

Block MathML variant

⊢ A

Occurrence 1: proving-things.tex, line 440, column 7

Expression 212

Inline MathML variant

t_{1} = t_{2}

Block MathML variant

t_{1} = t_{2}

Conventional reading: term t sub one is identical to term t sub two

Meaning here: The expression read 'term t sub one is identical to term t sub two' preserves the two terms or metalevel quantities and the source's equality role.

1 occurrence

Occurrence 1: identity.tex, line 89, column 1

Expression 213

Inline MathML variant

Γ_{0} ⊢ A

Block MathML variant

Γ_{0} ⊢ A

Conventional reading: A is tableau-derivable from Gamma sub zero

Meaning here: A is tableau-derivable from Gamma sub zero. Derivability here is defined by existence of the corresponding closed tableau, not by the sequent-calculus or natural-deduction rules used in other chapters.

2 occurrences

Expression 214

Inline MathML variant

A (s_{1})

Block MathML variant

A (s_{1})

Conventional reading: formula A with argument term s sub one

Meaning here: The expression read 'formula A with argument term s sub one' has the exact index, term, formula, sign, or structure role fixed by its source occurrence.

1 occurrence

Occurrence 1: identity.tex, line 71, column 21

Expression 215

Inline MathML variant

T A (t)

Block MathML variant

T A (t)

Occurrence 1: proof-theoretic-notions.tex, line 186, column 42

Expression 221

Inline MathML variant

\to

Block MathML variant

\to

Meaning here: The complete formula A, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

18 occurrences

Expression 229

Inline MathML variant

2

Block MathML variant

2

Conventional reading: two

Meaning here: Two is the referenced tableau line number.

10 occurrences

Expression 230

Inline MathML variant

M ⊨ A

Block MathML variant

M ⊨ A

4 occurrences

Expression 239

Inline MathML variant

s (x) = ⟦ t_{2} ⟧_{M}

Block MathML variant

s (x) = ⟦ t_{2} ⟧_{M}

Conventional reading: s applied to variable x is identical to the value of term t sub two in structure M

Meaning here: The expression read 's applied to variable x is identical to the value of term t sub two in structure M' denotes the exact term value, symbol interpretation, or assignment relation printed by the source.

1 occurrence

Occurrence 1: soundness-identity.tex, line 38, column 46

Expression 240

Inline MathML variant

t

Block MathML variant

t

Expression 271

Inline MathML variant

{F A \to B, T \neg A}

Block MathML variant

{F A \to B, T \neg A}

Conventional reading: the set containing the complete formula A implies B, carrying the false sign comma the complete formula not A, carrying the true sign

Meaning here: The set containing the complete formula A implies B, carrying the false sign comma the complete formula not A, carrying the true sign. Each true or false prefix is a tableau sign attached to the complete formula that follows; when several signed formulas occur inside braces, they are simultaneous tableau assumptions.

1 occurrence

Occurrence 1: provability-propositional.tex, line 148, column 16

Expression 272

Inline MathML variant

\land T

Block MathML variant

\land T

Conventional reading: true-conjunction tableau rule

Meaning here: True-conjunction tableau rule. This names the exact truth-sign and connective expansion rule used by a propositional tableau.

6 occurrences

Expression 273

Inline MathML variant

F A (t), T \forall x A (x),

Block MathML variant

F A (t), T \forall x A (x),

Conventional reading: first 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, followed by a printed trailing comma with no following formula

Meaning here: The expression read 'first 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, followed by a printed trailing comma with no following formula' preserves every truth sign, complete first-order formula, branch, and written order.

1 occurrence

Occurrence 1: provability-quantifiers.tex, line 79, column 3

Expression 274

Inline MathML variant

B_{1}

Block MathML variant

B_{1}

Conventional reading: B sub one

Meaning here: B sub one is the first propositional formula in the indexed premise family.

6 occurrences

Expression 275

Inline MathML variant

C_{m} \in Γ

Block MathML variant

C_{m} \in Γ

Conventional reading: C sub m belongs to Gamma

Meaning here: C sub m belongs to Gamma. This states membership in the displayed premise set.

1 occurrence

Occurrence 1: provability-consistency.tex, line 107, column 3

121 formal objects

Definition of a signed formula

A signed formula is a pair consisting of a truth value and a sentence. It is either the complete formula A carrying the true sign, or the complete formula A carrying the false sign.

A signed formula is a pair consisting of a truth value and a sentence.
It is either the complete formula A carrying the true sign, or the complete formula A carrying the false sign.

Source: content/first-order-logic/tableaux/rules-and-proofs.tex, line 21.

Definition of the negation tableau rules

The true-negation rule starts with not A carrying the true sign and continues the same branch with A carrying the false sign. The false-negation rule starts with not A carrying the false sign and continues the same branch with A carrying the true sign.

The true-negation rule starts with not A carrying the true sign and continues the same branch with A carrying the false sign.
The false-negation rule starts with not A carrying the false sign and continues the same branch with A carrying the true sign.

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 17.

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: content/first-order-logic/tableaux/propositional-rules.tex, line 21.

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: content/first-order-logic/tableaux/propositional-rules.tex, line 26.

Definition of the conjunction tableau rules

The true-conjunction rule starts with A and B carrying the true sign, then adds A carrying the true sign and B carrying the true sign on the same branch. The false-conjunction rule starts with A and B carrying the false sign, then splits into one branch with A carrying the false sign and another branch with B carrying the false sign.

The true-conjunction rule starts with A and B carrying the true sign, then adds A carrying the true sign and B carrying the true sign on the same branch.
The false-conjunction rule starts with A and B carrying the false sign, then splits into one branch with A carrying the false sign and another branch with B carrying the false sign.

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 31.

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: content/first-order-logic/tableaux/propositional-rules.tex, line 37.

False-conjunction branching tableau rule

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

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

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 42.

Definition of the disjunction tableau rules

The true-disjunction rule starts with A or B carrying the true sign, then splits into one branch with A carrying the true sign and another branch with B carrying the true sign. The false-disjunction rule starts with A or B carrying the false sign, then adds A carrying the false sign and B carrying the false sign on the same branch.

The true-disjunction rule starts with A or B carrying the true sign, then splits into one branch with A carrying the true sign and another branch with B carrying the true sign.
The false-disjunction rule starts with A or B carrying the false sign, then adds A carrying the false sign and B carrying the false sign on the same branch.

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 47.

True-disjunction branching tableau rule

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

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

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 51.

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: content/first-order-logic/tableaux/propositional-rules.tex, line 58.

Definition of the conditional tableau rules

The true-conditional rule starts with the conditional from A to B carrying the true sign, then splits into one branch with A carrying the false sign and another branch with B carrying the true sign. The false-conditional rule starts with the conditional from A to B carrying the false sign, then adds A carrying the true sign and B carrying the false sign on the same branch.

The true-conditional rule starts with the conditional from A to B carrying the true sign, then splits into one branch with A carrying the false sign and another branch with B carrying the true sign.
The false-conditional rule starts with the conditional from A to B carrying the false sign, then adds A carrying the true sign and B carrying the false sign on the same branch.

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 63.

True-conditional branching tableau rule

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

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

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 67.

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: content/first-order-logic/tableaux/propositional-rules.tex, line 74.

Definition of the cut tableau rule

The cut rule has no formula premise at the current node. Choose a formula A and split the branch into A carrying the true sign on one side and A carrying the false sign on the other.

The cut rule has no formula premise at the current node.
Choose a formula A and split the branch into A carrying the true sign on one side and A carrying the false sign on the other.

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 79.

Cut branching rule

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

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

Source: content/first-order-logic/tableaux/propositional-rules.tex, line 83.

Definition of the universal-quantifier tableau rules

The true-universal rule starts with every x satisfying A of x, carrying the true sign, and adds A of t carrying the true sign for any closed term t. The false-universal rule starts with every x satisfying A of x, carrying the false sign, and adds A of a carrying the false sign, where a is a new constant not occurring earlier on the branch. The freshness requirement on a is the eigenvariable condition; the true-universal rule has no corresponding freshness restriction on t.

The true-universal rule starts with every x satisfying A of x, carrying the true sign, and adds A of t carrying the true sign for any closed term t.
The false-universal rule starts with every x satisfying A of x, carrying the false sign, and adds A of a carrying the false sign, where a is a new constant not occurring earlier on the branch.
The freshness requirement on a is the eigenvariable condition; the true-universal rule has no corresponding freshness restriction on t.

Source: content/first-order-logic/tableaux/quantifier-rules.tex, line 15.

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: content/first-order-logic/tableaux/quantifier-rules.tex, line 19.

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: content/first-order-logic/tableaux/quantifier-rules.tex, line 24.

Definition of the existential-quantifier tableau rules

The true-existential rule starts with some x satisfying A of x, carrying the true sign, and adds A of a carrying the true sign, where a is a new constant not occurring earlier on the branch. The false-existential rule starts with some x satisfying A of x, carrying the false sign, and adds A of t carrying the false sign for any closed term t. The freshness requirement on a is the eigenvariable condition; the false-existential rule has no corresponding freshness restriction on t.

The true-existential rule starts with some x satisfying A of x, carrying the true sign, and adds A of a carrying the true sign, where a is a new constant not occurring earlier on the branch.
The false-existential rule starts with some x satisfying A of x, carrying the false sign, and adds A of t carrying the false sign for any closed term t.
The freshness requirement on a is the eigenvariable condition; the false-existential rule has no corresponding freshness restriction on t.

Source: content/first-order-logic/tableaux/quantifier-rules.tex, line 37.

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: content/first-order-logic/tableaux/quantifier-rules.tex, line 41.

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: content/first-order-logic/tableaux/quantifier-rules.tex, line 46.

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: content/first-order-logic/tableaux/quantifier-rules.tex, line 62.

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.

Source: content/first-order-logic/tableaux/quantifier-rules.tex, line 89.

Definition of a tableau derivation

A tableau for assumptions A sub one through A sub n, carrying signs S sub one through S sub n, is a finite tree of signed formulas; every S sub i is either the true sign or the false sign. First condition: the n topmost signed formulas are exactly those n assumptions, placed one below another. Second condition: every other signed formula results from a correct application of an inference rule to a signed formula in the branch above it. A branch is closed if and only if it contains both A carrying the true sign and that same A carrying the false sign; otherwise the branch is open. A tableau is closed when every branch is closed. It is open when it is not closed, equivalently when it has at least one open branch.

A tableau for assumptions A sub one through A sub n, carrying signs S sub one through S sub n, is a finite tree of signed formulas; every S sub i is either the true sign or the false sign.
First condition: the n topmost signed formulas are exactly those n assumptions, placed one below another.
Second condition: every other signed formula results from a correct application of an inference rule to a signed formula in the branch above it.
A branch is closed if and only if it contains both A carrying the true sign and that same A carrying the false sign; otherwise the branch is open.
A tableau is closed when every branch is closed. It is open when it is not closed, equivalently when it has at least one open branch.

Source: content/first-order-logic/tableaux/derivations.tex, line 23.

Example of extending a tableau derivation

Any set of assumptions by itself is a tableau, although it is closed only when the assumptions already include one formula with both the true and false signs. A larger tableau is obtained by applying an inference rule to a signed formula A and appending the rule conclusions to every branch containing that occurrence of A. The example starts with the single open assumption: A and not A, carrying the true sign. Applying the true-conjunction rule adds A carrying the true sign and not A carrying the true sign on the same branch. Printed rule annotations identify the applied rule and its source line; for example, true-conjunction one means the true-conjunction rule was applied to line one. Only not A carrying the true sign remains expandable. The true-negation rule adds A carrying the false sign, which closes the branch against A carrying the true sign.

Any set of assumptions by itself is a tableau, although it is closed only when the assumptions already include one formula with both the true and false signs.
A larger tableau is obtained by applying an inference rule to a signed formula A and appending the rule conclusions to every branch containing that occurrence of A.
The example starts with the single open assumption: A and not A, carrying the true sign.
Applying the true-conjunction rule adds A carrying the true sign and not A carrying the true sign on the same branch.
Printed rule annotations identify the applied rule and its source line; for example, true-conjunction one means the true-conjunction rule was applied to line one.
Only not A carrying the true sign remains expandable. The true-negation rule adds A carrying the false sign, which closes the branch against A carrying the true sign.

Source: content/first-order-logic/tableaux/derivations.tex, line 42.

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.

Source: content/first-order-logic/tableaux/derivations.tex, line 58.

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.

Source: content/first-order-logic/tableaux/derivations.tex, line 66.

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.

Source: content/first-order-logic/tableaux/derivations.tex, line 84.

Example proving that if A and B then A

The example seeks a closed tableau for the conditional from A and B to A. It begins with that conditional carrying the false sign as the sole assumption. Because each signed formula has at most one rule determined by its sign and main operator, the false-conditional rule must be applied; it adds A and B carrying the true sign, followed by A carrying the false sign. A checkmark is written only after the rule has been applied on every open branch containing that signed formula; checkmarks help construction but are not part of tableau syntax. Applying the true-conjunction rule to line two adds A carrying the true sign and B carrying the true sign. The only branch now contains A with both signs, so it closes and supplies the required closed tableau.

The example seeks a closed tableau for the conditional from A and B to A.
It begins with that conditional carrying the false sign as the sole assumption.
Because each signed formula has at most one rule determined by its sign and main operator, the false-conditional rule must be applied; it adds A and B carrying the true sign, followed by A carrying the false sign.
A checkmark is written only after the rule has been applied on every open branch containing that signed formula; checkmarks help construction but are not part of tableau syntax.
Applying the true-conjunction rule to line two adds A carrying the true sign and B carrying the true sign.
The only branch now contains A with both signs, so it closes and supplies the required closed tableau.

Source: content/first-order-logic/tableaux/proving-things.tex, line 15.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 20.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 30.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 52.

Example proving a nested conditional by tableau

The example seeks a closed tableau for the conditional from not A or B to the conditional from A to B. It begins with the whole conditional carrying the false sign. The false-conditional rule adds not A or B carrying the true sign, then the conditional from A to B carrying the false sign. Either expandable line may be handled first, because every signed formula must eventually have its rule applied in every branch. Applying the true-disjunction rule to line two splits the tableau: the left branch receives not A carrying the true sign and the right branch receives B carrying the true sign. Applying the false-conditional rule from line three on both branches adds A carrying the true sign and B carrying the false sign to each branch; only then may line three be checked. The right branch closes because it contains B with both signs. On the left branch, true negation applied to not A adds A carrying the false sign and closes against A carrying the true sign.

The example seeks a closed tableau for the conditional from not A or B to the conditional from A to B.
It begins with the whole conditional carrying the false sign.
The false-conditional rule adds not A or B carrying the true sign, then the conditional from A to B carrying the false sign.
Either expandable line may be handled first, because every signed formula must eventually have its rule applied in every branch.
Applying the true-disjunction rule to line two splits the tableau: the left branch receives not A carrying the true sign and the right branch receives B carrying the true sign.
Applying the false-conditional rule from line three on both branches adds A carrying the true sign and B carrying the false sign to each branch; only then may line three be checked.
The right branch closes because it contains B with both signs. On the left branch, true negation applied to not A adds A carrying the false sign and closes against A carrying the true sign.

Source: content/first-order-logic/tableaux/proving-things.tex, line 72.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 77.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 84.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 102.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 122.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 146.

Example closing a branching tableau

Tableaux may begin with any number of signed assumptions, may use more than one branching rule, and may have any number of branches. This example begins with two assumptions: A or open parenthesis B and C close parenthesis carrying the true sign; and open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis carrying the false sign. The true-disjunction rule on the first assumption splits into a branch with A carrying the true sign and a branch with B and C carrying the true sign. The false-conjunction rule is applied to the second assumption on both branches, splitting each into a continuation with A or B carrying the false sign and one with A or C carrying the false sign. False disjunction is applied to every branch containing A or B, adding A carrying the false sign and then B carrying the false sign; the branch already containing A carrying the true sign closes. False disjunction is next applied to every branch containing A or C, adding A carrying the false sign and then C carrying the false sign; the other branch containing A carrying the true sign closes. One printed node is moved downward only for visual clarity, without changing structure. Two branches remain open and B and C carrying the true sign remains unchecked. True conjunction adds B carrying the true sign and C carrying the true sign on each such branch, closing one against false-signed B and the other against false-signed C. The source finally presents a second closed tableau for the same two assumptions, applying the rules in a different order to demonstrate that the construction order may vary.

Tableaux may begin with any number of signed assumptions, may use more than one branching rule, and may have any number of branches.
This example begins with two assumptions: A or open parenthesis B and C close parenthesis carrying the true sign; and open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis carrying the false sign.
The true-disjunction rule on the first assumption splits into a branch with A carrying the true sign and a branch with B and C carrying the true sign.
The false-conjunction rule is applied to the second assumption on both branches, splitting each into a continuation with A or B carrying the false sign and one with A or C carrying the false sign.
False disjunction is applied to every branch containing A or B, adding A carrying the false sign and then B carrying the false sign; the branch already containing A carrying the true sign closes.
False disjunction is next applied to every branch containing A or C, adding A carrying the false sign and then C carrying the false sign; the other branch containing A carrying the true sign closes. One printed node is moved downward only for visual clarity, without changing structure.
Two branches remain open and B and C carrying the true sign remains unchecked. True conjunction adds B carrying the true sign and C carrying the true sign on each such branch, closing one against false-signed B and the other against false-signed C.
The source finally presents a second closed tableau for the same two assumptions, applying the rules in a different order to demonstrate that the construction order may vary.

Source: content/first-order-logic/tableaux/proving-things.tex, line 173.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 181.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 195.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 218.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 251.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 304.

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.

Source: content/first-order-logic/tableaux/proving-things.tex, line 366.

Exercise on associativity and double negation tableaux

Unsolved exercise. Give a closed tableau for each of the following four source-listed sets of signed assumptions; no solution is supplied. Source-listed mathematical item one: the complete formula A and open parenthesis B and C close parenthesis, carrying the true sign comma the complete formula open parenthesis A and B close parenthesis and C, carrying the false sign. Source-listed mathematical item two: the complete formula A or open parenthesis B or C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis or C, carrying the false sign. Source-listed mathematical item three: the complete formula A implies open parenthesis B implies C close parenthesis, carrying the true sign comma the complete formula B implies open parenthesis A implies C close parenthesis, carrying the false sign. Source-listed mathematical item four: the complete formula A, carrying the true sign comma the complete formula not not A, carrying the false sign.

Unsolved source exercise; no solution added.

Unsolved exercise. Give a closed tableau for each of the following four source-listed sets of signed assumptions; no solution is supplied.
Source-listed mathematical item one: the complete formula A and open parenthesis B and C close parenthesis, carrying the true sign comma the complete formula open parenthesis A and B close parenthesis and C, carrying the false sign.
Source-listed mathematical item two: the complete formula A or open parenthesis B or C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis or C, carrying the false sign.
Source-listed mathematical item three: the complete formula A implies open parenthesis B implies C close parenthesis, carrying the true sign comma the complete formula B implies open parenthesis A implies C close parenthesis, carrying the false sign.
Source-listed mathematical item four: the complete formula A, carrying the true sign comma the complete formula not not A, carrying the false sign.

Source: content/first-order-logic/tableaux/proving-things.tex, line 418.

Exercise on equivalences and De Morgan tableaux

Unsolved exercise. Give a closed tableau for each of the following twelve source-listed sets of signed assumptions; no solution is supplied. Source-listed mathematical item one: the complete formula open parenthesis A or B close parenthesis implies C, carrying the true sign comma the complete formula A implies C, carrying the false sign. Source-listed mathematical item two: the complete formula open parenthesis A implies C close parenthesis and open parenthesis B implies C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis implies C, carrying the false sign. Source-listed mathematical item three: the complete formula not open parenthesis A and not A close parenthesis, carrying the false sign. Source-listed mathematical item four: the complete formula B implies A, carrying the true sign comma the complete formula not A implies not B, carrying the false sign. Source-listed mathematical item five: the complete formula open parenthesis A implies not A close parenthesis implies not A, carrying the false sign. Source-listed mathematical item six: the complete formula not open parenthesis A implies B close parenthesis implies not B, carrying the false sign. Source-listed mathematical item seven: the complete formula A implies C, carrying the true sign comma the complete formula not open parenthesis A and not C close parenthesis, carrying the false sign. Source-listed mathematical item eight: the complete formula A and not C, carrying the true sign comma the complete formula not open parenthesis A implies C close parenthesis, carrying the false sign. Source-listed mathematical item nine: three tableau assumptions: the complete disjunction A or B carrying the true sign; the complete formula not B carrying the true sign; and the complete formula A carrying the false sign. Source-listed mathematical item ten: the complete formula not A or not B, carrying the true sign comma the complete formula not open parenthesis A and B close parenthesis, carrying the false sign. Source-listed mathematical item eleven: the complete formula open parenthesis not A and not B close parenthesis implies not open parenthesis A or B close parenthesis, carrying the false sign. Source-listed mathematical item twelve: the complete formula not open parenthesis A or B close parenthesis implies open parenthesis not A and not B close parenthesis, carrying the false sign. Source correction disclosure: 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.

Unsolved source exercise; no solution added.

Unsolved exercise. Give a closed tableau for each of the following twelve source-listed sets of signed assumptions; no solution is supplied.
Source-listed mathematical item one: the complete formula open parenthesis A or B close parenthesis implies C, carrying the true sign comma the complete formula A implies C, carrying the false sign.
Source-listed mathematical item two: the complete formula open parenthesis A implies C close parenthesis and open parenthesis B implies C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis implies C, carrying the false sign.
Source-listed mathematical item three: the complete formula not open parenthesis A and not A close parenthesis, carrying the false sign.
Source-listed mathematical item four: the complete formula B implies A, carrying the true sign comma the complete formula not A implies not B, carrying the false sign.
Source-listed mathematical item five: the complete formula open parenthesis A implies not A close parenthesis implies not A, carrying the false sign.
Source-listed mathematical item six: the complete formula not open parenthesis A implies B close parenthesis implies not B, carrying the false sign.
Source-listed mathematical item seven: the complete formula A implies C, carrying the true sign comma the complete formula not open parenthesis A and not C close parenthesis, carrying the false sign.
Source-listed mathematical item eight: the complete formula A and not C, carrying the true sign comma the complete formula not open parenthesis A implies C close parenthesis, carrying the false sign.
Source-listed mathematical item nine: three tableau assumptions: the complete disjunction A or B carrying the true sign; the complete formula not B carrying the true sign; and the complete formula A carrying the false sign.
Source-listed mathematical item ten: the complete formula not A or not B, carrying the true sign comma the complete formula not open parenthesis A and B close parenthesis, carrying the false sign.
Source-listed mathematical item eleven: the complete formula open parenthesis not A and not B close parenthesis implies not open parenthesis A or B close parenthesis, carrying the false sign.
Source-listed mathematical item twelve: the complete formula not open parenthesis A or B close parenthesis implies open parenthesis not A and not B close parenthesis, carrying the false sign.
Source correction disclosure: 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: content/first-order-logic/tableaux/proving-things.tex, line 428.

Exercise on conditional and negation tableaux

Unsolved exercise. Give a closed tableau for each of the following eight source-listed sets of signed assumptions; no solution is supplied. Source-listed mathematical item one: the complete formula not open parenthesis A implies B close parenthesis, carrying the true sign comma the complete formula A, carrying the false sign. Source-listed mathematical item two: the complete formula not open parenthesis A and B close parenthesis, carrying the true sign comma the complete formula not A or not B, carrying the false sign. Source-listed mathematical item three: the complete formula A implies B, carrying the true sign comma the complete formula not A or B, carrying the false sign. Source-listed mathematical item four: the complete formula not not A implies A, carrying the false sign. Source-listed mathematical item five: the complete formula A implies B, carrying the true sign comma the complete formula not A implies B, carrying the true sign comma the complete formula B, carrying the false sign. Source-listed mathematical item six: the complete formula open parenthesis A and B close parenthesis implies C, carrying the true sign comma the complete formula open parenthesis A implies C close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign. Source-listed mathematical item seven: the complete formula open parenthesis A implies B close parenthesis implies A, carrying the true sign comma the complete formula A, carrying the false sign. Source-listed mathematical item eight: the complete formula open parenthesis A implies B close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign.

Unsolved source exercise; no solution added.

Unsolved exercise. Give a closed tableau for each of the following eight source-listed sets of signed assumptions; no solution is supplied.
Source-listed mathematical item one: the complete formula not open parenthesis A implies B close parenthesis, carrying the true sign comma the complete formula A, carrying the false sign.
Source-listed mathematical item two: the complete formula not open parenthesis A and B close parenthesis, carrying the true sign comma the complete formula not A or not B, carrying the false sign.
Source-listed mathematical item three: the complete formula A implies B, carrying the true sign comma the complete formula not A or B, carrying the false sign.
Source-listed mathematical item four: the complete formula not not A implies A, carrying the false sign.
Source-listed mathematical item five: the complete formula A implies B, carrying the true sign comma the complete formula not A implies B, carrying the true sign comma the complete formula B, carrying the false sign.
Source-listed mathematical item six: the complete formula open parenthesis A and B close parenthesis implies C, carrying the true sign comma the complete formula open parenthesis A implies C close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign.
Source-listed mathematical item seven: the complete formula open parenthesis A implies B close parenthesis implies A, carrying the true sign comma the complete formula A, carrying the false sign.
Source-listed mathematical item eight: the complete formula open parenthesis A implies B close parenthesis or open parenthesis B implies C close parenthesis, carrying the false sign.

Source: content/first-order-logic/tableaux/proving-things.tex, line 446.

Example closing a quantified conditional tableau

The example seeks a closed tableau for the conditional from there exists an x such that not A of x, to not every x satisfying A of x. It starts with that conditional carrying the false sign, then applies false conditional to add the existential antecedent with the true sign and the negated universal consequent with the false sign. True existential is handled first with a fresh constant a, producing not A of a with the true sign without violating the eigenvariable condition. False negation applied to the negated universal produces the universal formula with the true sign. True negation applied to not A of a produces A of a with the false sign; true universal instantiated with a produces A of a with the true sign, closing the branch.

The example seeks a closed tableau for the conditional from there exists an x such that not A of x, to not every x satisfying A of x.
It starts with that conditional carrying the false sign, then applies false conditional to add the existential antecedent with the true sign and the negated universal consequent with the false sign.
True existential is handled first with a fresh constant a, producing not A of a with the true sign without violating the eigenvariable condition.
False negation applied to the negated universal produces the universal formula with the true sign.
True negation applied to not A of a produces A of a with the false sign; true universal instantiated with a produces A of a with the true sign, closing the branch.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 13.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 23.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 29.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 42.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 55.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 73.

Example closing a three-assumption quantifier tableau

The example begins with three assumptions: no object satisfies C with second argument b; some object satisfies both A and B; and every object satisfying B also satisfies C with second argument b. Because b already occurs among the assumptions, true existential is applied first using a different fresh constant a, yielding A of a and B of a with the true sign. The repeatable false-existential and true-universal rules are then instantiated with a, producing C of a comma b with the false sign and the conditional from B of a to C of a comma b with the true sign. The quantified assumptions remain unchecked because later instantiations could still be needed; true conjunction next adds A of a and B of a separately with the true sign. True conditional splits the branch into B of a with the false sign and C of a comma b with the true sign. Each branch closes against the corresponding formula already carrying the opposite sign.

The example begins with three assumptions: no object satisfies C with second argument b; some object satisfies both A and B; and every object satisfying B also satisfies C with second argument b.
Because b already occurs among the assumptions, true existential is applied first using a different fresh constant a, yielding A of a and B of a with the true sign.
The repeatable false-existential and true-universal rules are then instantiated with a, producing C of a comma b with the false sign and the conditional from B of a to C of a comma b with the true sign.
The quantified assumptions remain unchecked because later instantiations could still be needed; true conjunction next adds A of a and B of a separately with the true sign.
True conditional splits the branch into B of a with the false sign and C of a comma b with the true sign. Each branch closes against the corresponding formula already carrying the opposite sign.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 96.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 104.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 117.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 137.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 155.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 177.

Example coordinating eigenvariable and repeatable quantifier rules

The example begins with three true-signed assumptions: every x satisfies A of x; if every x satisfies A of x then some y satisfies B of y; and not some y satisfying B of y. True negation first converts the third assumption into the existential formula carrying the false sign. True conditional then splits the tableau: one branch receives the universal A formula with the false sign, and the other receives the existential B formula with the true sign. The two new formulas use eigenvariable rules, so false universal introduces a fresh b and yields A of b with the false sign, while true existential introduces a fresh c and yields B of c with the true sign. On the first branch, true universal is instantiated with b to add A of b with the true sign and close. On the second, false existential is instantiated with c to add B of c with the false sign and close.

The example begins with three true-signed assumptions: every x satisfies A of x; if every x satisfies A of x then some y satisfies B of y; and not some y satisfying B of y.
True negation first converts the third assumption into the existential formula carrying the false sign.
True conditional then splits the tableau: one branch receives the universal A formula with the false sign, and the other receives the existential B formula with the true sign.
The two new formulas use eigenvariable rules, so false universal introduces a fresh b and yields A of b with the false sign, while true existential introduces a fresh c and yields B of c with the true sign.
On the first branch, true universal is instantiated with b to add A of b with the true sign and close. On the second, false existential is instantiated with c to add B of c with the false sign and close.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 212.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 219.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 233.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 246.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 262.

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.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 285.

Exercise on six quantified tableau problems

Unsolved exercise. Give a closed tableau for each of the following six source-listed quantified problems; no solution is supplied. Source-listed mathematical item one: the complete formula the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable z, open parenthesis, the conjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis, carrying the false sign. Source-listed mathematical item two: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of for some variable x, formula A with argument variable x and for some variable y, formula B with argument variable y, close parenthesis; and whose consequent is for some variable z, open parenthesis, the disjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis, carrying the false sign. Source-listed mathematical item three: first the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is formula B, close parenthesis, carrying the true sign, then the complete formula the conditional whose antecedent is for some variable y, formula A with argument variable y; and whose consequent is formula B, carrying the false sign. Source-listed mathematical item four: first the complete formula for every variable x, the negation of formula A with argument variable x, carrying the true sign, then the complete formula the negation of for some variable x, formula A with argument variable x, carrying the false sign. Source-listed mathematical item five: the complete formula the conditional whose antecedent is the negation of for some variable x, formula A with argument variable x; and whose consequent is for every variable x, the negation of formula A with argument variable x, carrying the false sign. Source-listed mathematical item six: the complete formula the negation of for some variable x, for every variable y, open parenthesis, the conjunction of open parenthesis, the conditional whose antecedent is formula A with arguments variable x and variable y; and whose consequent is the negation of formula A with arguments variable y and variable y, close parenthesis and open parenthesis, the conditional whose antecedent is the negation of formula A with arguments variable y and variable y; and whose consequent is formula A with arguments variable x and variable y, close parenthesis, close parenthesis, carrying the false sign.

Unsolved source exercise; no solution added.

Unsolved exercise. Give a closed tableau for each of the following six source-listed quantified problems; no solution is supplied.
Source-listed mathematical item one: the complete formula the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable z, open parenthesis, the conjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis, carrying the false sign.
Source-listed mathematical item two: the complete formula the conditional whose antecedent is open parenthesis, the disjunction of for some variable x, formula A with argument variable x and for some variable y, formula B with argument variable y, close parenthesis; and whose consequent is for some variable z, open parenthesis, the disjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis, carrying the false sign.
Source-listed mathematical item three: first the complete formula for every variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is formula B, close parenthesis, carrying the true sign, then the complete formula the conditional whose antecedent is for some variable y, formula A with argument variable y; and whose consequent is formula B, carrying the false sign.
Source-listed mathematical item four: first the complete formula for every variable x, the negation of formula A with argument variable x, carrying the true sign, then the complete formula the negation of for some variable x, formula A with argument variable x, carrying the false sign.
Source-listed mathematical item five: the complete formula the conditional whose antecedent is the negation of for some variable x, formula A with argument variable x; and whose consequent is for every variable x, the negation of formula A with argument variable x, carrying the false sign.
Source-listed mathematical item six: the complete formula the negation of for some variable x, for every variable y, open parenthesis, the conjunction of open parenthesis, the conditional whose antecedent is formula A with arguments variable x and variable y; and whose consequent is the negation of formula A with arguments variable y and variable y, close parenthesis and open parenthesis, the conditional whose antecedent is the negation of formula A with arguments variable y and variable y; and whose consequent is formula A with arguments variable x and variable y, close parenthesis, close parenthesis, carrying the false sign.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 317.

Exercise on three further quantified tableau problems

Unsolved exercise. Give a closed tableau for each of the following three source-listed quantified problems; no solution is supplied. Source-listed mathematical item one: the complete formula the conditional whose antecedent is the negation of for every variable x, formula A with argument variable x; and whose consequent is for some variable x, the negation of formula A with argument variable x, carrying the false sign. Source-listed mathematical item two: first the complete formula open parenthesis, the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula B, close parenthesis, carrying the true sign, then the complete formula for some variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent is formula B, close parenthesis, carrying the false sign. Source-listed mathematical item three: the complete formula for some variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is for every variable y, formula A with argument variable y, close parenthesis, carrying the false sign.

Unsolved source exercise; no solution added.

Unsolved exercise. Give a closed tableau for each of the following three source-listed quantified problems; no solution is supplied.
Source-listed mathematical item one: the complete formula the conditional whose antecedent is the negation of for every variable x, formula A with argument variable x; and whose consequent is for some variable x, the negation of formula A with argument variable x, carrying the false sign.
Source-listed mathematical item two: first the complete formula open parenthesis, the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula B, close parenthesis, carrying the true sign, then the complete formula for some variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent is formula B, close parenthesis, carrying the false sign.
Source-listed mathematical item three: the complete formula for some variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is for every variable y, formula A with argument variable y, close parenthesis, carrying the false sign.

Source: content/first-order-logic/tableaux/proving-things-quant.tex, line 335.

Definition of tableau theoremhood

A sentence A is a tableau theorem when there is a closed tableau whose assumption is A carrying the false sign. The notation tableau-proves A says A is a theorem; tableau-does-not-prove A says it is not a theorem.

A sentence A is a tableau theorem when there is a closed tableau whose assumption is A carrying the false sign.
The notation tableau-proves A says A is a theorem; tableau-does-not-prove A says it is not a theorem.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 31.

Definition of tableau derivability

A sentence A is tableau-derivable from a set of sentences Gamma if and only if there is a finite set containing B sub one through B sub n that is a subset of Gamma, together with a closed tableau for false-signed A and true-signed B sub one through B sub n. The notation Gamma tableau-proves A records derivability; Gamma tableau-does-not-prove A records non-derivability.

A sentence A is tableau-derivable from a set of sentences Gamma if and only if there is a finite set containing B sub one through B sub n that is a subset of Gamma, together with a closed tableau for false-signed A and true-signed B sub one through B sub n.
The notation Gamma tableau-proves A records derivability; Gamma tableau-does-not-prove A records non-derivability.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 37.

Definition of tableau consistency

A set of sentences Gamma is inconsistent if and only if some finite set containing B sub one through B sub n is a subset of Gamma and there is a closed tableau whose assumptions are B sub one through B sub n, each carrying the true sign. Gamma is consistent when it is not inconsistent.

A set of sentences Gamma is inconsistent if and only if some finite set containing B sub one through B sub n is a subset of Gamma and there is a closed tableau whose assumptions are B sub one through B sub n, each carrying the true sign.
Gamma is consistent when it is not inconsistent.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 53.

Proposition: reflexivity of tableau derivability

Reflexivity: if A belongs to Gamma, then A is tableau-derivable from Gamma.

Reflexivity: if A belongs to Gamma, then A is tableau-derivable from Gamma.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 66.

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.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 73.

Proposition: monotonicity of tableau derivability

Monotonicity: if Gamma is a subset of Delta and A is tableau-derivable from Gamma, then A is tableau-derivable from Delta.

Monotonicity: if Gamma is a subset of Delta and A is tableau-derivable from Gamma, then A is tableau-derivable from Delta.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 82.

Proposition: transitivity of tableau derivability

Transitivity: if A is tableau-derivable from Gamma and B is tableau-derivable from the set containing A together with Delta, then B is tableau-derivable from the union of Gamma and Delta.

Transitivity: if A is tableau-derivable from Gamma and B is tableau-derivable from the set containing A together with Delta, then B is tableau-derivable from the union of Gamma and Delta.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 92.

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.

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.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 101.

Proposition characterizing inconsistency by derivability

Gamma is inconsistent if and only if every sentence A is tableau-derivable from Gamma.

Gamma is inconsistent if and only if every sentence A is tableau-derivable from Gamma.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 140.

Exercise proving the inconsistency characterization

Unsolved exercise. Prove the preceding proposition characterizing inconsistency by derivability; no solution is supplied.

Unsolved source exercise; no solution added.

Unsolved exercise. Prove the preceding proposition characterizing inconsistency by derivability; no solution is supplied.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 151.

Proposition: compactness of tableau derivability and consistency

Compactness, first clause: if A is tableau-derivable from Gamma, then some finite subset Gamma sub zero of Gamma also tableau-derives A. Compactness, second clause: if every finite subset of Gamma is consistent, then Gamma is consistent.

Compactness, first clause: if A is tableau-derivable from Gamma, then some finite subset Gamma sub zero of Gamma also tableau-derives A.
Compactness, second clause: if every finite subset of Gamma is consistent, then Gamma is consistent.

Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 162.

Proposition combining derivability with inconsistency

If A is tableau-derivable from Gamma and the union of Gamma with the singleton set containing A is inconsistent, then Gamma is inconsistent.

If A is tableau-derivable from Gamma and the union of Gamma with the singleton set containing A is inconsistent, then Gamma is inconsistent.

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 19.

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.

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.

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 27.

Proposition relating derivability to inconsistency after adding not A

A is tableau-derivable from Gamma if and only if the union of Gamma with the singleton set containing not A is inconsistent.

A is tableau-derivable from Gamma if and only if the union of Gamma with the singleton set containing not A is inconsistent.

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 40.

Exercise proving the dual inconsistency equivalence

Unsolved exercise. Prove that not A is tableau-derivable from Gamma if and only if the union of Gamma with the singleton set containing A is inconsistent; no solution is supplied. Source-listed mathematical item one: not A is tableau-derivable from Gamma. Source-listed mathematical item two: Gamma union the set containing A.

Unsolved source exercise; no solution added.

Unsolved exercise. Prove that not A is tableau-derivable from Gamma if and only if the union of Gamma with the singleton set containing A is inconsistent; no solution is supplied.
Source-listed mathematical item one: not A is tableau-derivable from Gamma.
Source-listed mathematical item two: Gamma union the set containing A.

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 75.

Proposition deriving inconsistency from A and not A

If A is tableau-derivable from Gamma and not A belongs to Gamma, then Gamma is inconsistent. Source correction disclosure: 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.

If A is tableau-derivable from Gamma and not A belongs to Gamma, then Gamma is inconsistent.
Source correction disclosure: 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: content/first-order-logic/tableaux/provability-consistency.tex, line 79.

Proposition combining two inconsistent extensions of Gamma

If both the union of Gamma with the singleton set containing A and the union of Gamma with the singleton set containing not A are inconsistent, then Gamma is inconsistent. Source correction disclosure: The reader removes the duplicated word in the source phrase 'left left.' Source correction disclosure: The reader corrects the source phrase 'we can applying' to 'we can apply.'

If both the union of Gamma with the singleton set containing A and the union of Gamma with the singleton set containing not A are inconsistent, then Gamma is inconsistent.
Source correction disclosure: The reader removes the duplicated word in the source phrase 'left left.'
Source correction disclosure: The reader corrects the source phrase 'we can applying' to 'we can apply.'

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 100.

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.

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.

Source: content/first-order-logic/tableaux/provability-consistency.tex, line 108.

Proposition: tableau derivability rules for conjunction

Conjunction, first clause: A is tableau-derivable from the conjunctive premise A and B, and B is tableau-derivable from that same conjunctive premise. Conjunction, second clause: A and B is tableau-derivable from the two premises A and B.

Conjunction, first clause: A is tableau-derivable from the conjunctive premise A and B, and B is tableau-derivable from that same conjunctive premise.
Conjunction, second clause: A and B is tableau-derivable from the two premises A and B.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 26.

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

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 the conjunction of formula A and formula B, carrying the true sign. Printed justification: assumption.
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.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 40.

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

Node one, at the root: the complete formula B, carrying the false sign. Printed justification: assumption.
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.
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.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 50.

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.

Node one, at the root: the complete formula the conjunction of formula A and formula B, 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.
Node three, continuing the branch below node two: the complete formula B, carrying the true sign. Printed justification: assumption.
Node three splits into two branches.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 62.

Proposition: tableau derivability rules for disjunction

Disjunction, first clause: the set containing A or B, not A, and not B is inconsistent. Disjunction, second clause: A or B is tableau-derivable from premise A, and it is also tableau-derivable from premise B.

Disjunction, first clause: the set containing A or B, not A, and not B is inconsistent.
Disjunction, second clause: A or B is tableau-derivable from premise A, and it is also tableau-derivable from premise B.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 75.

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.

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

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 86.

Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the false sign

Node one, at the root: the complete formula the disjunction of formula A and formula B, 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.
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.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 103.

Closed tableau beginning with the complete formula the disjunction of formula A and formula B, carrying the false sign, later construction stage two

Node one, at the root: the complete formula the disjunction of formula A and formula B, carrying the false sign. Printed justification: assumption.
Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
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.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 113.

Proposition: tableau derivability rules for conditionals

Conditional, first clause: B is tableau-derivable from the two premises A and the conditional from A to B. Conditional, second clause: the conditional from A to B is tableau-derivable from premise not A, and it is also tableau-derivable from premise B.

Conditional, first clause: B is tableau-derivable from the two premises A and the conditional from A to B.
Conditional, second clause: the conditional from A to B is tableau-derivable from premise not A, and it is also tableau-derivable from premise B.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 126.

Closed tableau beginning with the complete formula B, carrying the false sign, later construction stage two

Node one, at the root: the complete formula B, carrying the false sign. Printed justification: assumption.
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.
Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: assumption.
Node three splits into two branches.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 138.

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

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.
Node two, continuing the branch below node one: the complete formula the negation of formula A, carrying the true sign. Printed justification: assumption.
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.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 151.

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

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.
Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
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.
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.

Source: content/first-order-logic/tableaux/provability-propositional.tex, line 162.

Theorem: strong generalization for tableau derivability

Strong generalization: let c be a constant occurring neither in Gamma nor in A of x. If A of c is tableau-derivable from Gamma, then the universally quantified formula saying every x satisfies A of x is tableau-derivable from Gamma.

Strong generalization: let c be a constant occurring neither in Gamma nor in A of x.
If A of c is tableau-derivable from Gamma, then the universally quantified formula saying every x satisfies A of x is tableau-derivable from Gamma.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 17.

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.

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.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 26.

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.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 37.

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.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 44.

Proposition: tableau derivability rules for quantifiers

Existential clause: A of t tableau-derives the statement that there exists an x satisfying A of x. Universal clause: the statement that every x satisfies A of x tableau-derives A of t.

Existential clause: A of t tableau-derives the statement that there exists an x satisfying A of x.
Universal clause: the statement that every x satisfies A of x tableau-derives A of t.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 61.

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.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 73.

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.

Source: content/first-order-logic/tableaux/provability-quantifiers.tex, line 80.

Definition of satisfaction for signed formulas and branches

A structure M satisfies A carrying the true sign if and only if M satisfies A. The structure satisfies A carrying the false sign if and only if M does not satisfy A. The structure satisfies a set of signed formulas Gamma if and only if it satisfies every signed formula A with sign S that belongs to Gamma. Gamma is satisfiable when some structure satisfies it, and unsatisfiable otherwise.

A structure M satisfies A carrying the true sign if and only if M satisfies A.
The structure satisfies A carrying the false sign if and only if M does not satisfy A.
The structure satisfies a set of signed formulas Gamma if and only if it satisfies every signed formula A with sign S that belongs to Gamma.
Gamma is satisfiable when some structure satisfies it, and unsatisfiable otherwise.

Source: content/first-order-logic/tableaux/soundness.tex, line 41.

Theorem: a closed tableau has no satisfying valuation

Soundness theorem: if a set of signed formulas Gamma has a closed tableau, then Gamma is unsatisfiable.

Soundness theorem: if a set of signed formulas Gamma has a closed tableau, then Gamma is unsatisfiable.

Source: content/first-order-logic/tableaux/soundness.tex, line 53.

Exercise completing first-order tableau soundness

Unsolved exercise. Complete the omitted cases in the proof of first-order tableau soundness; no solution is supplied.

Unsolved source exercise; no solution added.

Unsolved exercise. Complete the omitted cases in the proof of first-order tableau soundness; no solution is supplied.

Source: content/first-order-logic/tableaux/soundness.tex, line 193.

Corollary: tableau theorems are valid

If A is a tableau theorem, then A is valid.

If A is a tableau theorem, then A is valid.

Source: content/first-order-logic/tableaux/soundness.tex, line 204.

Corollary: tableau derivability implies semantic entailment

If A is tableau-derivable from Gamma, then Gamma semantically entails A.

If A is tableau-derivable from Gamma, then Gamma semantically entails A.

Source: content/first-order-logic/tableaux/soundness.tex, line 209.

Corollary: satisfiable formula sets are consistent

If Gamma is satisfiable, then Gamma is consistent.

If Gamma is satisfiable, then Gamma is consistent.

Source: content/first-order-logic/tableaux/soundness.tex, line 225.

Definition of the identity tableau rules

The identity-reflexivity rule has no formula premise and adds t equals t carrying the true sign, for a closed term t. The true-identity substitution rule requires two formulas already on the branch: t one equals t two carrying the true sign, and A of t one carrying the true sign. It adds A of t two carrying the true sign. The false-identity substitution rule likewise requires true-signed t one equals t two and false-signed A of t one. It adds A of t two carrying the false sign. In each substitution rule, t, t one, and t two are closed terms, and both required premises remain available on the branch.

The identity-reflexivity rule has no formula premise and adds t equals t carrying the true sign, for a closed term t.
The true-identity substitution rule requires two formulas already on the branch: t one equals t two carrying the true sign, and A of t one carrying the true sign. It adds A of t two carrying the true sign.
The false-identity substitution rule likewise requires true-signed t one equals t two and false-signed A of t one. It adds A of t two carrying the false sign.
In each substitution rule, t, t one, and t two are closed terms, and both required premises remain available on the branch.

Source: content/first-order-logic/tableaux/identity.tex, line 16.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 20.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 27.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 34.

Examples of substitutability, symmetry, and transitivity of identity

The first closed tableau establishes substitutability of identicals: from s equals t and A of s, derive A of t by the true-identity rule. The second closed tableau establishes symmetry. From s one equals s two, add the reflexive identity s one equals s one, then use true identity to derive s two equals s one and close against its false-signed assumption. For that symmetry step, treat A of x as x equals s one, so A of s one is the reflexive identity and A of s two is the desired reversed identity. The third closed tableau establishes transitivity. From s one equals s two and s two equals s three, use true identity to derive s one equals s three and close against its false-signed assumption. For the transitivity step, line three supplies the identity premise and line two supplies A of s two, with A of x read as s one equals x.

The first closed tableau establishes substitutability of identicals: from s equals t and A of s, derive A of t by the true-identity rule.
The second closed tableau establishes symmetry. From s one equals s two, add the reflexive identity s one equals s one, then use true identity to derive s two equals s one and close against its false-signed assumption.
For that symmetry step, treat A of x as x equals s one, so A of s one is the reflexive identity and A of s two is the desired reversed identity.
The third closed tableau establishes transitivity. From s one equals s two and s two equals s three, use true identity to derive s one equals s three and close against its false-signed assumption.
For the transitivity step, line three supplies the identity premise and line two supplies A of s two, with A of x read as s one equals x.

Source: content/first-order-logic/tableaux/identity.tex, line 41.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 44.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 58.

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.

Source: content/first-order-logic/tableaux/identity.tex, line 75.

Exercise on quantified identity tableaux

Unsolved exercise. Give closed tableaux for the two source-listed quantified identity problems; no solution is supplied. Source-listed mathematical item one contains one formula: the complete formula for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis, carrying the false sign. Source-listed mathematical item two is one tableau-assumption set containing two simultaneous signed assumptions: the complete formula for some variable x, open parenthesis, the conjunction whose first conjunct is formula A with argument variable x; and whose second conjunct states that for every variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent states that variable y is identical to variable x, close parenthesis, close parenthesis, carrying the false sign; together with the complete formula the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis, carrying the true sign.

Unsolved source exercise; no solution added.

Unsolved exercise. Give closed tableaux for the two source-listed quantified identity problems; no solution is supplied.
Source-listed mathematical item one contains one formula: the complete formula for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis, carrying the false sign.
Source-listed mathematical item two is one tableau-assumption set containing two simultaneous signed assumptions: the complete formula for some variable x, open parenthesis, the conjunction whose first conjunct is formula A with argument variable x; and whose second conjunct states that for every variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent states that variable y is identical to variable x, close parenthesis, close parenthesis, carrying the false sign; together with the complete formula the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis, carrying the true sign.

Source: content/first-order-logic/tableaux/identity.tex, line 93.

Proposition: soundness of the identity tableau rules

Tableaux extended with the identity rules are sound: no closed tableau using those rules is satisfiable.

Tableaux extended with the identity rules are sound: no closed tableau using those rules is satisfiable.

Source: content/first-order-logic/tableaux/soundness-identity.tex, line 13.

14 source references

77 exact ordered proof-command bindings

Open the complete command binding ledger

Introduce the printed premise. source line 18.
Apply the printed tableau-rule label. source line 19.
Continue the branch with the printed conclusion. source line 20.
Display the completed proof tree. source line 21.
Introduce the printed premise. source line 23.
Apply the printed tableau-rule label. source line 24.
Continue the branch with the printed conclusion. source line 25.
Display the completed proof tree. source line 26.
Introduce the printed premise. source line 32.
Apply the printed tableau-rule label. source line 33.
Continue the branch with the printed conclusion. source line 34.
Suppress the inference line as printed. source line 35.
Continue the branch with the printed conclusion. source line 36.
Display the completed proof tree. source line 37.
Introduce the printed premise. source line 39.
Apply the printed tableau-rule label. source line 40.
Continue the branch with the printed conclusion. source line 41.
Display the completed proof tree. source line 42.
Introduce the printed premise. source line 48.
Apply the printed tableau-rule label. source line 49.
Continue the branch with the printed conclusion. source line 50.
Display the completed proof tree. source line 51.
Introduce the printed premise. source line 53.
Apply the printed tableau-rule label. source line 54.
Continue the branch with the printed conclusion. source line 55.
Suppress the inference line as printed. source line 56.
Continue the branch with the printed conclusion. source line 57.
Display the completed proof tree. source line 58.
Introduce the printed premise. source line 64.
Apply the printed tableau-rule label. source line 65.
Continue the branch with the printed conclusion. source line 66.
Display the completed proof tree. source line 67.
Introduce the printed premise. source line 69.
Apply the printed tableau-rule label. source line 70.
Continue the branch with the printed conclusion. source line 71.
Suppress the inference line as printed. source line 72.
Continue the branch with the printed conclusion. source line 73.
Display the completed proof tree. source line 74.
Introduce the printed premise. source line 80.
Apply the printed tableau-rule label. source line 81.
Continue the branch with the printed conclusion. source line 82.
Display the completed proof tree. source line 83.
Introduce the printed premise. source line 16.
Apply the printed tableau-rule label. source line 17.
Continue the branch with the printed conclusion. source line 18.
Display the completed proof tree. source line 19.
Introduce the printed premise. source line 21.
Apply the printed tableau-rule label. source line 22.
Continue the branch with the printed conclusion. source line 23.
Display the completed proof tree. source line 24.
Introduce the printed premise. source line 38.
Apply the printed tableau-rule label. source line 39.
Continue the branch with the printed conclusion. source line 40.
Display the completed proof tree. source line 41.
Introduce the printed premise. source line 43.
Apply the printed tableau-rule label. source line 44.
Continue the branch with the printed conclusion. source line 45.
Display the completed proof tree. source line 46.
Introduce the printed premise. source line 63.
Apply the printed tableau-rule label. source line 64.
Continue the branch with the printed conclusion. source line 65.
Introduce the printed premise. source line 17.
Apply the printed tableau-rule label. source line 18.
Continue the branch with the printed conclusion. source line 19.
Display the completed proof tree. source line 20.
Introduce the printed premise. source line 22.
Suppress the inference line as printed. source line 23.
Continue the branch with the printed conclusion. source line 24.
Apply the printed tableau-rule label. source line 25.
Continue the branch with the printed conclusion. source line 26.
Display the completed proof tree. source line 27.
Introduce the printed premise. source line 29.
Suppress the inference line as printed. source line 30.
Continue the branch with the printed conclusion. source line 31.
Apply the printed tableau-rule label. source line 32.
Continue the branch with the printed conclusion. source line 33.
Display the completed proof tree. source line 34.