The Open Logic Text — accessible offline edition

Tableaux — Explore equations

Tableaux

Reading preferences

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

Equation and object guide

All 166 stable expression records, 76 formal objects, 27 tableaux, nine proof trees, and four internal references are indexed here.

166 expression records

Expression 2

F(¬A∧¬B)→¬(A∨B)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 441, column 7

Expression 3

TBn

Conventional reading: the complete formula B sub n, carrying the true sign

Meaning here: The complete formula B sub n, 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
  1. Occurrence 1: provability-consistency.tex, line 116, column 45

Expression 4

Γ∪{FB}

Conventional reading: Gamma union the set containing the complete formula B, carrying the false sign

Meaning here: Gamma union the set containing the complete formula B, 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
  1. Occurrence 1: soundness.tex, line 94, column 36

Expression 5

TA→(B→C),FB→(A→C)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 423, column 7

Expression 6

FB∨C∈Γ

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

Meaning here: The complete formula B or 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
  1. Occurrence 1: soundness.tex, line 114, column 3

Expression 7

{TA,TB,FA∧B}

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

Meaning here: The set containing the complete formula A, carrying the true sign comma the complete formula B, carrying the true sign comma the complete formula A and B, 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
  1. Occurrence 1: provability-propositional.tex, line 60, column 44

Expression 10

Δ0={C1,…,Cn}⊆Δ

Conventional reading: Delta sub zero equals the set containing C sub one comma through the omitted intermediate entries comma C sub n is a subset of Delta

Meaning here: Delta sub zero equals the set containing C sub one comma through the omitted intermediate entries comma C sub n is a subset of Delta. This states the displayed finite-set inclusion.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 99, column 67

Expression 13

F¬(A∧¬A)

Conventional reading: the complete formula not open parenthesis A and not A close parenthesis, carrying the false sign

Meaning here: The complete formula not open parenthesis A and not A 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
  1. Occurrence 1: proving-things.tex, line 433, column 7

Expression 14

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
  1. Occurrence 1: provability-consistency.tex, line 95, column 8

Expression 16

A⊢B

Conventional reading: B is tableau-derivable from premise A

Meaning here: B is tableau-derivable from premise A. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 135, column 68

Expression 17

v

Conventional reading: valuation v

Meaning here: v is the propositional valuation assigning truth values to sentence letters.

12 occurrences
  1. Occurrence 1: soundness.tex, line 42, column 47
  2. Occurrence 2: soundness.tex, line 46, column 41
  3. Occurrence 3: soundness.tex, line 99, column 3
  4. Occurrence 4: soundness.tex, line 111, column 3
  5. Occurrence 5: soundness.tex, line 123, column 3
  6. Occurrence 6: soundness.tex, line 172, column 3
  7. Occurrence 7: soundness.tex, line 173, column 31
  8. Occurrence 8: soundness.tex, line 175, column 3
  9. Occurrence 9: soundness.tex, line 176, column 31
  10. Occurrence 10: soundness.tex, line 187, column 3
  11. Occurrence 11: soundness.tex, line 219, column 45
  12. Occurrence 12: soundness.tex, line 235, column 1

Expression 18

{FA,TA∧B}

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

Meaning here: The set containing the complete formula A, 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
  1. Occurrence 1: provability-propositional.tex, line 37, column 14

Expression 19

TA or FA.

Conventional reading: the complete formula A, carrying the true sign or the complete formula A, carrying the false sign period

Meaning here: The complete formula A, carrying the true sign or the complete formula A, carrying the false sign period. 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
  1. Occurrence 1: rules-and-proofs.tex, line 24, column 3

Expression 21

TA→B,T¬A→B,FB

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 453, column 7

Expression 22

T(A∨B)→C,FA→C

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 431, column 7

Expression 23

v⊨B∧C

Conventional reading: valuation v satisfies the complete conjunction B and C

Meaning here: Valuation v satisfies the complete conjunction B and C. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 108, column 3

Expression 24

{A∨B,¬A,¬B}

Conventional reading: the set containing A or B comma not A comma not B

Meaning here: The set containing A or B comma not A comma not B. This is the finite set of complete propositional formulas displayed by the source.

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

Expression 26

F¬A

Conventional reading: the complete formula not A, carrying the false sign

Meaning here: The complete formula not 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.

4 occurrences
  1. Occurrence 1: provability-consistency.tex, line 68, column 49
  2. Occurrence 2: provability-consistency.tex, line 70, column 28
  3. Occurrence 3: provability-consistency.tex, line 138, column 3
  4. Occurrence 4: provability-consistency.tex, line 139, column 6

Expression 27

{FA,TD1,…,TDm}

Conventional reading: the set containing the complete formula A, carrying the false sign comma the complete formula D sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula D sub m, carrying the true sign

Meaning here: The set containing the complete formula A, carrying the false sign comma the complete formula D sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula D 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 127, column 1

Expression 28

T¬B∈Γ

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

Meaning here: The complete formula not B, 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
  1. Occurrence 1: soundness.tex, line 93, column 3

Expression 29

TB∨C∈Γ

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

Meaning here: The complete formula B or 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
  1. Occurrence 1: soundness.tex, line 179, column 3

Expression 31

v⊨Bi

Conventional reading: valuation v satisfies B sub i

Meaning here: Valuation v satisfies B sub i. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 236, column 1

Expression 33

→T

Conventional reading: true-conditional tableau rule

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

1 occurrence
  1. Occurrence 1: soundness.tex, line 180, column 42

Expression 34

{FA∨B,TA}

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
  1. Occurrence 1: provability-propositional.tex, line 100, column 14

Expression 35

Reader projection

TA∨B,T¬B,FA

Frozen source MathML

TA∨B,¬B,FA

The source form is preserved; the reader projection is separately disclosed.

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

Meaning here: The intended exercise assumptions are true-signed A or B, true-signed not B, and false-signed A. The frozen source's malformed grouping is retained separately and disclosed by TR012-SOURCE-FORMULA-006.

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

Expression 36

{FB,TA→B,TA}

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

Meaning here: The set containing the complete formula B, carrying the false sign comma the complete formula A implies B, carrying the true 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
  1. Occurrence 1: provability-propositional.tex, line 136, column 11

Expression 41

FC

Conventional reading: the complete formula C, carrying the false sign

Meaning here: The complete formula C, 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.

4 occurrences
  1. Occurrence 1: soundness.tex, line 118, column 3
  2. Occurrence 2: soundness.tex, line 124, column 27
  3. Occurrence 3: soundness.tex, line 167, column 21
  4. Occurrence 4: soundness.tex, line 176, column 3

Expression 42

T¬(A→B),FA

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

Meaning here: The complete formula not open parenthesis A implies B close parenthesis, 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
  1. Occurrence 1: proving-things.tex, line 449, column 7

Expression 43

Reader projection

{FB,TA,TC1,…,TCn}has a closed tableau. If Γ⊢A then there is a finite set {D1,…,Dm}⊆Γ such that{FA,TD1,…,TDm}

Frozen source MathML

{FB,TA,TC1,…,TCn}has a closed tableau. If Γ⊢A then there are D1, …, Dm⊆Γ such that{FA,TD1,…,TDm}

The source form is preserved; the reader projection is separately disclosed.

Conventional reading: first tableau assumption set: false-signed B, true-signed A, and true-signed C sub one through C sub n; the source then states that this set has a closed tableau and, if A is derivable from Gamma, prints that D sub m is a subset of Gamma, which is malformed because D sub m is one formula; the disclosed reader interpretation instead selects the finite set D sub one through D sub m as a subset of Gamma and introduces a second closed tableau assumption set: false-signed A and true-signed D sub one through D sub m

Meaning here: The first tableau assumption set is false-signed B, true-signed A, and true-signed C sub one through C sub n. The frozen source then prints D sub m as a subset of Gamma. That printed relation is malformed because D sub m is a formula. The separately disclosed reader projection interprets the intended claim as the finite set containing D sub one through D sub m being a subset of Gamma, followed by the second tableau assumption set containing false-signed A and true-signed D sub one through D sub m.

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

Expression 45

FA∣TB

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

Meaning here: The complete formula A, carrying the false 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
  1. Occurrence 1: propositional-rules.tex, line 66, column 12

Expression 47

{TB1,…,TBn}

Conventional reading: the set containing the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign

Meaning here: The set containing the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, 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.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 183, column 7
  2. Occurrence 2: soundness.tex, line 233, column 17

Expression 48

v⊨C

Conventional reading: valuation v satisfies C

Meaning here: Valuation v satisfies C. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 110, column 3

Expression 49

Γ

Conventional reading: Gamma

Meaning here: Gamma is the set metavariable whose exact premise-set or signed-assumption-set role is fixed in each occurrence record.

28 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 39, column 15
  2. Occurrence 2: proof-theoretic-notions.tex, line 49, column 35
  3. Occurrence 3: proof-theoretic-notions.tex, line 54, column 24
  4. Occurrence 4: proof-theoretic-notions.tex, line 63, column 4
  5. Occurrence 5: proof-theoretic-notions.tex, line 72, column 52
  6. Occurrence 6: proof-theoretic-notions.tex, line 89, column 22
  7. Occurrence 7: proof-theoretic-notions.tex, line 142, column 1
  8. Occurrence 8: proof-theoretic-notions.tex, line 167, column 35
  9. Occurrence 9: proof-theoretic-notions.tex, line 168, column 22
  10. Occurrence 10: proof-theoretic-notions.tex, line 180, column 14
  11. Occurrence 11: provability-consistency.tex, line 21, column 22
  12. Occurrence 12: provability-consistency.tex, line 37, column 37
  13. Occurrence 13: provability-consistency.tex, line 80, column 58
  14. Occurrence 14: provability-consistency.tex, line 96, column 17
  15. Occurrence 15: provability-consistency.tex, line 97, column 6
  16. Occurrence 16: provability-consistency.tex, line 102, column 22
  17. Occurrence 17: provability-consistency.tex, line 115, column 31
  18. Occurrence 18: soundness.tex, line 47, column 40
  19. Occurrence 19: soundness.tex, line 48, column 29
  20. Occurrence 20: soundness.tex, line 55, column 6
  21. Occurrence 21: soundness.tex, line 55, column 41
  22. Occurrence 22: soundness.tex, line 67, column 18
  23. Occurrence 23: soundness.tex, line 67, column 34
  24. Occurrence 24: soundness.tex, line 82, column 5
  25. Occurrence 25: soundness.tex, line 85, column 46
  26. Occurrence 26: soundness.tex, line 227, column 4
  27. Occurrence 27: soundness.tex, line 231, column 44
  28. Occurrence 28: soundness.tex, line 237, column 6

Expression 50

⊢

Conventional reading: tableau derivability

Meaning here: Tableau derivability. 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
  1. Occurrence 1: provability-propositional.tex, line 19, column 51

Expression 51

TB→C∈Γ

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
  1. Occurrence 1: soundness.tex, line 181, column 3

Expression 53

{FA∨B,TB}

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

Meaning here: The set containing the complete formula A or B, carrying the false sign comma 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
  1. Occurrence 1: provability-propositional.tex, line 101, column 5

Expression 54

SiAi

Conventional reading: the complete formula A sub i, carrying sign S sub i

Meaning here: The complete formula A sub i, carrying sign S sub i. 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
  1. Occurrence 1: derivations.tex, line 29, column 3

Expression 55

TA∧B

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

Meaning here: 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
  1. Occurrence 1: proving-things.tex, line 50, column 1

Expression 58

F(A→¬A)→¬A

Conventional reading: the complete formula open parenthesis A implies not A close parenthesis implies not A, carrying the false sign

Meaning here: The complete formula open parenthesis A implies not A close parenthesis implies not 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
  1. Occurrence 1: proving-things.tex, line 435, column 7

Expression 60

F¬B∈Γ

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

Meaning here: The complete formula not B, 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
  1. Occurrence 1: soundness.tex, line 102, column 3

Expression 61

{T¬A,TB1,…,TBn}.

Conventional reading: the set containing the complete formula not A, carrying the true sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period

Meaning here: The set containing the complete formula not A, carrying the true sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period. 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
  1. Occurrence 1: provability-consistency.tex, line 54, column 1

Expression 63

TA→C,F¬(A∧¬C)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 437, column 7

Expression 64

T¬(A∧B),F¬A∨¬B

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 450, column 7

Expression 67

Γ⊢¬A

Conventional reading: not A is tableau-derivable from Gamma

Meaning here: Not A is tableau-derivable from Gamma. 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
  1. Occurrence 1: provability-consistency.tex, line 76, column 12

Expression 68

F¬(A→B)→¬B

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

Meaning here: The complete formula not open parenthesis A implies B close parenthesis implies not B, 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
  1. Occurrence 1: proving-things.tex, line 436, column 7

Expression 69

TB∧C∈Γ

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

Meaning here: The complete formula B and 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
  1. Occurrence 1: soundness.tex, line 104, column 3

Expression 70

FB∧C∈Γ

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
  1. Occurrence 1: soundness.tex, line 165, column 3

Expression 71

{FB,TA∧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
  1. Occurrence 1: provability-propositional.tex, line 38, column 5

Expression 72

A1,…,An⊢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
  1. Occurrence 1: proof-theoretic-notions.tex, line 136, column 64

Expression 73

{TA∨B,T¬A,T¬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
  1. Occurrence 1: provability-propositional.tex, line 84, column 41

Expression 74

TA∣TB

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
  1. Occurrence 1: propositional-rules.tex, line 50, column 12

Expression 75

F(A→B)∨(B→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
  1. Occurrence 1: proving-things.tex, line 456, column 7

Expression 76

B⊢A→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
  1. Occurrence 1: provability-propositional.tex, line 130, column 44

Expression 77

TB∧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
  1. Occurrence 1: proving-things.tex, line 301, column 31

Expression 79

A

Conventional reading: A

Meaning here: A is a metavariable for the complete propositional formula under discussion.

18 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 29, column 53
  2. Occurrence 2: rules-and-proofs.tex, line 30, column 38
  3. Occurrence 3: rules-and-proofs.tex, line 54, column 32
  4. Occurrence 4: rules-and-proofs.tex, line 56, column 19
  5. Occurrence 5: rules-and-proofs.tex, line 56, column 63
  6. Occurrence 6: derivations.tex, line 49, column 65
  7. Occurrence 7: derivations.tex, line 51, column 43
  8. Occurrence 8: proof-theoretic-notions.tex, line 32, column 16
  9. Occurrence 9: proof-theoretic-notions.tex, line 33, column 65
  10. Occurrence 10: proof-theoretic-notions.tex, line 38, column 16
  11. Occurrence 11: proof-theoretic-notions.tex, line 49, column 4
  12. Occurrence 12: proof-theoretic-notions.tex, line 117, column 26
  13. Occurrence 13: proof-theoretic-notions.tex, line 143, column 16
  14. Occurrence 14: provability-consistency.tex, line 33, column 55
  15. Occurrence 15: soundness.tex, line 22, column 27
  16. Occurrence 16: soundness.tex, line 71, column 30
  17. Occurrence 17: soundness.tex, line 206, column 22
  18. Occurrence 18: soundness.tex, line 220, column 43

Expression 80

¬T

Conventional reading: true-negation tableau rule

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

6 occurrences
  1. Occurrence 1: derivations.tex, line 81, column 18
  2. Occurrence 2: proving-things.tex, line 144, column 5
  3. Occurrence 3: provability-consistency.tex, line 52, column 11
  4. Occurrence 4: provability-consistency.tex, line 130, column 6
  5. Occurrence 5: provability-consistency.tex, line 131, column 17
  6. Occurrence 6: soundness.tex, line 92, column 42

Expression 81

B⊢A∨B

Conventional reading: A or B is tableau-derivable from premise B

Meaning here: A or 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
  1. Occurrence 1: provability-propositional.tex, line 78, column 42

Expression 82

{TB1,…,TBn}.

Conventional reading: the set containing the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period

Meaning here: The set containing the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 57, column 1

Expression 84

S1A1

Conventional reading: the complete formula A sub one, carrying sign S sub one

Meaning here: The complete formula A sub one, carrying sign S sub one. 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
  1. Occurrence 1: derivations.tex, line 24, column 31

Expression 85

v⊨Γ

Conventional reading: valuation v satisfies every formula in Gamma

Meaning here: Valuation v satisfies every formula in Gamma. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

6 occurrences
  1. Occurrence 1: soundness.tex, line 96, column 3
  2. Occurrence 2: soundness.tex, line 107, column 3
  3. Occurrence 3: soundness.tex, line 119, column 3
  4. Occurrence 4: soundness.tex, line 168, column 3
  5. Occurrence 5: soundness.tex, line 184, column 31
  6. Occurrence 6: soundness.tex, line 221, column 3

Expression 86

Γ⊢Ai

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

Meaning here: A sub i is tableau-derivable from Gamma. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 137, column 29

Expression 87

F¬(A∨B)→(¬A∧¬B)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 442, column 7

Expression 89

F¬¬A→A

Conventional reading: the complete formula not not A implies A, carrying the false sign

Meaning here: The complete formula not not A implies 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
  1. Occurrence 1: proving-things.tex, line 452, column 7

Expression 91

TB→A,F¬A→¬B

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

Meaning here: The complete formula B implies A, carrying the true sign comma the complete formula not A implies not B, 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
  1. Occurrence 1: proving-things.tex, line 434, column 7

Expression 92

{TA∨(B∧C),F(A∨B)∧(A∨C)}

Conventional reading: the set containing the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign

Meaning here: The set containing the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign comma the complete formula open parenthesis A or B close parenthesis and open parenthesis A or 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
  1. Occurrence 1: proving-things.tex, line 178, column 1

Expression 95

T(A→B)→A,FA

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
  1. Occurrence 1: proving-things.tex, line 455, column 7

Expression 97

{FA,TB1,…,TBn}

Conventional reading: the set containing the complete formula A, carrying the false sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign

Meaning here: The set containing the complete formula A, carrying the false sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, 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.

4 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 176, column 7
  2. Occurrence 2: provability-consistency.tex, line 48, column 1
  3. Occurrence 3: provability-consistency.tex, line 87, column 3
  4. Occurrence 4: soundness.tex, line 216, column 12

Expression 98

T(A→C)∧(B→C),F(A∨B)→C

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 432, column 7

Expression 99

{TA,TB1,…,TBn} and{T¬A,TC1,…,TCm}

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
  1. Occurrence 1: provability-consistency.tex, line 108, column 3

Expression 101

TA→B,F¬A∨B

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

Meaning here: The complete formula A implies B, carrying the true sign comma the complete formula not A or B, 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
  1. Occurrence 1: proving-things.tex, line 451, column 7

Expression 102

TA∧(B∧C),F(A∧B)∧C

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 421, column 7

Expression 103

SA∈Γ

Conventional reading: the complete formula A, carrying sign S belongs to Gamma

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
  1. Occurrence 1: soundness.tex, line 48, column 1
  2. Occurrence 2: soundness.tex, line 83, column 5

Expression 107

SnAn

Conventional reading: the complete formula A sub n, carrying sign S sub n

Meaning here: The complete formula A sub n, carrying sign S sub n. 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
  1. Occurrence 1: derivations.tex, line 25, column 1

Expression 109

{FA,TB1,…,TBn}{TA,TC1,…,TCm}

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

Meaning here: Two tableau rows: first, false-signed A together with true-signed B sub one through B sub n; second, true-signed 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
  1. Occurrence 1: provability-consistency.tex, line 27, column 3

Expression 110

A,B⊢A∧B

Conventional reading: A and B is tableau-derivable from the two premises A and B

Meaning here: A and B is tableau-derivable from the two premises A and 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
  1. Occurrence 1: provability-propositional.tex, line 30, column 47

Expression 112

{FA,TB1,…,TBn}.

Conventional reading: the set containing the complete formula A, carrying the false sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period

Meaning here: The set containing the complete formula A, carrying the false sign comma the complete formula B sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula B sub n, carrying the true sign period. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 42, column 1

Expression 113

TCm

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
  1. Occurrence 1: provability-consistency.tex, line 117, column 47

Expression 114

T¬A

Conventional reading: the complete formula not A, carrying the true sign

Meaning here: 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.

9 occurrences
  1. Occurrence 1: derivations.tex, line 64, column 44
  2. Occurrence 2: derivations.tex, line 80, column 20
  3. Occurrence 3: provability-consistency.tex, line 62, column 12
  4. Occurrence 4: provability-consistency.tex, line 65, column 12
  5. Occurrence 5: provability-consistency.tex, line 68, column 12
  6. Occurrence 6: provability-consistency.tex, line 130, column 32
  7. Occurrence 7: provability-consistency.tex, line 131, column 43
  8. Occurrence 8: provability-consistency.tex, line 136, column 18
  9. Occurrence 9: provability-consistency.tex, line 145, column 3

Expression 115

v⊭B→C

Conventional reading: valuation v does not satisfy the complete conditional from B to C

Meaning here: Valuation v does not satisfy the complete conditional from B to C. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 120, column 3

Expression 117

TA∨(B∨C),F(A∨B)∨C

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 422, column 7

Expression 119

TA∧¬C,F¬(A→C)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 438, column 7

Expression 120

Γ0∪Γ1⊆Γ

Conventional reading: Gamma sub zero union Gamma sub one is a subset of Gamma

Meaning here: Gamma sub zero union Gamma sub one is a subset of Gamma. This states the displayed finite-set inclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 36, column 54

Expression 121

FA

Conventional reading: the complete formula A, carrying the false sign

Meaning here: 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.

20 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 30, column 12
  2. Occurrence 2: rules-and-proofs.tex, line 45, column 5
  3. Occurrence 3: rules-and-proofs.tex, line 47, column 48
  4. Occurrence 4: rules-and-proofs.tex, line 52, column 24
  5. Occurrence 5: rules-and-proofs.tex, line 55, column 6
  6. Occurrence 6: propositional-rules.tex, line 88, column 43
  7. Occurrence 7: derivations.tex, line 35, column 25
  8. Occurrence 8: derivations.tex, line 46, column 27
  9. Occurrence 9: proving-things.tex, line 67, column 5
  10. Occurrence 10: proving-things.tex, line 145, column 4
  11. Occurrence 11: proof-theoretic-notions.tex, line 33, column 17
  12. Occurrence 12: proof-theoretic-notions.tex, line 118, column 38
  13. Occurrence 13: provability-consistency.tex, line 63, column 23
  14. Occurrence 14: provability-consistency.tex, line 65, column 45
  15. Occurrence 15: provability-consistency.tex, line 72, column 1
  16. Occurrence 16: provability-consistency.tex, line 120, column 3
  17. Occurrence 17: provability-consistency.tex, line 132, column 3
  18. Occurrence 18: provability-consistency.tex, line 142, column 3
  19. Occurrence 19: soundness.tex, line 45, column 1
  20. Occurrence 20: soundness.tex, line 70, column 25

Expression 122

⊬A

Conventional reading: A is not a tableau theorem

Meaning here: A is not a tableau theorem. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 34, column 18

Expression 124

¬A⊢A→B

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

Meaning here: The conditional from A to B is tableau-derivable from premise not A. 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
  1. Occurrence 1: provability-propositional.tex, line 130, column 10

Expression 125

v⊭B∧C

Conventional reading: valuation v does not satisfy the complete conjunction B and C

Meaning here: Valuation v does not satisfy the complete conjunction B and C. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 169, column 3

Expression 126

Γ⊢A

Conventional reading: A is tableau-derivable from Gamma

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

15 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 39, column 25
  2. Occurrence 2: proof-theoretic-notions.tex, line 68, column 26
  3. Occurrence 3: proof-theoretic-notions.tex, line 84, column 34
  4. Occurrence 4: proof-theoretic-notions.tex, line 94, column 4
  5. Occurrence 5: proof-theoretic-notions.tex, line 135, column 44
  6. Occurrence 6: proof-theoretic-notions.tex, line 142, column 30
  7. Occurrence 7: proof-theoretic-notions.tex, line 165, column 12
  8. Occurrence 8: proof-theoretic-notions.tex, line 174, column 14
  9. Occurrence 9: provability-consistency.tex, line 20, column 6
  10. Occurrence 10: provability-consistency.tex, line 42, column 1
  11. Occurrence 11: provability-consistency.tex, line 46, column 15
  12. Occurrence 12: provability-consistency.tex, line 80, column 6
  13. Occurrence 13: provability-consistency.tex, line 85, column 11
  14. Occurrence 14: soundness.tex, line 211, column 4
  15. Occurrence 15: soundness.tex, line 215, column 6

Expression 127

T¬A∨¬B,F¬(A∧B)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 440, column 7

Expression 129

TA∣FA

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

Meaning here: The complete formula A, carrying the true sign separate branch 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
  1. Occurrence 1: propositional-rules.tex, line 82, column 12

Expression 133

TC1

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

Meaning here: The complete formula C sub one, 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
  1. Occurrence 1: provability-consistency.tex, line 117, column 17

Expression 134

{FB,TA,TC1,…,TCn}

Conventional reading: the set containing the complete formula B, carrying the false sign comma the complete formula A, carrying the true sign comma the complete formula C sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula C sub n, carrying the true sign

Meaning here: The set containing the complete formula B, carrying the false sign comma the complete formula A, carrying the true sign comma the complete formula C sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula C sub n, 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 120, column 1

Expression 135

Δ⊢A

Conventional reading: A is tableau-derivable from Delta

Meaning here: A is tableau-derivable from Delta. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 84, column 60

Expression 136

A⊢A∨B

Conventional reading: A or B is tableau-derivable from premise A

Meaning here: A or B is tableau-derivable from premise A. 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
  1. Occurrence 1: provability-propositional.tex, line 78, column 14

Expression 137

FB,TC1,…,TCn,TD1,…,TDm.

Conventional reading: the complete formula B, carrying the false sign comma the complete formula C sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula C sub n, carrying the true sign comma the complete formula D sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula D sub m, carrying the true sign period

Meaning here: The complete formula B, carrying the false sign comma the complete formula C sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula C sub n, carrying the true sign comma the complete formula D sub one, carrying the true sign comma through the omitted intermediate entries comma the complete formula D sub m, carrying the true sign period. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 112, column 1

Expression 138

TA

Conventional reading: the complete formula A, carrying the true sign

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
  1. Occurrence 1: rules-and-proofs.tex, line 29, column 28
  2. Occurrence 2: rules-and-proofs.tex, line 44, column 49
  3. Occurrence 3: rules-and-proofs.tex, line 47, column 24
  4. Occurrence 4: rules-and-proofs.tex, line 51, column 37
  5. Occurrence 5: propositional-rules.tex, line 88, column 12
  6. Occurrence 6: derivations.tex, line 35, column 1
  7. Occurrence 7: derivations.tex, line 46, column 3
  8. Occurrence 8: derivations.tex, line 64, column 20
  9. Occurrence 9: proving-things.tex, line 66, column 36
  10. Occurrence 10: proof-theoretic-notions.tex, line 118, column 1
  11. Occurrence 11: proof-theoretic-notions.tex, line 126, column 1
  12. Occurrence 12: provability-consistency.tex, line 71, column 1
  13. Occurrence 13: provability-consistency.tex, line 119, column 31
  14. Occurrence 14: provability-consistency.tex, line 125, column 13
  15. Occurrence 15: provability-consistency.tex, line 126, column 9
  16. Occurrence 16: provability-consistency.tex, line 139, column 43
  17. Occurrence 17: soundness.tex, line 43, column 38
  18. Occurrence 18: soundness.tex, line 70, column 1

Expression 142

TA,F¬¬A

Conventional reading: the complete formula A, carrying the true sign comma the complete formula not not A, carrying the false sign

Meaning here: The complete formula A, carrying the true sign comma the complete formula not not 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
  1. Occurrence 1: proving-things.tex, line 424, column 7

Expression 144

FB

Conventional reading: the complete formula B, carrying the false sign

Meaning here: The complete formula B, 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.

4 occurrences
  1. Occurrence 1: soundness.tex, line 100, column 3
  2. Occurrence 2: soundness.tex, line 166, column 43
  3. Occurrence 3: soundness.tex, line 173, column 3
  4. Occurrence 4: soundness.tex, line 184, column 3

Expression 145

TA∧¬A

Conventional reading: the complete formula A and not A, carrying the true sign

Meaning here: The complete formula A and 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
  1. Occurrence 1: derivations.tex, line 54, column 41

Expression 148

FB→C∈Γ

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

Meaning here: The complete formula B implies 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
  1. Occurrence 1: soundness.tex, line 116, column 3

Expression 149

(¬A∨B)→(A→B)

Conventional reading: open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis

Meaning here: Open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis. This is the complete propositional formula; its explicit parentheses determine logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 73, column 41

Expression 150

{FA→B,TB}

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

Meaning here: The set containing the complete formula A implies B, carrying the false sign comma 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
  1. Occurrence 1: provability-propositional.tex, line 149, column 38

Expression 151

Γ1={C1,…,Cn}⊆Γ

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

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

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

Expression 152

TB

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

Meaning here: 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.

5 occurrences
  1. Occurrence 1: soundness.tex, line 105, column 38
  2. Occurrence 2: soundness.tex, line 112, column 3
  3. Occurrence 3: soundness.tex, line 117, column 38
  4. Occurrence 4: soundness.tex, line 124, column 3
  5. Occurrence 5: soundness.tex, line 183, column 18

Expression 153

FA∣FB

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

Meaning here: The complete formula A, carrying the false sign separate branch the complete formula B, 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
  1. Occurrence 1: propositional-rules.tex, line 41, column 12

Expression 155

∧T1

Conventional reading: true-conjunction tableau rule, applied to line one

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

1 occurrence
  1. Occurrence 1: derivations.tex, line 76, column 23

Expression 156

A∧B⊢B

Conventional reading: B is tableau-derivable from the single conjunctive premise A and B

Meaning here: B is tableau-derivable from the single conjunctive premise A and 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
  1. Occurrence 1: provability-propositional.tex, line 29, column 13

Expression 157

Γ⊬A

Conventional reading: A is not tableau-derivable from Gamma

Meaning here: A is not tableau-derivable from Gamma. 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
  1. Occurrence 1: proof-theoretic-notions.tex, line 49, column 53

Expression 158

v⊨¬B

Conventional reading: valuation v satisfies not B

Meaning here: Valuation v satisfies not B. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

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

Expression 159

TB1

Conventional reading: the complete formula B sub one, carrying the true sign

Meaning here: The complete formula B sub one, 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
  1. Occurrence 1: provability-consistency.tex, line 116, column 15

Expression 160

T(A∧B)→C,F(A→C)∨(B→C)

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

Meaning here: 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. 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
  1. Occurrence 1: proving-things.tex, line 454, column 7

Expression 162

{FA→B,T¬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
  1. Occurrence 1: provability-propositional.tex, line 148, column 16

Expression 164

v⊭A

Conventional reading: valuation v does not satisfy A

Meaning here: Valuation v does not satisfy A. This states exactly whether the named propositional valuation satisfies the complete formula or premise set.

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

Thirty-six tableaux and proof trees

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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.

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

Words-only linearization: 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.

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

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

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

Words-only linearization: Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption. This source tableau has one node and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule one. Node three, continuing the branch below node two: the complete formula not A, carrying the true sign. Printed justification: true-conjunction tableau rule one. This source tableau has three nodes and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula A and not A, carrying the true sign. Printed justification: assumption. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule one. Node three, continuing the branch below node two: the complete formula not A, carrying the true sign. Printed justification: true-conjunction tableau rule one. Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule three. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption. This source tableau has one node and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: false-conditional tableau rule one. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-conditional tableau rule one. This source tableau has three nodes and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula A and B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-conditional tableau rule one. Node four, continuing the branch below node three: the complete formula A, carrying the true sign. Printed justification: true-conjunction tableau rule two. Node five, continuing the branch below node four: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node. This source tableau has five nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This source tableau has one node and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. This source tableau has three nodes and one terminal branch; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. Node three splits into two branches. Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two. Node five, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two. This source tableau has five nodes and two terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three splits into two branches. Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two. Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. Node seven, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two. Node eight, continuing the branch below node seven: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three. Node nine, continuing the branch below node eight: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. The branch closes at this node. This source tableau has nine nodes and two terminal branches; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula not A or B, carrying the true sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three, continuing the branch below node two: the complete formula open parenthesis A implies B close parenthesis, carrying the false sign. Printed justification: false-conditional tableau rule one. This node is marked checked. Node three splits into two branches. Node four, on the left branch below node three: the complete formula not A, carrying the true sign. Printed justification: true-disjunction tableau rule two. Node five, continuing the branch below node four: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. Node seven, continuing the branch below node six: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule four. The branch closes at this node. Node eight, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule two. Node nine, continuing the branch below node eight: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule three. Node ten, continuing the branch below node nine: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule three. The branch closes at this node. This source tableau has ten nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node four, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This source tableau has four nodes and two terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node three splits into two branches. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. Node five, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. Node six, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node six splits into two branches. Node seven, on the left branch below node six: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. Node eight, on the right branch below node six: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This source tableau has eight nodes and four terminal branches; zero terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
  2. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
  3. Node two splits into two branches.
  4. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
  5. Node three splits into two branches.
  6. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  7. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  8. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
  9. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.
  10. Node eight, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.
  11. Node eight splits into two branches.
  12. Node nine, on the left branch below node eight: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  13. Node ten, continuing the branch below node nine: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  14. Node eleven, continuing the branch below node ten: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  15. Node twelve, on the right branch below node eight: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two.

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node three splits into two branches. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. Node eight, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node eight splits into two branches. Node nine, on the left branch below node eight: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node ten, continuing the branch below node nine: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node eleven, continuing the branch below node ten: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node twelve, on the right branch below node eight: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This source tableau has twelve nodes and four terminal branches; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
  2. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
  3. Node two splits into two branches.
  4. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
  5. Node three splits into two branches.
  6. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  7. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  8. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
  9. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  10. Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity.
  11. Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
  12. Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one.
  13. Node ten splits into two branches.
  14. Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  15. Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  16. Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  17. Node fourteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  18. Node fifteen, continuing the branch below node fourteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity.
  19. Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four.

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node three splits into two branches. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity. Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node. Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node ten splits into two branches. Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node fourteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node fifteen, continuing the branch below node fourteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. The printed tableau moves this node downward by two positions for visual clarity. Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. This source tableau has sixteen nodes and four terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
  2. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
  3. Node two splits into two branches.
  4. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one.
  5. Node three splits into two branches.
  6. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  7. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  8. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
  9. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  10. Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  11. Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node.
  12. Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
  13. Node ten splits into two branches.
  14. Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  15. Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  16. Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  17. Node fourteen, continuing the branch below node thirteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three.
  18. Node fifteen, continuing the branch below node fourteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node.
  19. Node sixteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  20. Node seventeen, continuing the branch below node sixteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  21. Node eighteen, continuing the branch below node seventeen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four.
  22. Node nineteen, continuing the branch below node eighteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three.
  23. Node twenty, continuing the branch below node nineteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. Node three splits into two branches. Node four, on the left branch below node three: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node six, continuing the branch below node five: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node. Node seven, on the right branch below node three: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node eight, continuing the branch below node seven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node nine, continuing the branch below node eight: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. The branch closes at this node. Node ten, on the right branch below node two: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked. Node ten splits into two branches. Node eleven, on the left branch below node ten: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node twelve, continuing the branch below node eleven: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node thirteen, continuing the branch below node twelve: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node fourteen, continuing the branch below node thirteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three. Node fifteen, continuing the branch below node fourteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node. Node sixteen, on the right branch below node ten: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node seventeen, continuing the branch below node sixteen: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node eighteen, continuing the branch below node seventeen: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule four. Node nineteen, continuing the branch below node eighteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule three. Node twenty, continuing the branch below node nineteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule three. The branch closes at this node. This source tableau has twenty nodes and four terminal branches; four terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked.
  2. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked.
  3. Node two splits into two branches.
  4. Node three, on the left branch below node two: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  5. Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three.
  6. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule three.
  7. Node five splits into two branches.
  8. Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
  9. Node seven, on the right branch below node five: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
  10. Node eight, continuing the branch below node seven: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six.
  11. Node nine, continuing the branch below node eight: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node.
  12. Node ten, on the right branch below node two: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked.
  13. Node eleven, continuing the branch below node ten: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three.
  14. Node twelve, continuing the branch below node eleven: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule three.
  15. Node twelve splits into two branches.
  16. Node thirteen, on the left branch below node twelve: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
  17. Node fourteen, on the right branch below node twelve: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked.
  18. Node fifteen, continuing the branch below node fourteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six.
  19. Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign. Printed justification: assumption. This node is marked checked. Node two, continuing the branch below node one: the complete formula open parenthesis A or B close parenthesis and open parenthesis A or C close parenthesis, carrying the false sign. Printed justification: assumption. This node is marked checked. Node two splits into two branches. Node three, on the left branch below node two: the complete formula A or B, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule three. Node five splits into two branches. Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node. Node seven, on the right branch below node five: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked. Node eight, continuing the branch below node seven: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six. Node nine, continuing the branch below node eight: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node. Node ten, on the right branch below node two: the complete formula A or C, carrying the false sign. Printed justification: false-conjunction tableau rule two. This node is marked checked. Node eleven, continuing the branch below node ten: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule three. Node twelve, continuing the branch below node eleven: the complete formula C, carrying the false sign. Printed justification: false-disjunction tableau rule three. Node twelve splits into two branches. Node thirteen, on the left branch below node twelve: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node. Node fourteen, on the right branch below node twelve: the complete formula B and C, carrying the true sign. Printed justification: true-disjunction tableau rule one. This node is marked checked. Node fifteen, continuing the branch below node fourteen: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule six. Node sixteen, continuing the branch below node fifteen: the complete formula C, carrying the true sign. Printed justification: true-conjunction tableau rule six. The branch closes at this node. This source tableau has sixteen nodes and four terminal branches; four terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: 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. This source tableau has two nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: 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 and 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 two. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

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

Words-only linearization: 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 A and 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 two. Node four, continuing the branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conjunction tableau rule two. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A and B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula B, carrying the true sign. Printed justification: assumption.
  4. Node three splits into two branches.
  5. Node four, on the left branch below node three: the complete formula A, carrying the false sign. Printed justification: false-conjunction tableau rule one. The branch closes at this node.
  6. Node five, on the right branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conjunction tableau rule one. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A and 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 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 one. The branch closes at this node. This source tableau has five nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

Closed tableau beginning with the complete formula A or B, carrying the true sign

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

  1. Node one, at the root: the complete formula A or B, carrying the true sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula not A, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula not B, carrying the true sign. Printed justification: assumption.
  4. Node four, continuing the branch below node three: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule two.
  5. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: true-negation tableau rule three.
  6. Node five splits into two branches.
  7. Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.
  8. Node seven, on the right branch below node five: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A or B, carrying the true sign. Printed justification: assumption. Node two, continuing the branch below node one: the complete formula not A, carrying the true sign. Printed justification: assumption. Node three, continuing the branch below node two: the complete formula not 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 two. Node five, continuing the branch below node four: the complete formula B, carrying the false sign. Printed justification: true-negation tableau rule three. Node five splits into two branches. Node six, on the left branch below node five: the complete formula A, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node. Node seven, on the right branch below node five: the complete formula B, carrying the true sign. Printed justification: true-disjunction tableau rule one. The branch closes at this node. This source tableau has seven nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula A, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule one.
  4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A or 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 one. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A or B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula A, carrying the false sign. Printed justification: false-disjunction tableau rule one.
  4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A or 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 one. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-disjunction tableau rule one. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula A implies B, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: assumption.
  4. Node three splits into two branches.
  5. Node four, on the left branch below node three: the complete formula A, carrying the false sign. Printed justification: true-conditional tableau rule two. The branch closes at this node.
  6. Node five, on the right branch below node three: the complete formula B, carrying the true sign. Printed justification: true-conditional tableau rule two. The branch closes at this node.

Words-only linearization: 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 A implies 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 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 two. The branch closes at this node. This source tableau has five nodes and two terminal branches; two terminal branches are explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A implies B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula not A, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule one.
  4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one.
  5. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule two. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A implies B, carrying the false sign. Printed justification: assumption. Node two, continuing the branch below node one: the complete formula not 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 one. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one. Node five, continuing the branch below node four: the complete formula A, carrying the false sign. Printed justification: true-negation tableau rule two. The branch closes at this node. This source tableau has five nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

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

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

  1. Node one, at the root: the complete formula A implies B, carrying the false sign. Printed justification: assumption.
  2. Node two, continuing the branch below node one: the complete formula B, carrying the true sign. Printed justification: assumption.
  3. Node three, continuing the branch below node two: the complete formula A, carrying the true sign. Printed justification: false-conditional tableau rule one.
  4. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one. The branch closes at this node.

Words-only linearization: Node one, at the root: the complete formula A implies 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 one. Node four, continuing the branch below node three: the complete formula B, carrying the false sign. Printed justification: false-conditional tableau rule one. The branch closes at this node. This source tableau has four nodes and one terminal branch; one terminal branch is explicitly marked closed. It preserves every printed assumption, truth sign, rule citation, line reference, checkmark, branch split, and closure marker in deterministic preorder.

76 formal objects

  1. Definition of a signed formula — rules-and-proofs.tex, line 21.
  2. Definition of the negation tableau rules — propositional-rules.tex, line 17.
  3. True-negation tableau rule — propositional-rules.tex, line 18.
  4. False-negation tableau rule — propositional-rules.tex, line 23.
  5. Definition of the conjunction tableau rules — propositional-rules.tex, line 31.
  6. True-conjunction tableau rule — propositional-rules.tex, line 32.
  7. False-conjunction branching tableau rule — propositional-rules.tex, line 39.
  8. Definition of the disjunction tableau rules — propositional-rules.tex, line 47.
  9. True-disjunction branching tableau rule — propositional-rules.tex, line 48.
  10. False-disjunction tableau rule — propositional-rules.tex, line 53.
  11. Definition of the conditional tableau rules — propositional-rules.tex, line 63.
  12. True-conditional branching tableau rule — propositional-rules.tex, line 64.
  13. False-conditional tableau rule — propositional-rules.tex, line 69.
  14. Definition of the cut tableau rule — propositional-rules.tex, line 79.
  15. Cut branching rule — propositional-rules.tex, line 80.
  16. Definition of a tableau derivation — derivations.tex, line 23.
  17. Example of extending a tableau derivation — derivations.tex, line 42.
  18. Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign — derivations.tex, line 58.
  19. Open or intermediate tableau beginning with the complete formula A and not A, carrying the true sign, later construction stage two — derivations.tex, line 66.
  20. Closed tableau beginning with the complete formula A and not A, carrying the true sign — derivations.tex, line 84.
  21. Example proving that if A and B then A — proving-things.tex, line 15.
  22. Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign — proving-things.tex, line 20.
  23. Open or intermediate tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign, later construction stage two — proving-things.tex, line 30.
  24. Closed tableau beginning with the complete formula open parenthesis A and B close parenthesis implies A, carrying the false sign — proving-things.tex, line 52.
  25. Example proving a nested conditional by tableau — proving-things.tex, line 72.
  26. Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign — proving-things.tex, line 77.
  27. Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage two — proving-things.tex, line 84.
  28. Open or intermediate tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign, later construction stage three — proving-things.tex, line 102.
  29. Partially closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign — proving-things.tex, line 122.
  30. Closed tableau beginning with the complete formula open parenthesis not A or B close parenthesis implies open parenthesis A implies B close parenthesis, carrying the false sign — proving-things.tex, line 146.
  31. Example closing a branching tableau — proving-things.tex, line 173.
  32. Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign — proving-things.tex, line 181.
  33. Open or intermediate tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two — proving-things.tex, line 195.
  34. Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign — proving-things.tex, line 218.
  35. Partially closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two — proving-things.tex, line 251.
  36. Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign — proving-things.tex, line 304.
  37. Closed tableau beginning with the complete formula A or open parenthesis B and C close parenthesis, carrying the true sign, later construction stage two — proving-things.tex, line 366.
  38. Exercise on associativity and double negation tableaux — proving-things.tex, line 418; preserved unsolved prompt.
  39. Exercise on equivalences and De Morgan tableaux — proving-things.tex, line 428; preserved unsolved prompt.
  40. Exercise on conditional and negation tableaux — proving-things.tex, line 446; preserved unsolved prompt.
  41. Definition of tableau theoremhood — proof-theoretic-notions.tex, line 31.
  42. Definition of tableau derivability — proof-theoretic-notions.tex, line 37.
  43. Definition of tableau consistency — proof-theoretic-notions.tex, line 53.
  44. Proposition: reflexivity of tableau derivability — proof-theoretic-notions.tex, line 66.
  45. Closed tableau beginning with the complete formula A, carrying the false sign — proof-theoretic-notions.tex, line 73.
  46. Proposition: monotonicity of tableau derivability — proof-theoretic-notions.tex, line 82.
  47. Proposition: transitivity of tableau derivability — proof-theoretic-notions.tex, line 92.
  48. Two closed-tableau assumption sets used for transitivity — proof-theoretic-notions.tex, line 101.
  49. Proposition characterizing inconsistency by derivability — proof-theoretic-notions.tex, line 140.
  50. Exercise proving the inconsistency characterization — proof-theoretic-notions.tex, line 157; preserved unsolved prompt.
  51. Proposition: compactness of tableau derivability and consistency — proof-theoretic-notions.tex, line 162.
  52. Proposition combining derivability with inconsistency — provability-consistency.tex, line 19.
  53. Paired closed-tableau assumptions in the combination proof — provability-consistency.tex, line 27.
  54. Proposition relating derivability to inconsistency after adding not A — provability-consistency.tex, line 40.
  55. Exercise proving the dual inconsistency equivalence — provability-consistency.tex, line 75; preserved unsolved prompt.
  56. Proposition deriving inconsistency from A and not A — provability-consistency.tex, line 79.
  57. Proposition combining two inconsistent extensions of Gamma — provability-consistency.tex, line 100.
  58. Two closed-tableau rows for the cut construction — provability-consistency.tex, line 108.
  59. Proposition: tableau derivability rules for conjunction — provability-propositional.tex, line 26.
  60. Closed tableau beginning with the complete formula A, carrying the false sign, later construction stage two — provability-propositional.tex, line 40.
  61. Closed tableau beginning with the complete formula B, carrying the false sign — provability-propositional.tex, line 50.
  62. Closed tableau beginning with the complete formula A and B, carrying the false sign — provability-propositional.tex, line 62.
  63. Proposition: tableau derivability rules for disjunction — provability-propositional.tex, line 75.
  64. Closed tableau beginning with the complete formula A or B, carrying the true sign — provability-propositional.tex, line 86.
  65. Closed tableau beginning with the complete formula A or B, carrying the false sign — provability-propositional.tex, line 103.
  66. Closed tableau beginning with the complete formula A or B, carrying the false sign, later construction stage two — provability-propositional.tex, line 113.
  67. Proposition: tableau derivability rules for conditionals — provability-propositional.tex, line 126.
  68. Closed tableau beginning with the complete formula B, carrying the false sign, later construction stage two — provability-propositional.tex, line 138.
  69. Closed tableau beginning with the complete formula A implies B, carrying the false sign — provability-propositional.tex, line 151.
  70. Closed tableau beginning with the complete formula A implies B, carrying the false sign, later construction stage two — provability-propositional.tex, line 162.
  71. Definition of satisfaction for signed formulas and branches — soundness.tex, line 41.
  72. Theorem: a closed tableau has no satisfying valuation — soundness.tex, line 53.
  73. Exercise completing omitted soundness cases — soundness.tex, line 199; preserved unsolved prompt.
  74. Corollary: tableau theorems are tautologies — soundness.tex, line 204.
  75. Corollary: tableau derivability implies semantic entailment — soundness.tex, line 209.
  76. Corollary: satisfiable formula sets are consistent — soundness.tex, line 225.

Four resolved internal references

  1. Proposition characterizing inconsistency by derivability — proof-theoretic-notions.tex, line 158.
  2. Theorem: a closed tableau has no satisfying valuation — soundness.tex, line 200.
  3. Theorem: a closed tableau has no satisfying valuation — soundness.tex, line 218.
  4. Theorem: a closed tableau has no satisfying valuation — soundness.tex, line 234.