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 proof-object guide

All 64 stable expression records, 128 native MathML variants, 137 occurrence backlinks, and four ordered formal narratives are indexed here.

64 expression records

Expression 5

Inline MathML variant

⊧A\Entails !A

Block MathML variant

⊧A\Entails !A

Conventional reading: A is valid

Meaning here: Formula A is valid in first-order logic: every first-order structure satisfies A under every variable assignment relevant to A's free variables.

1 occurrence
  1. Occurrence 1: content/first-order-logic/proof-systems/introduction.tex, line 62, column 35

Expression 7

Inline MathML variant

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

Block MathML variant

Γ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: content/first-order-logic/proof-systems/tableaux.tex, line 45, column 50

Expression 8

Inline MathML variant

Γ⊢⊥\Gamma \Proves \lfalse

Block MathML variant

Γ⊢⊥\Gamma \Proves \lfalse

Conventional reading: Gamma syntactically derives a contradiction

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

2 occurrences
  1. Occurrence 1: content/first-order-logic/proof-systems/natural-deduction.tex, line 77, column 36
  2. Occurrence 2: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 66, column 35

Expression 10

Inline MathML variant

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

Block MathML variant

𝕋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: content/first-order-logic/proof-systems/tableaux.tex, line 19, column 1

Expression 11

Inline MathML variant

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

Block MathML variant

(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: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 56, column 8

Expression 12

Inline MathML variant

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

Block MathML variant

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: content/first-order-logic/proof-systems/tableaux.tex, line 38, column 1

Expression 16

Inline MathML variant

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

Block MathML variant

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: content/first-order-logic/proof-systems/sequent-calculus.tex, line 18, column 1

Expression 19

Inline MathML variant

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

Block MathML variant

{𝕋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: content/first-order-logic/proof-systems/tableaux.tex, line 67, column 1

Expression 20

Inline MathML variant

Γ\Gamma

Block MathML variant

Γ\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: content/first-order-logic/proof-systems/introduction.tex, line 58, column 58
  2. Occurrence 2: content/first-order-logic/proof-systems/introduction.tex, line 94, column 1
  3. Occurrence 3: content/first-order-logic/proof-systems/sequent-calculus.tex, line 33, column 62
  4. Occurrence 4: content/first-order-logic/proof-systems/sequent-calculus.tex, line 34, column 43
  5. Occurrence 5: content/first-order-logic/proof-systems/sequent-calculus.tex, line 39, column 42
  6. Occurrence 6: content/first-order-logic/proof-systems/sequent-calculus.tex, line 52, column 7
  7. Occurrence 7: content/first-order-logic/proof-systems/sequent-calculus.tex, line 54, column 7
  8. Occurrence 8: content/first-order-logic/proof-systems/natural-deduction.tex, line 62, column 54
  9. Occurrence 9: content/first-order-logic/proof-systems/natural-deduction.tex, line 77, column 7
  10. Occurrence 10: content/first-order-logic/proof-systems/tableaux.tex, line 65, column 7
  11. Occurrence 11: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 22, column 43
  12. Occurrence 12: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 48, column 44
  13. Occurrence 13: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 50, column 48
  14. Occurrence 14: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 66, column 7
  15. Occurrence 15: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 68, column 7

Expression 21

Inline MathML variant

⊢\Proves

Block MathML variant

⊢\Proves

Conventional reading: syntactic derivability

Meaning here: The turnstile denotes the derivability relation for the proof system currently under discussion.

5 occurrences
  1. Occurrence 1: content/first-order-logic/proof-systems/introduction.tex, line 59, column 9
  2. Occurrence 2: content/first-order-logic/proof-systems/introduction.tex, line 92, column 6
  3. Occurrence 3: content/first-order-logic/proof-systems/sequent-calculus.tex, line 37, column 5
  4. Occurrence 4: content/first-order-logic/proof-systems/tableaux.tex, line 44, column 5
  5. Occurrence 5: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 46, column 5

Expression 27

Inline MathML variant

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

Block MathML variant

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: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 30, column 1

Expression 29

Inline MathML variant

A!A

Block MathML variant

A!A

Conventional reading: formula A

Meaning here: The metavariable A denotes an arbitrary formula.

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

Expression 35

Inline MathML variant

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

Block MathML variant

{𝔽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: content/first-order-logic/proof-systems/tableaux.tex, line 48, column 1

Expression 36

Inline MathML variant

⊢(A∧B)→A\Proves (!A \land !B) \lif !A

Block MathML variant

⊢(A∧B)→A\Proves (!A \land !B) \lif !A

Conventional reading: the conditional from A and B to A is derivable without assumptions

Meaning here: The conditional from A and B to A is a theorem of the proof system currently under discussion.

3 occurrences
  1. Occurrence 1: content/first-order-logic/proof-systems/sequent-calculus.tex, line 43, column 6
  2. Occurrence 2: content/first-order-logic/proof-systems/natural-deduction.tex, line 65, column 55
  3. Occurrence 3: content/first-order-logic/proof-systems/tableaux.tex, line 51, column 60

Expression 37

Inline MathML variant

Γ⊧A\Gamma \Entails !A

Block MathML variant

Γ⊧A\Gamma \Entails !A

Conventional reading: Gamma semantically entails A

Meaning here: Gamma semantically entails A in first-order logic: every first-order structure under every relevant variable assignment that satisfies every formula in Gamma also satisfies A under that assignment.

2 occurrences
  1. Occurrence 1: content/first-order-logic/proof-systems/introduction.tex, line 63, column 42
  2. Occurrence 2: content/first-order-logic/proof-systems/introduction.tex, line 76, column 30

Expression 46

Inline MathML variant

Γ⊢A\Gamma \Proves !A

Block MathML variant

Γ⊢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: content/first-order-logic/proof-systems/introduction.tex, line 58, column 3
  2. Occurrence 2: content/first-order-logic/proof-systems/introduction.tex, line 63, column 7
  3. Occurrence 3: content/first-order-logic/proof-systems/introduction.tex, line 76, column 1
  4. Occurrence 4: content/first-order-logic/proof-systems/sequent-calculus.tex, line 38, column 10
  5. Occurrence 5: content/first-order-logic/proof-systems/natural-deduction.tex, line 60, column 14
  6. Occurrence 6: content/first-order-logic/proof-systems/tableaux.tex, line 45, column 1
  7. Occurrence 7: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 47, column 13
  8. Occurrence 8: content/first-order-logic/proof-systems/axiomatic-deduction.tex, line 68, column 38

Expression 49

Inline MathML variant

B!B

Block MathML variant

B!B

Conventional reading: formula B

Meaning here: The metavariable B denotes an arbitrary formula.

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

Expression 63

Inline MathML variant

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

Block MathML variant

∧𝕋\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: content/first-order-logic/proof-systems/tableaux.tex, line 34, column 1

Four proof and derivation 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.
Indexed formulas in this object
  1. projected-formula-0008109
  2. projected-formula-0008110
  3. projected-formula-0008111

Source: content/first-order-logic/proof-systems/sequent-calculus.tex, line 44.

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.
Indexed formulas in this object
  1. projected-formula-0008133
  2. projected-formula-0008134
  3. projected-formula-0008135

Source: content/first-order-logic/proof-systems/natural-deduction.tex, line 67.

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.
Indexed formulas in this object
  1. No separately indexed formula occurrence is owned by this non-linear source object; its complete words-only narrative is preserved above.

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

References and exercises

No source cross-references or exercises occur in this chapter.