The Open Logic Text — accessible offline edition

Derivation Systems — Explore equations

Derivation Systems

Reading preferences

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

Equation and object guide

Every distinct expression in Derivation Systems appears with navigable MathML, reviewed speech and meaning, and every source occurrence.

64 expression records

Expression 2

Bi∈Γ!B_i \in \Gamma

Conventional reading: formula B sub i belongs to Gamma

Meaning here: The indexed formula B sub i is a member of the set of formulas Gamma.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 70, column 10

Expression 7

Γ0={B1,…,Bn}⊆Γ\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma

Conventional reading: Gamma sub zero equals the finite set containing B sub one through B sub n, and Gamma sub zero is a subset of Gamma

Meaning here: Gamma sub zero is the displayed finite subset of Gamma whose members are B sub one through B sub n.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 45, column 50

Expression 10

𝕋A or 𝔽A.\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.

Conventional reading: true-signed formula A, or false-signed formula A

Meaning here: The two tableau forms of formula A, prefixed respectively by the blackboard-bold true and false truth-value signs.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 19, column 1

Expression 11

(B→(B∨A))→(A→(B→(B∨A)))(!B \lif (!B \lor !A)) \lif (!A \lif (!B \lif (!B \lor !A)))

Conventional reading: if B implies B or A, then A implies that B implies B or A

Meaning here: A conditional axiom instance whose antecedent is B implies B or A and whose consequent is A implies that same conditional.

1 occurrence
  1. Occurrence 1: axiomatic-deduction.tex, line 56, column 8

Expression 12

A∧B𝔽\TRule{\False}{!A \land !B}

Conventional reading: false-conjunction tableau rule

Meaning here: The tableau rule applied when the conjunction A and B has the blackboard-bold false truth-value sign; it branches to formulas A and B carrying that same false sign.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 38, column 1

Expression 13

⇒(A∧B)→A\fCenter (!A \land !B) \lif !A

Conventional reading: empty antecedent sequent arrow: if A and B, then A

Meaning here: A sequent with no formula on the left and the conditional from A and B to A on the right.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 49, column 12

Expression 16

A1,…,Am⇒B1,…,Bm,!A_1, \dots, !A_m \Sequent !B_1, \dots, !B_m,

Conventional reading: A sub one through A sub m, sequent arrow, B sub one through B sub m

Meaning here: A general sequent with the A sequence as antecedent and the B sequence as succedent.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 18, column 1

Expression 19

{𝕋B1,…,𝕋Bn}\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}

Conventional reading: the set of true-signed formulas B sub one through B sub n

Meaning here: A finite set containing formulas B sub one through B sub n, each prefixed by the blackboard-bold true tableau truth-value sign.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 67, column 1

Expression 20

Γ\Gamma

Conventional reading: Gamma

Meaning here: Gamma is a context-sensitive source symbol; every bound occurrence record states its exact role in that source sentence.

15 occurrences
  1. Occurrence 1: introduction.tex, line 58, column 58
  2. Occurrence 2: introduction.tex, line 94, column 1
  3. Occurrence 3: sequent-calculus.tex, line 33, column 62
  4. Occurrence 4: sequent-calculus.tex, line 34, column 43
  5. Occurrence 5: sequent-calculus.tex, line 39, column 42
  6. Occurrence 6: sequent-calculus.tex, line 52, column 7
  7. Occurrence 7: sequent-calculus.tex, line 54, column 7
  8. Occurrence 8: natural-deduction.tex, line 62, column 54
  9. Occurrence 9: natural-deduction.tex, line 77, column 7
  10. Occurrence 10: tableaux.tex, line 65, column 7
  11. Occurrence 11: axiomatic-deduction.tex, line 22, column 43
  12. Occurrence 12: axiomatic-deduction.tex, line 48, column 44
  13. Occurrence 13: axiomatic-deduction.tex, line 50, column 48
  14. Occurrence 14: axiomatic-deduction.tex, line 66, column 7
  15. Occurrence 15: axiomatic-deduction.tex, line 68, column 7

Expression 22

𝕋\True

Conventional reading: blackboard-bold true tableau sign

Meaning here: The blackboard-bold letter T is the tableau truth-value sign for true.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 18, column 2

Expression 24

A∈Γ0!A \in \Gamma_0

Conventional reading: formula A belongs to Gamma sub zero

Meaning here: Formula A occurs in the finite antecedent sequence Gamma sub zero used in the sequent derivation.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 53, column 53

Expression 25

A,Γ⇒Δ,B!A, \Gamma \Sequent \Delta, !B

Conventional reading: A together with Gamma, sequent arrow, Delta together with B

Meaning here: A sequent whose antecedent contains A and Gamma and whose succedent contains Delta and B.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 32, column 47

Expression 27

A→(B→A)B→(B∨C)(B∧C)→B!A \lif (!B \lif !A) \qquad !B \lif (!B \lor !C) \qquad (!B \land !C) \lif !B

Conventional reading: three axiom schemas: first, A implies that B implies A; second, B implies B or C; third, if B and C, then B

Meaning here: Three displayed examples of axiom schemas governing the conditional, disjunction, and conjunction.

1 occurrence
  1. Occurrence 1: axiomatic-deduction.tex, line 30, column 1

Expression 28

Γ⇒Δ,A→B\Gamma \Sequent \Delta, !A \lif !B

Conventional reading: Gamma, sequent arrow, Delta together with the conditional if A then B

Meaning here: A sequent with Gamma on the left and Delta plus the conditional A implies B on the right.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 33, column 16

Expression 29

A!A

Conventional reading: formula A

Meaning here: The metavariable A denotes an arbitrary formula.

28 occurrences
  1. Occurrence 1: introduction.tex, line 57, column 44
  2. Occurrence 2: introduction.tex, line 58, column 31
  3. Occurrence 3: introduction.tex, line 75, column 14
  4. Occurrence 4: introduction.tex, line 75, column 41
  5. Occurrence 5: sequent-calculus.tex, line 34, column 11
  6. Occurrence 6: sequent-calculus.tex, line 39, column 17
  7. Occurrence 7: sequent-calculus.tex, line 41, column 1
  8. Occurrence 8: natural-deduction.tex, line 30, column 65
  9. Occurrence 9: natural-deduction.tex, line 51, column 27
  10. Occurrence 10: natural-deduction.tex, line 52, column 64
  11. Occurrence 11: natural-deduction.tex, line 61, column 35
  12. Occurrence 12: natural-deduction.tex, line 62, column 64
  13. Occurrence 13: natural-deduction.tex, line 64, column 1
  14. Occurrence 14: natural-deduction.tex, line 70, column 14
  15. Occurrence 15: axiomatic-deduction.tex, line 18, column 38
  16. Occurrence 16: axiomatic-deduction.tex, line 21, column 7
  17. Occurrence 17: axiomatic-deduction.tex, line 22, column 7
  18. Occurrence 18: axiomatic-deduction.tex, line 23, column 7
  19. Occurrence 19: axiomatic-deduction.tex, line 25, column 17
  20. Occurrence 20: axiomatic-deduction.tex, line 40, column 54
  21. Occurrence 21: axiomatic-deduction.tex, line 43, column 20
  22. Occurrence 22: axiomatic-deduction.tex, line 43, column 65
  23. Occurrence 23: axiomatic-deduction.tex, line 48, column 14
  24. Occurrence 24: axiomatic-deduction.tex, line 49, column 81
  25. Occurrence 25: axiomatic-deduction.tex, line 50, column 17
  26. Occurrence 26: axiomatic-deduction.tex, line 60, column 30
  27. Occurrence 27: axiomatic-deduction.tex, line 67, column 61
  28. Occurrence 28: axiomatic-deduction.tex, line 68, column 66

Expression 35

{𝔽A,𝕋B1,…,𝕋Bn}\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}

Conventional reading: the set containing false-signed A and true-signed B sub one through B sub n

Meaning here: The tableau starts with A prefixed by the blackboard-bold false sign and each B formula prefixed by the blackboard-bold true sign.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 48, column 1

Expression 38

[A∧B]1\Discharge{!A \land !B}{1}

Conventional reading: the single assumption that is the conjunction of A and B, labeled one for discharge

Meaning here: An occurrence of the conjunctive assumption A and B marked with discharge label one.

1 occurrence
  1. Occurrence 1: natural-deduction.tex, line 68, column 11

Expression 46

Γ⊢A\Gamma \Proves !A

Conventional reading: Gamma syntactically derives A

Meaning here: Formula A is derivable from the premise set Gamma according to the proof system currently under discussion.

8 occurrences
  1. Occurrence 1: introduction.tex, line 58, column 3
  2. Occurrence 2: introduction.tex, line 63, column 7
  3. Occurrence 3: introduction.tex, line 76, column 1
  4. Occurrence 4: sequent-calculus.tex, line 38, column 10
  5. Occurrence 5: natural-deduction.tex, line 60, column 14
  6. Occurrence 6: tableaux.tex, line 45, column 1
  7. Occurrence 7: axiomatic-deduction.tex, line 47, column 13
  8. Occurrence 8: axiomatic-deduction.tex, line 68, column 38

Expression 49

B!B

Conventional reading: formula B

Meaning here: The metavariable B denotes an arbitrary formula.

7 occurrences
  1. Occurrence 1: sequent-calculus.tex, line 34, column 21
  2. Occurrence 2: natural-deduction.tex, line 31, column 5
  3. Occurrence 3: natural-deduction.tex, line 50, column 52
  4. Occurrence 4: axiomatic-deduction.tex, line 41, column 33
  5. Occurrence 5: axiomatic-deduction.tex, line 42, column 53
  6. Occurrence 6: axiomatic-deduction.tex, line 44, column 37
  7. Occurrence 7: axiomatic-deduction.tex, line 60, column 39

Expression 55

𝔽B\sFmla{\False}{!B}

Conventional reading: false-signed formula B

Meaning here: Formula B prefixed by the blackboard-bold false tableau truth-value sign.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 39, column 26

Expression 57

𝕋B\sFmla{\True}{!B}

Conventional reading: true-signed formula B

Meaning here: Formula B prefixed by the blackboard-bold true tableau truth-value sign.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 36, column 25

Expression 59

A∧B,Γ⇒Δ!A \land !B, \Gamma \Sequent \Delta

Conventional reading: A and B together with Gamma, sequent arrow, Delta

Meaning here: A sequent whose antecedent contains the conjunction A and B plus Gamma and whose succedent is Delta.

1 occurrence
  1. Occurrence 1: sequent-calculus.tex, line 31, column 28

Expression 61

𝔽\False

Conventional reading: blackboard-bold false tableau sign

Meaning here: The blackboard-bold letter F is the tableau truth-value sign for false.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 18, column 13

Expression 63

∧𝕋\TRule{\True}{\land}

Conventional reading: true-conjunction tableau rule

Meaning here: The tableau rule that expands a conjunction carrying the blackboard-bold true truth-value sign into both conjuncts carrying that same true sign on one branch.

1 occurrence
  1. Occurrence 1: tableaux.tex, line 34, column 1

Expression 64

⊢A→(B→(B∨A))\Proves !A \lif (!B \lif (!B \lor !A))

Conventional reading: the conditional A implies that B implies B or A is derivable without assumptions

Meaning here: The theorem claim established by the three-line axiomatic derivation.

1 occurrence
  1. Occurrence 1: axiomatic-deduction.tex, line 52, column 63

Proof objects

Sequent-calculus derivation of the conditional from A and B to A

The proof starts from the initial sequent with A on both sides. The left conjunction rule replaces the left A by A and B. The right conditional rule moves that conjunction into the antecedent of a conditional on the right, leaving the left side empty.

  1. Initial sequent: A, sequent arrow, A.
  2. Apply the left conjunction sequent rule to obtain: A and B, sequent arrow, A.
  3. Apply the right conditional sequent rule to obtain an empty antecedent sequent whose conclusion is: if A and B, then A.

Natural-deduction derivation of the conditional from A and B to A

The natural-deduction proof assumes A and B, extracts A by conjunction elimination, and then introduces the conditional while discharging the conjunction assumption.

  1. Assume the conjunction A and B, marked with discharge label one.
  2. By conjunction elimination, infer A.
  3. By conditional introduction, infer: if A and B, then A; discharge the assumption marked one.

Closed tableau for the conditional from A and B to A

This one-branch tableau refutes the assumption that the conditional from A and B to A is false. It reaches a matching true and false occurrence of A, so the branch closes. The spoken description preserves the rule names printed in the source, including its true-conditional labels on the conjunction expansion, rather than silently correcting them.

  1. Begin with the false-signed conditional: if A and B, then A.
  2. Add the true-signed conjunction A and B and the false-signed formula A, using the source's false-conditional rule label one.
  3. From the true-signed conjunction, add true-signed A and then true-signed B. The source labels these two additions as the true-conditional rule, label two.
  4. The branch closes because it contains both true-signed A and false-signed A.

4 formal objects

  1. Sequent-calculus derivation of the conditional from A and B to A — sequent-calculus.tex, line 44.
  2. Natural-deduction derivation of the conditional from A and B to A — natural-deduction.tex, line 67.
  3. Closed tableau for the conditional from A and B to A — tableaux.tex, line 53.
  4. Three-line axiomatic derivation — axiomatic-deduction.tex, line 54.