The Open Logic Text — accessible offline edition

Axiomatic Deduction — Explore equations

Axiomatic Deduction

Reading preferences

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

Equation and object guide

All 146 stable expression records, 44 formal objects, five derivations, five unsolved exercises, and 57 resolved references are indexed here.

146 expression records

Expression 3

{¬¬A}⊢A\{ \lnot\lnot!A\} \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from the premise set containing not not A

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from the premise set containing not not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 113, column 8

Expression 4

(E→(D→E))→((¬D∨E)→(D→E))(!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))

Conventional reading: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 35, column 8

Expression 5

⊢¬A→(A→⊥)\Proves \lnot !A \lif (!A \lif \lfalse)

Conventional reading: the complete formula not A implies open parenthesis A implies falsum close parenthesis is derivable with no premises

Meaning here: The statement is read 'the complete formula not A implies open parenthesis A implies falsum close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 42, column 1
  2. Occurrence 2: provability-propositional.tex, line 50, column 43

Expression 6

Γ⊢(¬A→⊥)→¬¬A\Gamma \Proves (\lnot !A \lif \lfalse) \lif \lnot\lnot !A

Conventional reading: the complete formula open parenthesis not A implies falsum close parenthesis implies not not A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula open parenthesis not A implies falsum close parenthesis implies not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 48, column 33

Expression 7

Reader projection

⊢(A→B)→((B→C)→(A→C))\Proves (!A \lif !B) \lif ((!B \lif !C) \lif (!A \lif !C)

Frozen source MathML

⊢(A→B)→((B→C)→(A→C)\Proves (!A \lif !B) \lif ((!B \lif !C) \lif (!A \lif !C)

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

Conventional reading: the complete formula open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis is derivable with no premises

Meaning here: The statement is read 'the complete formula open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 106, column 7

Expression 10

Γ={A→B,B→C}\Gamma = \{!A \lif !B, !B \lif !C\}

Conventional reading: Gamma equals the set containing A implies B comma B implies C

Meaning here: Gamma is defined as the two-premise set containing the conditional from A to B and the conditional from B to C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 85, column 47

Expression 12

Γ⊢⊥\Gamma \Proves \lfalse

Conventional reading: the complete formula falsum is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula falsum is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

3 occurrences
  1. Occurrence 1: provability-consistency.tex, line 29, column 47
  2. Occurrence 2: provability-consistency.tex, line 67, column 3
  3. Occurrence 3: soundness.tex, line 131, column 6

Expression 16

A→B!A \lif !B

Conventional reading: A implies B

Meaning here: The complete propositional formula is read 'A implies B'. Spoken parentheses and connective names preserve its printed logical scope.

9 occurrences
  1. Occurrence 1: proving-things.tex, line 20, column 16
  2. Occurrence 2: proving-things.tex, line 44, column 46
  3. Occurrence 3: proving-things.tex, line 66, column 61
  4. Occurrence 4: proving-things.tex, line 88, column 8
  5. Occurrence 5: proving-things.tex, line 108, column 41
  6. Occurrence 6: proving-things.tex, line 115, column 67
  7. Occurrence 7: deduction-theorem.tex, line 40, column 10
  8. Occurrence 8: deduction-theorem.tex, line 71, column 64
  9. Occurrence 9: provability-propositional.tex, line 75, column 12

Expression 18

Γ⊢¬¬A\Gamma \Proves \lnot\lnot !A

Conventional reading: the complete formula not not A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 49, column 61

Expression 19

(D→(D→D))→(D→D)(!D \lif (!D \lif !D)) \lif (!D \lif !D)

Conventional reading: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 76, column 8

Expression 20

A≡⊥!A \ident \lfalse

Conventional reading: A is syntactically identical to falsum

Meaning here: The expression is read 'A is syntactically identical to falsum'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

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

Expression 22

B∈Γ∪{A}!B \in \Gamma \cup \{!A\}

Conventional reading: B belongs to Gamma union the set containing A

Meaning here: The expression is read 'B belongs to Gamma union the set containing A'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 28, column 45

Expression 23

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

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

Meaning here: The complete propositional formula is read 'not open parenthesis A or B close parenthesis implies not A'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 24

((A∧B)→C)→(A→(B→C))((!A \land !B) \lif !C) \lif (!A \lif (!B \lif !C))

Conventional reading: open parenthesis open parenthesis A and B close parenthesis implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis open parenthesis A and B close parenthesis implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 25

Γ⊢A→C\Gamma \Proves !A \lif !C

Conventional reading: the complete formula A implies C is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula A implies C is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 103, column 29

Expression 26

Γ∪{¬A}⊢¬B\Gamma \cup \{ \lnot !A\} \Proves \lnot !B

Conventional reading: the complete formula not B is axiomatically derivable from the union of Gamma and the singleton set containing not A

Meaning here: The statement is read 'the complete formula not B is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 108, column 10

Expression 27

{A,¬A}⊢B\{ !A, \lnot!A\} \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the displayed premises the set containing A comma not A

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises the set containing A comma not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 111, column 8

Expression 28

A1,…,Ak=A,B1,…,Bl=B.!A_1, \dots, !A_k = !A, !B_1, \dots, !B_l = !B.

Conventional reading: derivation A sub one through A sub k, whose last formula is A; followed by derivation B sub one through B sub l, whose last formula is B

Meaning here: The displayed text concatenates a derivation ending in A with a derivation ending in B, preserving both indexed endpoints.

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

Expression 30

v⊭⊥\pSat/{v}{\lfalse}

Conventional reading: valuation v does not satisfy falsum

Meaning here: The valuation statement is read 'valuation v does not satisfy falsum'. It states exactly whether v makes the complete displayed propositional formula true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 136, column 31

Expression 31

B∈{A}!B \in \{ !A\}

Conventional reading: B belongs to the set containing A

Meaning here: The expression is read 'B belongs to the set containing A'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 70, column 55

Expression 32

Γ⊬⊥\Gamma\Proves/ \lfalse

Conventional reading: the complete formula falsum is not axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula falsum is not axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 33

{A}∪Δ⊢B\{!A\} \cup \Delta \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the union of the singleton set containing A and Delta

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the union of the singleton set containing A and Delta'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 65, column 28
  2. Occurrence 2: proof-theoretic-notions.tex, line 70, column 11

Expression 34

Γ∪{B}⊢A\Gamma \cup \{ !B\} \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 109, column 26

Expression 35

Γ⊢¬A→⊥\Gamma \Proves \lnot !A \lif \lfalse

Conventional reading: the complete formula not A implies falsum is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not A implies falsum is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 37

Γ\Gamma

Conventional reading: Gamma

Meaning here: Gamma is the set of premise formulas from which axiomatic derivability is considered.

38 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 25, column 4
  2. Occurrence 2: rules-and-proofs.tex, line 26, column 28
  3. Occurrence 3: rules-and-proofs.tex, line 45, column 60
  4. Occurrence 4: rules-and-proofs.tex, line 53, column 27
  5. Occurrence 5: rules-and-proofs.tex, line 78, column 57
  6. Occurrence 6: rules-and-proofs.tex, line 84, column 49
  7. Occurrence 7: rules-and-proofs.tex, line 85, column 55
  8. Occurrence 8: proving-things.tex, line 84, column 42
  9. Occurrence 9: proving-things.tex, line 98, column 45
  10. Occurrence 10: proving-things.tex, line 108, column 59
  11. Occurrence 11: proving-things.tex, line 109, column 44
  12. Occurrence 12: proving-things.tex, line 113, column 25
  13. Occurrence 13: proof-theoretic-notions.tex, line 27, column 49
  14. Occurrence 14: proof-theoretic-notions.tex, line 28, column 55
  15. Occurrence 15: proof-theoretic-notions.tex, line 39, column 7
  16. Occurrence 16: proof-theoretic-notions.tex, line 49, column 66
  17. Occurrence 17: proof-theoretic-notions.tex, line 59, column 33
  18. Occurrence 18: proof-theoretic-notions.tex, line 74, column 53
  19. Occurrence 19: proof-theoretic-notions.tex, line 76, column 26
  20. Occurrence 20: proof-theoretic-notions.tex, line 93, column 1
  21. Occurrence 21: proof-theoretic-notions.tex, line 117, column 35
  22. Occurrence 22: proof-theoretic-notions.tex, line 118, column 22
  23. Occurrence 23: proof-theoretic-notions.tex, line 126, column 62
  24. Occurrence 24: proof-theoretic-notions.tex, line 128, column 50
  25. Occurrence 25: provability-consistency.tex, line 21, column 8
  26. Occurrence 26: provability-consistency.tex, line 30, column 19
  27. Occurrence 27: provability-consistency.tex, line 61, column 58
  28. Occurrence 28: provability-consistency.tex, line 73, column 22
  29. Occurrence 29: soundness.tex, line 23, column 49
  30. Occurrence 30: soundness.tex, line 25, column 32
  31. Occurrence 31: soundness.tex, line 61, column 1
  32. Occurrence 32: soundness.tex, line 63, column 4
  33. Occurrence 33: soundness.tex, line 126, column 4
  34. Occurrence 34: soundness.tex, line 130, column 44
  35. Occurrence 35: soundness.tex, line 132, column 16
  36. Occurrence 36: soundness.tex, line 134, column 16
  37. Occurrence 37: soundness.tex, line 138, column 54
  38. Occurrence 38: soundness.tex, line 139, column 1

Expression 39

Γ∪{A}⊢A→B\Gamma \cup \{!A\} \Proves !A \lif !B

Conventional reading: the complete formula A implies B is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula A implies B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 56, column 11

Expression 40

Γ⊆Δ\Gamma \subseteq \Delta

Conventional reading: Gamma is a subset of Delta

Meaning here: The expression is read 'Gamma is a subset of Delta'. This states inclusion between the two displayed premise sets.

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

Expression 41

D→(B→D)!D \lif (!B \lif !D)

Conventional reading: D implies open parenthesis B implies D close parenthesis

Meaning here: The complete propositional formula is read 'D implies open parenthesis B implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 67, column 24

Expression 42

{¬A,¬B}⊢(A∨B)→⊥\{\lnot !A, \lnot !B\} \Proves (!A \lor !B) \lif \lfalse

Conventional reading: the complete formula open parenthesis A or B close parenthesis implies falsum is axiomatically derivable from the displayed premises the set containing not A comma not B

Meaning here: The statement is read 'the complete formula open parenthesis A or B close parenthesis implies falsum is axiomatically derivable from the displayed premises the set containing not A comma not B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 54, column 33

Expression 44

Γ∪Δ⊢B\Gamma \cup \Delta \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the union of premise sets Gamma and Delta

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the union of premise sets Gamma and Delta'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 45

(D→((D→D)→D))→continued on the next display line(!D \lif ((!D \lif !D) \lif !D)) \lif {}

Conventional reading: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line

Meaning here: The complete propositional formula is read 'open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 74, column 8

Expression 46

Ai!A_i

Conventional reading: A sub i

Meaning here: A sub i is the formula at derivation step i.

8 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 31, column 7
  2. Occurrence 2: rules-and-proofs.tex, line 32, column 7
  3. Occurrence 3: rules-and-proofs.tex, line 72, column 7
  4. Occurrence 4: rules-and-proofs.tex, line 76, column 27
  5. Occurrence 5: rules-and-proofs.tex, line 78, column 32
  6. Occurrence 6: proof-theoretic-notions.tex, line 75, column 58
  7. Occurrence 7: proof-theoretic-notions.tex, line 126, column 12
  8. Occurrence 8: proof-theoretic-notions.tex, line 128, column 30

Expression 47

v⊨A\pSat{v}{!A}

Conventional reading: valuation v satisfies A

Meaning here: The valuation statement is read 'valuation v satisfies A'. It states exactly whether v makes the complete displayed propositional formula true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 38, column 6

Expression 48

{A,A→B}⊢B\{!A, !A \lif !B\} \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the displayed premises the set containing A comma A implies B

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises the set containing A comma A implies B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 37, column 16

Expression 49

((D→(D→D))→(D→D))((!D \lif (!D \lif !D)) \lif (!D \lif !D))

Conventional reading: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 75, column 12

Expression 53

Γ⊢¬A\Gamma \Proves \lnot !A

Conventional reading: the complete formula not A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 56, column 12

Expression 55

(A∧B)→A(A∧B)→BA→(B→(A∧B))A→(A∨B)A→(B∨A)(A→C)→((B→C)→((A∨B)→C))A→(B→A)(A→(B→C))→((A→B)→(A→C))(A→B)→((A→¬B)→¬A)¬A→(A→B)⊤⊥→A(A→⊥)→¬A¬¬A→A& (!A \land !B) \lif !A \ollabel{ax:land1}\\ & (!A \land !B) \lif !B \ollabel{ax:land2}\\ & !A \lif (!B \lif (!A \land !B)) \ollabel{ax:land3}\\ & !A \lif (!A \lor !B) \ollabel{ax:lor1}\\ & !A \lif (!B \lor !A) \ollabel{ax:lor2}\\ & (!A \lif !C) \lif ((!B \lif !C) \lif ((!A \lor !B) \lif !C)) \ollabel{ax:lor3}\\ & !A \lif (!B \lif !A) \ollabel{ax:lif1}\\ & (!A \lif (!B \lif !C)) \lif ((!A \lif !B) \lif (!A \lif !C)) \ollabel{ax:lif2}\\ & (!A \lif !B) \lif ((!A \lif \lnot !B) \lif \lnot !A) \ollabel{ax:lnot1}\\ & \lnot !A \lif (!A \lif !B) \ollabel{ax:lnot2}\\ & \ltrue \ollabel{ax:ltrue}\\ & \lfalse \lif !A \ollabel{ax:lfalse1}\\ & (!A \lif \lfalse) \lif \lnot !A \ollabel{ax:lfalse2}\\ & \lnot\lnot !A \lif !A \ollabel{ax:dne}

Conventional reading: fourteen axiom schemes in source order. Conjunction elimination left: open parenthesis A and B close parenthesis implies A. Conjunction elimination right: open parenthesis A and B close parenthesis implies B. Conjunction introduction: A implies open parenthesis B implies open parenthesis A and B close parenthesis close parenthesis. Disjunction introduction left: A implies open parenthesis A or B close parenthesis. Disjunction introduction right: A implies open parenthesis B or A close parenthesis. Disjunction elimination: open parenthesis A implies C close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis open parenthesis A or B close parenthesis implies C close parenthesis close parenthesis. Conditional scheme one: A implies open parenthesis B implies A close parenthesis. Conditional scheme two: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Negation scheme one: open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis A implies not B close parenthesis implies not A close parenthesis. Negation scheme two: not A implies open parenthesis A implies B close parenthesis. Truth scheme: verum. Falsity scheme one: falsum implies A. Falsity scheme two: open parenthesis A implies falsum close parenthesis implies not A. Double negation elimination: not not A implies A.

Meaning here: This is the complete ordered list of fourteen propositional axiom schemes, with every connective scope and source label preserved.

1 occurrence
  1. Occurrence 1: axioms-rules-propositional.tex, line 18, column 1

Expression 57

Γ⊢(A→(C→B))→((A→C)→(A→B)),\Gamma \Proves (!A \lif (!C \lif !B)) \lif ((!A\lif !C) \lif (!A \lif !B)),

Conventional reading: from Gamma derive the conditional whose antecedent is the conditional from A to the conditional from C to B, and whose consequent is the conditional whose antecedent is the conditional from A to C and whose consequent is the conditional from A to B

Meaning here: The statement is read 'from Gamma derive the conditional whose antecedent is the conditional from A to the conditional from C to B, and whose consequent is the conditional whose antecedent is the conditional from A to C and whose consequent is the conditional from A to B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 89, column 1

Expression 58

A1,…,An⊢B!A_1, \dots, !A_n \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the displayed premises A sub one comma through the omitted intermediate entries comma A sub n

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises A sub one comma through the omitted intermediate entries comma A sub n'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 59

Γ∪{A}⊢⊥\Gamma \cup \{!A\} \Proves \lfalse

Conventional reading: the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 60

B⊢A→B!B \Proves !A \lif !B

Conventional reading: the complete formula A implies B is axiomatically derivable from premise B

Meaning here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 61

A∨B,¬A,¬B!A \lor !B, \lnot !A, \lnot !B

Conventional reading: the three formulas A or B, not A, and not B

Meaning here: The complete propositional formula is read 'the three formulas A or B, not A, and not B'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 62

Γ⊢A→B\Gamma \Proves !A \lif !B

Conventional reading: the complete formula A implies B is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

8 occurrences
  1. Occurrence 1: proving-things.tex, line 102, column 27
  2. Occurrence 2: proving-things.tex, line 107, column 11
  3. Occurrence 3: deduction-theorem.tex, line 32, column 48
  4. Occurrence 4: deduction-theorem.tex, line 51, column 9
  5. Occurrence 5: deduction-theorem.tex, line 55, column 40
  6. Occurrence 6: deduction-theorem.tex, line 70, column 23
  7. Occurrence 7: deduction-theorem.tex, line 71, column 6
  8. Occurrence 8: deduction-theorem.tex, line 94, column 1

Expression 63

A!A

Conventional reading: A

Meaning here: A is the arbitrary complete propositional formula used in this exact source statement.

38 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 48, column 46
  2. Occurrence 2: rules-and-proofs.tex, line 52, column 28
  3. Occurrence 3: rules-and-proofs.tex, line 55, column 15
  4. Occurrence 4: rules-and-proofs.tex, line 55, column 47
  5. Occurrence 5: rules-and-proofs.tex, line 58, column 6
  6. Occurrence 6: rules-and-proofs.tex, line 58, column 29
  7. Occurrence 7: rules-and-proofs.tex, line 65, column 8
  8. Occurrence 8: rules-and-proofs.tex, line 84, column 15
  9. Occurrence 9: rules-and-proofs.tex, line 86, column 4
  10. Occurrence 10: rules-and-proofs.tex, line 90, column 15
  11. Occurrence 11: rules-and-proofs.tex, line 91, column 4
  12. Occurrence 12: rules-and-proofs.tex, line 91, column 55
  13. Occurrence 13: axioms-rules-propositional.tex, line 37, column 67
  14. Occurrence 14: proving-things.tex, line 20, column 7
  15. Occurrence 15: proving-things.tex, line 21, column 52
  16. Occurrence 16: proving-things.tex, line 47, column 54
  17. Occurrence 17: proving-things.tex, line 54, column 24
  18. Occurrence 18: proving-things.tex, line 65, column 33
  19. Occurrence 19: proof-theoretic-notions.tex, line 27, column 15
  20. Occurrence 20: proof-theoretic-notions.tex, line 29, column 4
  21. Occurrence 21: proof-theoretic-notions.tex, line 33, column 15
  22. Occurrence 22: proof-theoretic-notions.tex, line 34, column 1
  23. Occurrence 23: proof-theoretic-notions.tex, line 34, column 52
  24. Occurrence 24: proof-theoretic-notions.tex, line 49, column 19
  25. Occurrence 25: proof-theoretic-notions.tex, line 49, column 56
  26. Occurrence 26: proof-theoretic-notions.tex, line 59, column 23
  27. Occurrence 27: proof-theoretic-notions.tex, line 60, column 1
  28. Occurrence 28: proof-theoretic-notions.tex, line 74, column 43
  29. Occurrence 29: proof-theoretic-notions.tex, line 93, column 60
  30. Occurrence 30: deduction-theorem.tex, line 39, column 10
  31. Occurrence 31: provability-propositional.tex, line 74, column 12
  32. Occurrence 32: soundness.tex, line 22, column 27
  33. Occurrence 33: soundness.tex, line 23, column 10
  34. Occurrence 34: soundness.tex, line 35, column 6
  35. Occurrence 35: soundness.tex, line 60, column 53
  36. Occurrence 36: soundness.tex, line 64, column 47
  37. Occurrence 37: soundness.tex, line 68, column 43
  38. Occurrence 38: soundness.tex, line 121, column 23

Expression 64

Γ∪{A}⊢B\Gamma \cup \{!A\} \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: deduction-theorem.tex, line 50, column 29
  2. Occurrence 2: deduction-theorem.tex, line 58, column 56

Expression 65

B⊢A∨B!B \Proves !A \lor !B

Conventional reading: the complete formula A or B is axiomatically derivable from premise B

Meaning here: The statement is read 'the complete formula A or B is axiomatically derivable from premise B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 66

A≡An!A \ident !A_n

Conventional reading: A is syntactically identical to A sub n

Meaning here: The expression is read 'A is syntactically identical to A sub n'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

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

Expression 68

⊢¬B→(B→⊥)\Proves \lnot !B \lif (!B \lif \lfalse)

Conventional reading: the complete formula not B implies open parenthesis B implies falsum close parenthesis is derivable with no premises

Meaning here: The statement is read 'the complete formula not B implies open parenthesis B implies falsum close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 51, column 24

Expression 69

(¬D→(D→E))→((E→(D→E))→((¬D∨E)→(D→E))).(\lnot !D \lif (!D \lif !E)) \lif ((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))).

Conventional reading: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 70

Γ∪{A}⊢C\Gamma \cup \{!A\} \Proves !C

Conventional reading: the complete formula C is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula C is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 81, column 51

Expression 71

(D→D)(!D \lif !D)

Conventional reading: open parenthesis D implies D close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis D implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 70, column 58

Expression 72

{¬B}⊢B→⊥\{\lnot !B\} \Proves !B \lif \lfalse

Conventional reading: the complete formula B implies falsum is axiomatically derivable from the premise set containing not B

Meaning here: The statement is read 'the complete formula B implies falsum is axiomatically derivable from the premise set containing not B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 53, column 18

Expression 74

Γ⊢Ai\Gamma \Proves !A_i

Conventional reading: the complete formula A sub i is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula A sub i is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 75

(¬D→(D→E))→continued on the next display line(\lnot !D \lif (!D \lif !E)) \lif {}

Conventional reading: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line

Meaning here: The complete propositional formula is read 'open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 33, column 8

Expression 76

A,A→B⊢B!A, !A \lif !B \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from the displayed premises A comma A implies B

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises A comma A implies B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: provability-propositional.tex, line 19, column 19
  2. Occurrence 2: provability-propositional.tex, line 64, column 46

Expression 77

Γ⊨B\Gamma \Entails !B

Conventional reading: the complete formula B is semantically entailed by premise set Gamma

Meaning here: The statement is read 'the complete formula B is semantically entailed by premise set Gamma'. Every propositional valuation satisfying every formula in Gamma also satisfies the complete displayed conclusion.

1 occurrence
  1. Occurrence 1: soundness.tex, line 73, column 13

Expression 78

A→A!A \lif !A

Conventional reading: A implies A

Meaning here: The complete propositional formula is read 'A implies A'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 72, column 25

Expression 79

¬D\lnot !D

Conventional reading: not D

Meaning here: The complete propositional formula is read 'not D'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 80

Γ⊢¬A→(A→⊥)\Gamma \Proves \lnot !A \lif (!A \lif \lfalse)

Conventional reading: the complete formula not A implies open parenthesis A implies falsum close parenthesis is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not A implies open parenthesis A implies falsum close parenthesis is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 81

Γ∪{¬A}⊢¬A\Gamma \cup \{\lnot !A\} \Proves \lnot !A

Conventional reading: the complete formula not A is axiomatically derivable from the union of Gamma and the singleton set containing not A

Meaning here: The statement is read 'the complete formula not A is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 40, column 48

Expression 83

¬A∈Γ\lnot !A \in \Gamma

Conventional reading: not A belongs to Gamma

Meaning here: The expression is read 'not A belongs to Gamma'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 61, column 30

Expression 85

D→E!D \lif !E

Conventional reading: D implies E

Meaning here: The complete propositional formula is read 'D implies E'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 22, column 38

Expression 87

Γ⊢¬¬A→A\Gamma \Proves \lnot\lnot !A \lif !A

Conventional reading: the complete formula not not A implies A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not not A implies A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 50, column 55

Expression 88

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Conventional reading: Gamma sub zero is a subset of Gamma

Meaning here: The expression is read 'Gamma sub zero is a subset of Gamma'. This states inclusion between the two displayed premise sets.

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

Expression 90

(B→C)→(A→(B→C))(!B \lif !C) \lif (!A \lif (!B \lif !C))

Conventional reading: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 90, column 8

Expression 91

Γ⊢B\Gamma \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

8 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 87, column 19
  2. Occurrence 2: proof-theoretic-notions.tex, line 89, column 1
  3. Occurrence 3: deduction-theorem.tex, line 28, column 23
  4. Occurrence 4: deduction-theorem.tex, line 33, column 13
  5. Occurrence 5: deduction-theorem.tex, line 43, column 38
  6. Occurrence 6: deduction-theorem.tex, line 68, column 19
  7. Occurrence 7: provability-consistency.tex, line 26, column 55
  8. Occurrence 8: provability-consistency.tex, line 28, column 15

Expression 92

(A→(B→C))→((A→B)→(A→C))(!A \lif (!B \lif !C)) \lif ((!A \lif !B) \lif (!A \lif !C))

Conventional reading: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 93

Γ∪{¬A}⊢A\Gamma \cup \{\lnot !A\} \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing not A

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 39, column 41

Expression 94

Γ⊨A\Gamma \Entails !A

Conventional reading: the complete formula A is semantically entailed by premise set Gamma

Meaning here: The statement is read 'the complete formula A is semantically entailed by premise set Gamma'. Every propositional valuation satisfying every formula in Gamma also satisfies the complete displayed conclusion.

4 occurrences
  1. Occurrence 1: soundness.tex, line 56, column 29
  2. Occurrence 2: soundness.tex, line 65, column 1
  3. Occurrence 3: soundness.tex, line 65, column 58
  4. Occurrence 4: soundness.tex, line 74, column 11

Expression 95

D→((D→D)→D)!D \lif ((!D \lif !D) \lif !D)

Conventional reading: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis

Meaning here: The complete propositional formula is read 'D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 96

((A→B)→(A→C))((!A \lif !B) \lif (!A \lif !C))

Conventional reading: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 93, column 12
  2. Occurrence 2: proving-things.tex, line 94, column 8

Expression 98

A,B⊢A∧B!A, !B \Proves !A \land !B

Conventional reading: the complete formula A and B is axiomatically derivable from the displayed premises A comma B

Meaning here: The statement is read 'the complete formula A and B is axiomatically derivable from the displayed premises A comma B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 27, column 47

Expression 99

{¬A}⊢A→⊥\{\lnot !A\} \Proves !A \lif \lfalse

Conventional reading: the complete formula A implies falsum is axiomatically derivable from the premise set containing not A

Meaning here: The statement is read 'the complete formula A implies falsum is axiomatically derivable from the premise set containing not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 52, column 39

Expression 100

Γ∪{A}⊢C→B\Gamma \cup \{!A\} \Proves !C \lif !B

Conventional reading: the complete formula C implies B is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula C implies B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 81, column 7

Expression 101

C→B!C \lif !B

Conventional reading: C implies B

Meaning here: The complete propositional formula is read 'C implies B'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 80, column 20

Expression 102

Γ∪{B}⊢A\Gamma \cup \{!B\} \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 26, column 11

Expression 103

Reader projection

B∈Γ∪{A}\in \Gamma \cup \{!A\}

Frozen source MathML

∈Γ∪{A}\in \Gamma \cup \{!A\}

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

Conventional reading: B belongs to Gamma union the set containing A

Meaning here: The expression is read 'B belongs to Gamma union the set containing A'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 67, column 8

Expression 105

(A→(B→C))→continued on the next display line(!A \lif (!B \lif !C)) \lif {}

Conventional reading: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line

Meaning here: The complete propositional formula is read 'open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 92, column 8

Expression 106

Γ⊢B→(A→B)\Gamma \Proves !B \lif (!A \lif !B)

Conventional reading: the complete formula B implies open parenthesis A implies B close parenthesis is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula B implies open parenthesis A implies B close parenthesis is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 68, column 58

Expression 107

Γ∪{¬A}⊢⊥\Gamma \cup \{\lnot !A\} \Proves \lfalse

Conventional reading: the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing not A

Meaning here: The statement is read 'the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 43, column 54
  2. Occurrence 2: provability-consistency.tex, line 46, column 62

Expression 110

Γ∪{A}⊢A\Gamma \cup \{!A\} \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing A

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 57, column 40

Expression 111

¬A⊢A→B\lnot !A \Proves !A \lif !B

Conventional reading: the complete formula A implies B is axiomatically derivable from premise not A

Meaning here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise not A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 66, column 10

Expression 112

Γ⊢A\Gamma \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

21 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 85, column 1
  2. Occurrence 2: proof-theoretic-notions.tex, line 28, column 1
  3. Occurrence 3: proof-theoretic-notions.tex, line 45, column 26
  4. Occurrence 4: proof-theoretic-notions.tex, line 54, column 34
  5. Occurrence 5: proof-theoretic-notions.tex, line 65, column 4
  6. Occurrence 6: proof-theoretic-notions.tex, line 86, column 44
  7. Occurrence 7: proof-theoretic-notions.tex, line 93, column 30
  8. Occurrence 8: proof-theoretic-notions.tex, line 115, column 12
  9. Occurrence 9: proof-theoretic-notions.tex, line 124, column 14
  10. Occurrence 10: deduction-theorem.tex, line 23, column 62
  11. Occurrence 11: deduction-theorem.tex, line 25, column 54
  12. Occurrence 12: deduction-theorem.tex, line 27, column 48
  13. Occurrence 13: deduction-theorem.tex, line 32, column 24
  14. Occurrence 14: deduction-theorem.tex, line 115, column 45
  15. Occurrence 15: provability-consistency.tex, line 20, column 6
  16. Occurrence 16: provability-consistency.tex, line 27, column 45
  17. Occurrence 17: provability-consistency.tex, line 35, column 1
  18. Occurrence 18: provability-consistency.tex, line 39, column 15
  19. Occurrence 19: provability-consistency.tex, line 51, column 55
  20. Occurrence 20: provability-consistency.tex, line 61, column 6
  21. Occurrence 21: soundness.tex, line 56, column 4

Expression 113

Γ0⊢A\Gamma_0 \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from premise set Gamma sub zero

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from premise set Gamma sub zero'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 116, column 33
  2. Occurrence 2: proof-theoretic-notions.tex, line 130, column 10

Expression 118

B!B

Conventional reading: B

Meaning here: B is the arbitrary complete propositional formula used in this exact source statement.

21 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 64, column 23
  2. Occurrence 2: rules-and-proofs.tex, line 74, column 13
  3. Occurrence 3: rules-and-proofs.tex, line 77, column 2
  4. Occurrence 4: axioms-rules-propositional.tex, line 37, column 6
  5. Occurrence 5: proving-things.tex, line 20, column 50
  6. Occurrence 6: proving-things.tex, line 22, column 6
  7. Occurrence 7: proving-things.tex, line 45, column 47
  8. Occurrence 8: proving-things.tex, line 66, column 16
  9. Occurrence 9: proving-things.tex, line 69, column 42
  10. Occurrence 10: proving-things.tex, line 70, column 48
  11. Occurrence 11: proof-theoretic-notions.tex, line 81, column 39
  12. Occurrence 12: deduction-theorem.tex, line 41, column 10
  13. Occurrence 13: deduction-theorem.tex, line 62, column 26
  14. Occurrence 14: deduction-theorem.tex, line 65, column 36
  15. Occurrence 15: deduction-theorem.tex, line 66, column 24
  16. Occurrence 16: deduction-theorem.tex, line 66, column 61
  17. Occurrence 17: deduction-theorem.tex, line 75, column 52
  18. Occurrence 18: deduction-theorem.tex, line 76, column 39
  19. Occurrence 19: deduction-theorem.tex, line 78, column 16
  20. Occurrence 20: provability-propositional.tex, line 76, column 12
  21. Occurrence 21: soundness.tex, line 69, column 37

Expression 119

Γ⊢¬¬A\Gamma \Proves \lnot\lnot!A

Conventional reading: the complete formula not not A is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 115, column 10

Expression 121

Δ⊢A\Delta \Proves !A

Conventional reading: the complete formula A is axiomatically derivable from premise set Delta

Meaning here: The statement is read 'the complete formula A is axiomatically derivable from premise set Delta'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 122

A⊢A∨B!A \Proves !A \lor !B

Conventional reading: the complete formula A or B is axiomatically derivable from premise A

Meaning here: The statement is read 'the complete formula A or B is axiomatically derivable from premise A'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 123

Γ⊢B→C\Gamma \Proves !B \lif !C

Conventional reading: the complete formula B implies C is axiomatically derivable from premise set Gamma

Meaning here: The statement is read 'the complete formula B implies C is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 102, column 59
  2. Occurrence 2: proving-things.tex, line 107, column 43

Expression 125

(¬D∨E)→(D→E)(\lnot !D \lor !E) \lif (!D \lif !E)

Conventional reading: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 17, column 26
  2. Occurrence 2: proving-things.tex, line 37, column 8

Expression 132

((E→(D→E))→((¬D∨E)→(D→E)))((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E)))

Conventional reading: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 34, column 11

Expression 133

B≡A!B \ident !A

Conventional reading: B is syntactically identical to A

Meaning here: The expression is read 'B is syntactically identical to A'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 77, column 67

Expression 134

Γ∪{A}\Gamma \cup \{!A\}

Conventional reading: Gamma union the set containing A

Meaning here: The expression is read 'Gamma union the set containing A'. This forms the union of the displayed premise sets.

7 occurrences
  1. Occurrence 1: deduction-theorem.tex, line 62, column 36
  2. Occurrence 2: deduction-theorem.tex, line 65, column 46
  3. Occurrence 3: deduction-theorem.tex, line 76, column 1
  4. Occurrence 4: provability-consistency.tex, line 20, column 30
  5. Occurrence 5: provability-consistency.tex, line 25, column 6
  6. Occurrence 6: provability-consistency.tex, line 56, column 42
  7. Occurrence 7: provability-consistency.tex, line 72, column 6

Expression 139

A∧B⊢B!A \land !B \Proves !B

Conventional reading: the complete formula B is axiomatically derivable from premise A and B

Meaning here: The statement is read 'the complete formula B is axiomatically derivable from premise A and B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 26, column 13

Expression 140

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

Conventional reading: open parenthesis A and B close parenthesis implies open parenthesis B and A close parenthesis

Meaning here: The complete propositional formula is read 'open parenthesis A and B close parenthesis implies open parenthesis B and A close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 142

Γ⊨B→A\Gamma \Entails !B \lif !A

Conventional reading: the complete formula B implies A is semantically entailed by premise set Gamma

Meaning here: The statement is read 'the complete formula B implies A is semantically entailed by premise set Gamma'. Every propositional valuation satisfying every formula in Gamma also satisfies the complete displayed conclusion.

1 occurrence
  1. Occurrence 1: soundness.tex, line 73, column 38

Expression 143

{A∨B,¬A,¬B}⊢⊥\{!A \lor !B, \lnot !A, \lnot !B\} \Proves \lfalse

Conventional reading: the complete formula falsum is axiomatically derivable from the displayed premises the set containing A or B comma not A comma not B

Meaning here: The statement is read 'the complete formula falsum is axiomatically derivable from the displayed premises the set containing A or B comma not A comma not B'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

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

Expression 146

Γ⊢A→(C→B);Γ⊢A→C.& \Gamma \Proves !A \lif (!C \lif !B); \\ & \Gamma \Proves !A \lif !C.

Conventional reading: two statements: from Gamma derive the conditional from A to the conditional from C to B; and from Gamma derive the conditional from A to C

Meaning here: The statement is read 'two statements: from Gamma derive the conditional from A to the conditional from C to B; and from Gamma derive the conditional from A to C'. It asserts or denies the existence of a finite axiomatic derivation with the displayed premise set and conclusion.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 84, column 1

Five ordered derivations

Five-line derivation from not D or E to D implies E

The derivation uses three named propositional axiom schemes and two applications of modus ponens. A long formula on line two is split across two printed rows and is preserved as two ordered source segments.

  1. Line one: not D implies open parenthesis D implies E close parenthesis. Justification: the second negation axiom scheme.
  2. Line two is printed in two formula segments. Segment one: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis. Justification: the third disjunction axiom scheme.
  3. Line three: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis. Justification: modus ponens from lines one and two.
  4. Line four: E implies open parenthesis D implies E close parenthesis. Justification: the first conditional axiom scheme.
  5. Line five: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis. Justification: modus ponens from lines three and four.

Words-only linearization: Five-line derivation from not D or E to D implies E. The derivation uses three named propositional axiom schemes and two applications of modus ponens. A long formula on line two is split across two printed rows and is preserved as two ordered source segments. Line one: not D implies open parenthesis D implies E close parenthesis. Justification: the second negation axiom scheme. Line two is printed in two formula segments. Segment one: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis. Justification: the third disjunction axiom scheme. Line three: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis. Justification: modus ponens from lines one and two. Line four: E implies open parenthesis D implies E close parenthesis. Justification: the first conditional axiom scheme. Line five: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis. Justification: modus ponens from lines three and four. Resolved reference one: Reference to the second negation axiom scheme. Resolved reference two: Reference to the third disjunction axiom scheme. Resolved reference three: Reference to the first conditional axiom scheme.

Five-line derivation of D implies D

The derivation uses three conditional-axiom instances and two applications of modus ponens. Its second line is preserved as two ordered printed formula segments.

  1. Line one: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis. Justification: the first conditional axiom scheme.
  2. Line two is printed in two formula segments. Segment one: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis. Justification: the second conditional axiom scheme.
  3. Line three: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis. Justification: modus ponens from lines one and two.
  4. Line four: D implies open parenthesis D implies D close parenthesis. Justification: the first conditional axiom scheme.
  5. Line five: D implies D. Justification: modus ponens from lines three and four.

Words-only linearization: Five-line derivation of D implies D. The derivation uses three conditional-axiom instances and two applications of modus ponens. Its second line is preserved as two ordered printed formula segments. Line one: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis. Justification: the first conditional axiom scheme. Line two is printed in two formula segments. Segment one: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis. Justification: the second conditional axiom scheme. Line three: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis. Justification: modus ponens from lines one and two. Line four: D implies open parenthesis D implies D close parenthesis. Justification: the first conditional axiom scheme. Line five: D implies D. Justification: modus ponens from lines three and four. Resolved reference one: Reference to the first conditional axiom scheme. Resolved reference two: Reference to the second conditional axiom scheme. Resolved reference three: Reference to the first conditional axiom scheme.

Seven-line derivation chaining A implies B and B implies C

The seven-line derivation begins with two hypotheses, adds instances of the two conditional axiom schemes, and applies modus ponens three times. Its fifth line spans two printed formula segments.

  1. Line one: A implies B. Justification: hypothesis.
  2. Line two: B implies C. Justification: hypothesis.
  3. Line three: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis. Justification: the first conditional axiom scheme.
  4. Line four: A implies open parenthesis B implies C close parenthesis. Justification: modus ponens from lines two and three.
  5. Line five is printed in two formula segments. Segment one: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Justification: the second conditional axiom scheme.
  6. Line six: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Justification: modus ponens from lines four and five.
  7. Line seven: A implies C. Justification: modus ponens from lines one and six.

Words-only linearization: Seven-line derivation chaining A implies B and B implies C. The seven-line derivation begins with two hypotheses, adds instances of the two conditional axiom schemes, and applies modus ponens three times. Its fifth line spans two printed formula segments. Line one: A implies B. Justification: hypothesis. Line two: B implies C. Justification: hypothesis. Line three: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis. Justification: the first conditional axiom scheme. Line four: A implies open parenthesis B implies C close parenthesis. Justification: modus ponens from lines two and three. Line five is printed in two formula segments. Segment one: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line. Segment two: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Justification: the second conditional axiom scheme. Line six: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Justification: modus ponens from lines four and five. Line seven: A implies C. Justification: modus ponens from lines one and six. Resolved reference one: Reference to the first conditional axiom scheme. Resolved reference two: Reference to the second conditional axiom scheme.

Three-line derivation by modus ponens

The derivation takes A and the conditional from A to B as hypotheses, then obtains B by modus ponens.

  1. Line one: A. Justification: hypothesis.
  2. Line two: A implies B. Justification: hypothesis.
  3. Line three: B. Justification: modus ponens from lines one and two.

Words-only linearization: Three-line derivation by modus ponens. The derivation takes A and the conditional from A to B as hypotheses, then obtains B by modus ponens. Line one: A. Justification: hypothesis. Line two: A implies B. Justification: hypothesis. Line three: B. Justification: modus ponens from lines one and two.

Three-line conditional-elimination derivation

The derivation takes A and the conditional from A to B as hypotheses and obtains B by modus ponens.

  1. Line one: A. Justification: hypothesis.
  2. Line two: A implies B. Justification: hypothesis.
  3. Line three: B. Justification: modus ponens from lines one and two.

Words-only linearization: Three-line conditional-elimination derivation. The derivation takes A and the conditional from A to B as hypotheses and obtains B by modus ponens. Line one: A. Justification: hypothesis. Line two: A implies B. Justification: hypothesis. Line three: B. Justification: modus ponens from lines one and two.

44 formal objects

  1. Definition of an axiomatic derivation from Gamma — rules-and-proofs.tex, line 24.
  2. Definition of a rule of inference — rules-and-proofs.tex, line 43.
  3. Definition of derivability in Rules and derivations — rules-and-proofs.tex, line 83.
  4. Definition of theoremhood in Rules and derivations — rules-and-proofs.tex, line 89.
  5. Definition of the propositional axiom set — axioms-rules-propositional.tex, line 15.
  6. The fourteen propositional axiom schemes — axioms-rules-propositional.tex, line 18.
  7. Definition of modus ponens — axioms-rules-propositional.tex, line 36.
  8. Example deriving the conditional from not D or E to the conditional from D to E — proving-things.tex, line 16.
  9. Five-line derivation from not D or E to D implies E — proving-things.tex, line 31.
  10. Example deriving the identity conditional — proving-things.tex, line 41.
  11. Five-line derivation of D implies D — proving-things.tex, line 72.
  12. Example chaining two conditionals — proving-things.tex, line 82.
  13. Seven-line derivation chaining A implies B and B implies C — proving-things.tex, line 87.
  14. Proposition: chaining derivable conditionals — proving-things.tex, line 101.
  15. Exercise: three derivations from the propositional axioms — proving-things.tex, line 120; preserved unsolved prompt.
  16. Definition of derivability in Proof-Theoretic Notions — proof-theoretic-notions.tex, line 26.
  17. Definition of theoremhood in Proof-Theoretic Notions — proof-theoretic-notions.tex, line 32.
  18. Definition of consistency — proof-theoretic-notions.tex, line 38.
  19. Proposition: reflexivity of derivability — proof-theoretic-notions.tex, line 43.
  20. Proposition: monotonicity of derivability — proof-theoretic-notions.tex, line 52.
  21. Proposition: transitivity of derivability — proof-theoretic-notions.tex, line 63.
  22. Proposition: inconsistency and derivability of every formula — proof-theoretic-notions.tex, line 91.
  23. Exercise: prove the inconsistency characterization — proof-theoretic-notions.tex, line 107; preserved unsolved prompt.
  24. Proposition: compactness of axiomatic derivability — proof-theoretic-notions.tex, line 112.
  25. Proposition: meta-level modus ponens — deduction-theorem.tex, line 31.
  26. Three-line derivation by modus ponens — deduction-theorem.tex, line 38.
  27. The Deduction Theorem — deduction-theorem.tex, line 49.
  28. The two induction-hypothesis consequences — deduction-theorem.tex, line 84.
  29. Proposition: five useful derivability facts — deduction-theorem.tex, line 103.
  30. Exercise: prove the five derivability facts — deduction-theorem.tex, line 127; preserved unsolved prompt.
  31. Proposition: removing a provable assumption from an inconsistency — provability-consistency.tex, line 19.
  32. Proposition: derivability characterized by inconsistency with a negation — provability-consistency.tex, line 33.
  33. Exercise: characterize derivability of a negation by inconsistency — provability-consistency.tex, line 55; preserved unsolved prompt.
  34. Proposition: an explicit contradiction makes Gamma inconsistent — provability-consistency.tex, line 60.
  35. Proposition: two inconsistent opposite extensions make Gamma inconsistent — provability-consistency.tex, line 71.
  36. Exercise: prove the opposite-extensions proposition — provability-consistency.tex, line 87; preserved unsolved prompt.
  37. Proposition: derivability principles for conjunction — provability-propositional.tex, line 23.
  38. Proposition: derivability principles for disjunction — provability-propositional.tex, line 41.
  39. Proposition: derivability principles for the conditional — provability-propositional.tex, line 62.
  40. Three-line conditional-elimination derivation — provability-propositional.tex, line 73.
  41. Proposition: every propositional axiom is a tautology — soundness.tex, line 34.
  42. Theorem: soundness of axiomatic deduction — soundness.tex, line 54.
  43. Corollary: every theorem is a tautology — soundness.tex, line 119.
  44. Corollary: every satisfiable premise set is consistent — soundness.tex, line 124.

57 resolved references

  1. Reference to the third disjunction axiom scheme — proving-things.tex, line 21.
  2. Reference to the second negation axiom scheme — proving-things.tex, line 29.
  3. Reference to the first conditional axiom scheme — proving-things.tex, line 30.
  4. Reference to the second negation axiom scheme — proving-things.tex, line 32.
  5. Reference to the third disjunction axiom scheme — proving-things.tex, line 34.
  6. Reference to the first conditional axiom scheme — proving-things.tex, line 36.
  7. Reference to the first conditional axiom scheme — proving-things.tex, line 44.
  8. Reference to the first conditional axiom scheme — proving-things.tex, line 49.
  9. Reference to the second conditional axiom scheme — proving-things.tex, line 58.
  10. Reference to the second conditional axiom scheme — proving-things.tex, line 64.
  11. Reference to the first conditional axiom scheme — proving-things.tex, line 69.
  12. Reference to the first conditional axiom scheme — proving-things.tex, line 70.
  13. Reference to the first conditional axiom scheme — proving-things.tex, line 73.
  14. Reference to the second conditional axiom scheme — proving-things.tex, line 75.
  15. Reference to the first conditional axiom scheme — proving-things.tex, line 77.
  16. Reference to the first conditional axiom scheme — proving-things.tex, line 90.
  17. Reference to the second conditional axiom scheme — proving-things.tex, line 93.
  18. Reference to the proposition characterizing inconsistency by derivability — proof-theoretic-notions.tex, line 108.
  19. Reference to the reflexivity proposition for derivability — deduction-theorem.tex, line 23.
  20. Reference to the monotonicity proposition for derivability — deduction-theorem.tex, line 25.
  21. Reference to the transitivity proposition for derivability — deduction-theorem.tex, line 27.
  22. Reference to the transitivity proposition for derivability — deduction-theorem.tex, line 43.
  23. Reference to the monotonicity proposition for derivability — deduction-theorem.tex, line 57.
  24. Reference to the reflexivity proposition for derivability — deduction-theorem.tex, line 58.
  25. Reference to the meta-level modus ponens proposition — deduction-theorem.tex, line 58.
  26. Reference to the first conditional axiom scheme — deduction-theorem.tex, line 69.
  27. Reference to the meta-level modus ponens proposition — deduction-theorem.tex, line 70.
  28. Reference to the example deriving the identity conditional — deduction-theorem.tex, line 73.
  29. Reference to the second conditional axiom scheme — deduction-theorem.tex, line 93.
  30. Reference to the meta-level modus ponens proposition — deduction-theorem.tex, line 93.
  31. Reference to the first conditional axiom scheme — deduction-theorem.tex, line 97.
  32. Reference to the second conditional axiom scheme — deduction-theorem.tex, line 97.
  33. Reference to the proposition listing five useful derivability facts — deduction-theorem.tex, line 128.
  34. Reference to the reflexivity proposition for derivability — provability-consistency.tex, line 26.
  35. Reference to the transitivity proposition for derivability — provability-consistency.tex, line 29.
  36. Reference to the monotonicity proposition for derivability — provability-consistency.tex, line 40.
  37. Reference to the reflexivity proposition for derivability — provability-consistency.tex, line 41.
  38. Reference to the second negation axiom scheme — provability-consistency.tex, line 42.
  39. Reference to the meta-level modus ponens proposition — provability-consistency.tex, line 43.
  40. Reference to the second falsity axiom scheme — provability-consistency.tex, line 49.
  41. Reference to the meta-level modus ponens proposition — provability-consistency.tex, line 50.
  42. Reference to the double-negation-elimination axiom scheme — provability-consistency.tex, line 51.
  43. Reference to the meta-level modus ponens proposition — provability-consistency.tex, line 52.
  44. Reference to the second negation axiom scheme — provability-consistency.tex, line 66.
  45. Reference to the meta-level modus ponens proposition — provability-consistency.tex, line 67.
  46. Reference to the proposition about two inconsistent opposite extensions — provability-consistency.tex, line 88.
  47. Reference to the first conjunction axiom scheme — provability-propositional.tex, line 33.
  48. Reference to the second conjunction axiom scheme — provability-propositional.tex, line 33. Reader correction: The frozen proof cites the first conjunction-elimination axiom twice. The two conclusions require the first and second conjunction-elimination axioms, so the reader names axiom land two for the second citation.
  49. Reference to the third conjunction axiom scheme — provability-propositional.tex, line 35.
  50. Reference to the first negation axiom scheme — provability-propositional.tex, line 50.
  51. Reference to the third disjunction axiom scheme — provability-propositional.tex, line 54.
  52. Reference to the first disjunction axiom scheme — provability-propositional.tex, line 57.
  53. Reference to the second disjunction axiom scheme — provability-propositional.tex, line 57.
  54. Reference to the second negation axiom scheme — provability-propositional.tex, line 79.
  55. Reference to the first conditional axiom scheme — provability-propositional.tex, line 79.
  56. Reference to the Semantic Deduction Theorem — soundness.tex, line 77.
  57. Reference to the soundness theorem for axiomatic deduction — soundness.tex, line 132.