The Open Logic Text — accessible offline edition

The Sequent Calculus — Explore equations

The Sequent Calculus

Reading preferences

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

Equation and object guide

Every distinct expression, formal object, proof diagram, source reference, and disclosed printed-source concern is indexed here.

280 expression records

Expression 2

¬(A→B)⇒A\lnot(!A \lif !B) \Sequent !A

Conventional reading: antecedent containing the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 3

Γ0∪Δ0⊆Γ∪Δ\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta

Conventional reading: the union of Gamma sub zero and capital Delta sub zero is a subset of the union of Gamma and capital Delta

Meaning here: The finite-premise-set inclusion is read 'the union of Gamma sub zero and capital Delta sub zero is a subset of the union of Gamma and capital Delta' and states that every member of the set on the left belongs to the set on the right.

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

Expression 4

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

Conventional reading: the disjunction of the negation of formula A and formula B

Meaning here: The propositional formula is read 'the disjunction of the negation of formula A and formula B'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

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

Expression 5

A∧B⇒A!A\land !B \fCenter !A

Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: proving-things.tex, line 22, column 10
  2. Occurrence 2: proving-things.tex, line 34, column 10
  3. Occurrence 3: proving-things.tex, line 44, column 10

Expression 6

¬(A∧B)⇒¬A∨¬B\lnot(!A \land !B) \Sequent \lnot !A \lor \lnot !B

Conventional reading: antecedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis; sequent arrow; succedent containing the disjunction of the negation of formula A and the negation of formula B

Meaning here: The sequent read 'antecedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis; sequent arrow; succedent containing the disjunction of the negation of formula A and the negation of formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 7

A⇒A∨B!A \fCenter !A \lor !B

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 8

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

Conventional reading: antecedent containing the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is formula B; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is formula B; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 11

A,¬A⇒!A, \lnot !A \fCenter

Conventional reading: antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 92, column 14
  2. Occurrence 2: provability-propositional.tex, line 123, column 18

Expression 12

A⇒B!A \fCenter !B

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 13

C∈Γ!C \in \Gamma

Conventional reading: formula C is a member of Gamma

Meaning here: The membership statement is read 'formula C is a member of Gamma'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

9 occurrences
  1. Occurrence 1: soundness.tex, line 93, column 24
  2. Occurrence 2: soundness.tex, line 97, column 54
  3. Occurrence 3: soundness.tex, line 116, column 23
  4. Occurrence 4: soundness.tex, line 122, column 17
  5. Occurrence 5: soundness.tex, line 146, column 51
  6. Occurrence 6: soundness.tex, line 150, column 66
  7. Occurrence 7: soundness.tex, line 173, column 51
  8. Occurrence 8: soundness.tex, line 176, column 17
  9. Occurrence 9: soundness.tex, line 201, column 64

Expression 14

Θ=A∧B,Γ\Theta = !A \land !B, \Gamma

Conventional reading: capital Theta equals first the conjunction of formula A and formula B, then Gamma

Meaning here: The identity read 'capital Theta equals first the conjunction of formula A and formula B, then Gamma' identifies capital Theta, the antecedent sequence of the soundness proof's end-sequent, with first the conjunction of formula A and formula B, then Gamma.

1 occurrence
  1. Occurrence 1: soundness.tex, line 141, column 7

Expression 16

A,¬A∨B⇒!A, \lnot !A \lor !B \Sequent \quad

Conventional reading: antecedent containing first formula A, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 18

C,B⇒A!C, !B \fCenter !A

Conventional reading: antecedent containing first formula C, then formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing first formula C, then formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 19

⇒¬(A∧¬A)\Sequent \lnot(!A \land \lnot !A)

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and the negation of formula A, close parenthesis

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and the negation of formula A, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 21

v⊭B\pSat/{v}{!B}

Conventional reading: valuation v does not satisfy formula B

Meaning here: The valuation claim 'valuation v does not satisfy formula B' states exactly whether the named propositional valuation makes the formula true.

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

Expression 22

A,Π⇒Λ!A, \Pi \fCenter \Lambda

Conventional reading: antecedent containing first formula A, then capital Pi; sequent arrow; succedent containing capital Lambda

Meaning here: The sequent read 'antecedent containing first formula A, then capital Pi; sequent arrow; succedent containing capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 275, column 12

Expression 23

C⇒C!C \fCenter !C

Conventional reading: antecedent containing formula C; sequent arrow; succedent containing formula C

Meaning here: The sequent read 'antecedent containing formula C; sequent arrow; succedent containing formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: derivations.tex, line 52, column 7
  2. Occurrence 2: derivations.tex, line 60, column 7
  3. Occurrence 3: derivations.tex, line 94, column 7
  4. Occurrence 4: derivations.tex, line 111, column 7

Expression 24

¬B,A⇒\lnot !B, !A \fCenter

Conventional reading: antecedent containing first the negation of formula B, then formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula B, then formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 26

Θ=A,Γ\Theta = !A, \Gamma

Conventional reading: capital Theta equals first formula A, then Gamma

Meaning here: The identity read 'capital Theta equals first formula A, then Gamma' identifies capital Theta, the antecedent sequence of the soundness proof's end-sequent, with first formula A, then Gamma.

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

Expression 27

¬A∨¬B⇒¬(A∧B)\lnot !A \lor \lnot !B \Sequent \lnot(!A \land !B)

Conventional reading: antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis

Meaning here: The sequent read 'antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 28

A→B,Γ,Π⇒Δ,Λ!A \lif !B, \Gamma, \Pi \fCenter \Delta, \Lambda

Conventional reading: antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then Gamma, and finally capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda

Meaning here: The sequent read 'antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then Gamma, and finally capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 79, column 11
  2. Occurrence 2: soundness.tex, line 316, column 15

Expression 29

π1\pi_1

Conventional reading: pi sub one

Meaning here: Pi sub one denotes the second cited sequent-calculus derivation.

8 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 112, column 45
  2. Occurrence 2: proof-theoretic-notions.tex, line 119, column 15
  3. Occurrence 3: provability-consistency.tex, line 29, column 20
  4. Occurrence 4: provability-consistency.tex, line 35, column 13
  5. Occurrence 5: provability-consistency.tex, line 57, column 17
  6. Occurrence 6: provability-consistency.tex, line 64, column 15
  7. Occurrence 7: provability-consistency.tex, line 107, column 62
  8. Occurrence 8: provability-consistency.tex, line 117, column 13

Expression 30

A⊢B!A \Proves !B

Conventional reading: formula A syntactically derives formula B

Meaning here: In the current L K sequent calculus, 'formula A syntactically derives formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 31

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

Conventional reading: antecedent containing first formula A, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula A, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

5 occurrences
  1. Occurrence 1: proving-things.tex, line 72, column 10
  2. Occurrence 2: proving-things.tex, line 87, column 10
  3. Occurrence 3: proving-things.tex, line 105, column 10
  4. Occurrence 4: proving-things.tex, line 126, column 10
  5. Occurrence 5: proving-things.tex, line 148, column 10

Expression 32

𝔳\pAssign{v}

Conventional reading: valuation v

Meaning here: The fraktur letter v names a propositional truth-value assignment.

28 occurrences
  1. Occurrence 1: soundness.tex, line 43, column 23
  2. Occurrence 2: soundness.tex, line 49, column 21
  3. Occurrence 3: soundness.tex, line 63, column 49
  4. Occurrence 4: soundness.tex, line 92, column 57
  5. Occurrence 5: soundness.tex, line 115, column 55
  6. Occurrence 6: soundness.tex, line 121, column 21
  7. Occurrence 7: soundness.tex, line 143, column 24
  8. Occurrence 8: soundness.tex, line 155, column 9
  9. Occurrence 9: soundness.tex, line 156, column 45
  10. Occurrence 10: soundness.tex, line 170, column 59
  11. Occurrence 11: soundness.tex, line 179, column 40
  12. Occurrence 12: soundness.tex, line 181, column 35
  13. Occurrence 13: soundness.tex, line 193, column 29
  14. Occurrence 14: soundness.tex, line 204, column 35
  15. Occurrence 15: soundness.tex, line 206, column 29
  16. Occurrence 16: soundness.tex, line 279, column 51
  17. Occurrence 17: soundness.tex, line 281, column 32
  18. Occurrence 18: soundness.tex, line 284, column 33
  19. Occurrence 19: soundness.tex, line 287, column 29
  20. Occurrence 20: soundness.tex, line 289, column 29
  21. Occurrence 21: soundness.tex, line 300, column 24
  22. Occurrence 22: soundness.tex, line 301, column 29
  23. Occurrence 23: soundness.tex, line 319, column 59
  24. Occurrence 24: soundness.tex, line 320, column 41
  25. Occurrence 25: soundness.tex, line 323, column 29
  26. Occurrence 26: soundness.tex, line 360, column 55
  27. Occurrence 27: soundness.tex, line 376, column 55
  28. Occurrence 28: soundness.tex, line 380, column 27

Expression 33

Γ,Π⇒Δ,Λ\Gamma, \Pi \Sequent \Delta, \Lambda

Conventional reading: antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda

Meaning here: The sequent read 'antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: soundness.tex, line 321, column 3
  2. Occurrence 2: soundness.tex, line 323, column 60

Expression 35

Γ⇒Δ,AA,Π⇒ΛcutΓ,Π⇒Δ,Λ\Axiom$ \Gamma \fCenter \Delta, !A$ \Axiom$ !A, \Pi \fCenter \Lambda $ \RightLabel{\Cut} \BinaryInf$ \Gamma, \Pi \fCenter \Delta, \Lambda$ \DisplayProof

Conventional reading: Premise or initial sequent: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A. Premise or initial sequent: antecedent containing first formula A, then capital Pi; sequent arrow; succedent containing capital Lambda. The next inference is labeled cut rule. From the two immediately preceding branches using the cut rule, infer antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda. The source ends this displayed proof segment here.

Meaning here: A two-premise cut inference: the first premise has A on the right, the second has A on the left, and the conclusion removes that cut formula while concatenating the remaining sides.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 71, column 1

Expression 36

A⇒A,B!A \fCenter !A, !B

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing first formula A, then formula B

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing first formula A, then formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 37

LWeakening\LeftR{\Weakening}

Conventional reading: left weakening rule

Meaning here: The label 'left weakening rule' names the side of the sequent and the connective or structural operation governed by this inference rule.

1 occurrence
  1. Occurrence 1: derivations.tex, line 40, column 1

Expression 38

Γ0⇒\Gamma_0 \Sequent \quad

Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

5 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 72, column 13
  2. Occurrence 2: proof-theoretic-notions.tex, line 74, column 32
  3. Occurrence 3: proof-theoretic-notions.tex, line 165, column 19
  4. Occurrence 4: soundness.tex, line 374, column 4
  5. Occurrence 5: soundness.tex, line 375, column 1

Expression 39

A,Γ1⇒!A, \Gamma_1 \Sequent \quad

Conventional reading: antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 26, column 51

Expression 40

C,D⇒D!C, !D \fCenter !D

Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula D

Meaning here: The sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula D' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: derivations.tex, line 78, column 10
  2. Occurrence 2: derivations.tex, line 101, column 10
  3. Occurrence 3: derivations.tex, line 110, column 10

Expression 41

Γ,B,A,Π⇒Δ,\Gamma, !B, !A, \Pi \fCenter \Delta,

Conventional reading: antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta, followed by a printed trailing comma with no following formula

Meaning here: The printed sequent is read 'antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta, followed by a printed trailing comma with no following formula'. Its final comma is preserved and leaves a following succedent entry unstated; no formula is supplied by this projection.

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

Expression 43

π0\pi_0

Conventional reading: pi sub zero

Meaning here: Pi sub zero denotes the first cited sequent-calculus derivation.

7 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 110, column 21
  2. Occurrence 2: proof-theoretic-notions.tex, line 116, column 15
  3. Occurrence 3: provability-consistency.tex, line 28, column 8
  4. Occurrence 4: provability-consistency.tex, line 32, column 13
  5. Occurrence 5: provability-consistency.tex, line 52, column 17
  6. Occurrence 6: provability-consistency.tex, line 107, column 50
  7. Occurrence 7: provability-consistency.tex, line 112, column 13

Expression 44

B→A⇒¬A→¬B!B \lif !A \Sequent \lnot !A \lif \lnot !B

Conventional reading: antecedent containing the conditional whose antecedent is formula B; and whose consequent is formula A; sequent arrow; succedent containing the conditional whose antecedent is the negation of formula A; and whose consequent is the negation of formula B

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is formula B; and whose consequent is formula A; sequent arrow; succedent containing the conditional whose antecedent is the negation of formula A; and whose consequent is the negation of formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 45

L¬\LeftR{\lnot}

Conventional reading: left negation rule

Meaning here: The label 'left negation rule' names the side of the sequent and the connective or structural operation governed by this inference rule.

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

Expression 46

A,B⇒A∧B!A, !B \Sequent !A \land !B

Conventional reading: antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 47

A⇒A∨B!A \Sequent !A \lor !B

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 48

Γ0′′⇒A\Gamma_0'' \Sequent !A

Conventional reading: antecedent containing Gamma sub zero double prime; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing Gamma sub zero double prime; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 49

¬A,Γ⇒Δ\lnot !A, \Gamma \fCenter \Delta

Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 20, column 10
  2. Occurrence 2: soundness.tex, line 110, column 14

Expression 50

B⇒A∨B!B \Sequent !A \lor !B

Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 51

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: propositional-rules.tex, line 47, column 11
  2. Occurrence 2: derivations.tex, line 86, column 11
  3. Occurrence 3: soundness.tex, line 297, column 15

Expression 52

Γ0⇒A\Gamma_0 \fCenter !A

Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

3 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 117, column 10
  2. Occurrence 2: provability-consistency.tex, line 33, column 8
  3. Occurrence 3: provability-consistency.tex, line 87, column 12

Expression 53

Δ=⟨B1,…,Bn⟩\Delta = \tuple{!B_1, \dots, !B_n}

Conventional reading: capital Delta equals the finite sequence first formula B sub one, continuing through the omitted intermediate entries, and finally formula B sub n

Meaning here: The identity read 'capital Delta equals the finite sequence first formula B sub one, continuing through the omitted intermediate entries, and finally formula B sub n' defines capital Delta to be the finite sequence first formula B sub one, continuing through the omitted intermediate entries, and finally formula B sub n, an ordered finite sequence.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 32, column 1

Expression 54

Γ0′=⟨B,B,C⟩\Gamma_0' = \tuple{!B, !B, !C}

Conventional reading: Gamma sub zero prime equals the finite sequence first formula B, then formula B, and finally formula C

Meaning here: The identity read 'Gamma sub zero prime equals the finite sequence first formula B, then formula B, and finally formula C' defines Gamma sub zero prime to be the finite sequence first formula B, then formula B, and finally formula C, an ordered finite sequence.

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

Expression 55

¬B,A∧B⇒\lnot !B, !A \land !B \fCenter

Conventional reading: antecedent containing first the negation of formula B, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula B, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 218, column 10
  2. Occurrence 2: proving-things.tex, line 239, column 10

Expression 56

A,Γ0⇒!A, \Gamma_0 \Sequent \quad

Conventional reading: antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 57

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

Conventional reading: antecedent containing first the disjunction of the negation of formula A and formula B, then formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first the disjunction of the negation of formula A and formula B, then formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 85, column 11
  2. Occurrence 2: proving-things.tex, line 103, column 11
  3. Occurrence 3: proving-things.tex, line 124, column 11
  4. Occurrence 4: proving-things.tex, line 146, column 11

Expression 58

B,B,C⇒A!B, !B, !C \fCenter !A

Conventional reading: antecedent containing first formula B, then formula B, and finally formula C; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing first formula B, then formula B, and finally formula C; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 59

⇒A∨¬A,A∨¬A\fCenter !A \lor \lnot !A, !A \lor \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing first the disjunction of formula A and the negation of formula A, then the disjunction of formula A and the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing first the disjunction of formula A and the negation of formula A, then the disjunction of formula A and the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 279, column 10
  2. Occurrence 2: proving-things.tex, line 294, column 10

Expression 60

¬A,Γ1⇒\lnot !A, \Gamma_1 \fCenter

Conventional reading: antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 61

A,B⇒B!A, !B \fCenter !B

Conventional reading: antecedent containing first formula A, then formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 99, column 10
  2. Occurrence 2: proving-things.tex, line 120, column 10
  3. Occurrence 3: proving-things.tex, line 142, column 10
  4. Occurrence 4: provability-propositional.tex, line 131, column 18

Expression 62

A,Γ!A, \Gamma

Conventional reading: first formula A, then Gamma

Meaning here: The ordered finite formula sequence is read 'first formula A, then Gamma'; the source uses that order in its sequent or inconsistency argument.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 47, column 64

Expression 63

A,¬A⇒B!A, \lnot !A \fCenter !B

Conventional reading: antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 64

A∧(B∧C)⇒(A∧B)∧C!A \land (!B \land !C) \Sequent (!A \land !B) \land !C

Conventional reading: antecedent containing the conjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis; sequent arrow; succedent containing the conjunction of open parenthesis, the conjunction of formula A and formula B, close parenthesis and formula C

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and open parenthesis, the conjunction of formula B and formula C, close parenthesis; sequent arrow; succedent containing the conjunction of open parenthesis, the conjunction of formula A and formula B, close parenthesis and formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 65

¬A∨¬B⇒¬(A∧B)\lnot !A \lor \lnot !B \Sequent \lnot (!A \land !B)

Conventional reading: antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis

Meaning here: The sequent read 'antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 66

⇒A∨¬A\fCenter !A \lor \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 261, column 10
  2. Occurrence 2: proving-things.tex, line 268, column 10
  3. Occurrence 3: proving-things.tex, line 281, column 10
  4. Occurrence 4: proving-things.tex, line 296, column 10

Expression 67

A,Γ0⇒!A, \Gamma_0 \fCenter

Conventional reading: antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 68

¬A⇒A→B\lnot !A \fCenter !A \lif !B

Conventional reading: antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 69

Θ⇒Ξ\Theta \Sequent \Xi

Conventional reading: antecedent containing capital Theta; sequent arrow; succedent containing capital Xi

Meaning here: The sequent read 'antecedent containing capital Theta; sequent arrow; succedent containing capital Xi' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

9 occurrences
  1. Occurrence 1: soundness.tex, line 53, column 59
  2. Occurrence 2: soundness.tex, line 54, column 21
  3. Occurrence 3: soundness.tex, line 58, column 33
  4. Occurrence 4: soundness.tex, line 75, column 48
  5. Occurrence 5: soundness.tex, line 102, column 36
  6. Occurrence 6: soundness.tex, line 119, column 62
  7. Occurrence 7: soundness.tex, line 129, column 57
  8. Occurrence 8: soundness.tex, line 180, column 47
  9. Occurrence 9: soundness.tex, line 182, column 3

Expression 70

Γ⇒Δ,B\Gamma \fCenter \Delta, !B

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: propositional-rules.tex, line 45, column 7
  2. Occurrence 2: propositional-rules.tex, line 66, column 7
  3. Occurrence 3: derivations.tex, line 84, column 7
  4. Occurrence 4: soundness.tex, line 295, column 12

Expression 71

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 304, column 58

Expression 72

¬A,Γ0⇒\lnot !A, \Gamma_0 \Sequent \quad

Conventional reading: antecedent containing first the negation of formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 83, column 11

Expression 74

A,B⇒A∧B!A, !B \fCenter !A \land !B

Conventional reading: antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 75

¬A∨¬B,A∧B⇒\lnot !A \lor \lnot !B, !A \land !B \fCenter

Conventional reading: antecedent containing first the disjunction of the negation of formula A and the negation of formula B, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the disjunction of the negation of formula A and the negation of formula B, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 221, column 11
  2. Occurrence 2: proving-things.tex, line 242, column 11

Expression 76

⇒(A→B)∨(B→C)\Sequent (!A \lif !B) \lor (!B \lif !C)

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the disjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the disjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 77

Γ⇒A\Gamma \fCenter !A

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 67, column 13

Expression 78

Γ0,Δ0⇒B\Gamma_0, \Delta_0 \fCenter !B

Conventional reading: antecedent containing first Gamma sub zero, then capital Delta sub zero; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first Gamma sub zero, then capital Delta sub zero; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 79

Γ,B,A,Π⇒Δ\Gamma, !B, !A, \Pi \fCenter \Delta

Conventional reading: antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 56, column 10

Expression 80

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

Conventional reading: the union of the set containing formula A and capital Delta syntactically derives formula B

Meaning here: In the current L K sequent calculus, 'the union of the set containing formula A and capital Delta syntactically derives formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 104, column 28
  2. Occurrence 2: proof-theoretic-notions.tex, line 110, column 60

Expression 81

A∧B,¬A∨¬B⇒!A \land !B, \lnot !A \lor \lnot !B \fCenter

Conventional reading: antecedent containing first the conjunction of formula A and formula B, then the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the conjunction of formula A and formula B, then the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

5 occurrences
  1. Occurrence 1: proving-things.tex, line 171, column 10
  2. Occurrence 2: proving-things.tex, line 185, column 10
  3. Occurrence 3: proving-things.tex, line 204, column 10
  4. Occurrence 4: proving-things.tex, line 223, column 10
  5. Occurrence 5: proving-things.tex, line 244, column 10

Expression 82

v⊨C\pSat{v}{!C}

Conventional reading: valuation v satisfies formula C

Meaning here: The valuation claim 'valuation v satisfies formula C' states exactly whether the named propositional valuation makes the formula true.

12 occurrences
  1. Occurrence 1: soundness.tex, line 95, column 21
  2. Occurrence 2: soundness.tex, line 100, column 17
  3. Occurrence 3: soundness.tex, line 101, column 29
  4. Occurrence 4: soundness.tex, line 118, column 12
  5. Occurrence 5: soundness.tex, line 125, column 3
  6. Occurrence 6: soundness.tex, line 147, column 7
  7. Occurrence 7: soundness.tex, line 153, column 8
  8. Occurrence 8: soundness.tex, line 174, column 7
  9. Occurrence 9: soundness.tex, line 178, column 25
  10. Occurrence 10: soundness.tex, line 198, column 7
  11. Occurrence 11: soundness.tex, line 201, column 3
  12. Occurrence 12: soundness.tex, line 203, column 25

Expression 83

Γ\Gamma

Conventional reading: Gamma

Meaning here: Gamma is context-sensitive: it denotes a sequent antecedent sequence or a premise set, as stated by every exact occurrence record.

30 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 23, column 7
  2. Occurrence 2: rules-and-proofs.tex, line 24, column 42
  3. Occurrence 3: rules-and-proofs.tex, line 38, column 43
  4. Occurrence 4: rules-and-proofs.tex, line 39, column 25
  5. Occurrence 5: rules-and-proofs.tex, line 46, column 4
  6. Occurrence 6: rules-and-proofs.tex, line 47, column 50
  7. Occurrence 7: rules-and-proofs.tex, line 49, column 4
  8. Occurrence 8: derivations.tex, line 49, column 1
  9. Occurrence 9: derivations.tex, line 72, column 6
  10. Occurrence 10: derivations.tex, line 89, column 57
  11. Occurrence 11: proof-theoretic-notions.tex, line 38, column 15
  12. Occurrence 12: proof-theoretic-notions.tex, line 41, column 61
  13. Occurrence 13: proof-theoretic-notions.tex, line 70, column 20
  14. Occurrence 14: proof-theoretic-notions.tex, line 72, column 43
  15. Occurrence 15: proof-theoretic-notions.tex, line 135, column 1
  16. Occurrence 16: proof-theoretic-notions.tex, line 152, column 35
  17. Occurrence 17: proof-theoretic-notions.tex, line 153, column 22
  18. Occurrence 18: proof-theoretic-notions.tex, line 163, column 14
  19. Occurrence 19: proof-theoretic-notions.tex, line 166, column 24
  20. Occurrence 20: provability-consistency.tex, line 21, column 22
  21. Occurrence 21: provability-consistency.tex, line 42, column 50
  22. Occurrence 22: provability-consistency.tex, line 76, column 58
  23. Occurrence 23: provability-consistency.tex, line 97, column 14
  24. Occurrence 24: provability-consistency.tex, line 102, column 22
  25. Occurrence 25: provability-consistency.tex, line 123, column 50
  26. Occurrence 26: soundness.tex, line 368, column 4
  27. Occurrence 27: soundness.tex, line 372, column 44
  28. Occurrence 28: soundness.tex, line 379, column 41
  29. Occurrence 29: soundness.tex, line 380, column 52
  30. Occurrence 30: soundness.tex, line 381, column 1

Expression 85

A,Γ⇒Δ!A, \Gamma \fCenter \Delta

Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

8 occurrences
  1. Occurrence 1: propositional-rules.tex, line 23, column 7
  2. Occurrence 2: propositional-rules.tex, line 33, column 7
  3. Occurrence 3: propositional-rules.tex, line 54, column 7
  4. Occurrence 4: structural-rules.tex, line 28, column 10
  5. Occurrence 5: structural-rules.tex, line 42, column 10
  6. Occurrence 6: derivations.tex, line 44, column 10
  7. Occurrence 7: soundness.tex, line 83, column 14
  8. Occurrence 8: soundness.tex, line 137, column 12

Expression 86

⇒Δ\quad \Sequent \Delta

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 39, column 59

Expression 87

⇒A\quad \Sequent !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 89

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

Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 82, column 7
  2. Occurrence 2: soundness.tex, line 187, column 12

Expression 90

A⇒B,A!A \fCenter !B, !A

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing first formula B, then formula A

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing first formula B, then formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 115, column 10
  2. Occurrence 2: proving-things.tex, line 137, column 10

Expression 93

C,D⇒C∧D!C, !D \fCenter !C \land !D

Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D

Meaning here: The sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: derivations.tex, line 103, column 11

Expression 94

A,Δ0⇒B!A, \Delta_0 \fCenter !B

Conventional reading: antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 95

v⊭¬A\pSat/{v}{\lnot !A}

Conventional reading: valuation v does not satisfy the negation of formula A

Meaning here: The valuation claim 'valuation v does not satisfy the negation of formula A' states exactly whether the named propositional valuation makes the formula true.

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

Expression 97

C∈Δ,A→B!C \in \Delta, !A \lif !B

Conventional reading: formula C is a member of the sequence formed by first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The membership statement is read 'formula C is a member of the sequence formed by first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 200, column 21

Expression 98

¬A,A∧B⇒\lnot !A, !A \land !B \fCenter

Conventional reading: antecedent containing first the negation of formula A, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then the conjunction of formula A and formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 215, column 10
  2. Occurrence 2: proving-things.tex, line 233, column 10

Expression 99

LExchange\LeftR{\Exchange}

Conventional reading: left exchange rule

Meaning here: The label 'left exchange rule' names the side of the sequent and the connective or structural operation governed by this inference rule.

1 occurrence
  1. Occurrence 1: derivations.tex, line 56, column 36

Expression 100

LK\Log{LK}

Conventional reading: the sequent calculus L K

Meaning here: L K is the classical sequent calculus defined and used in this chapter.

19 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 66, column 50
  2. Occurrence 2: derivations.tex, line 23, column 14
  3. Occurrence 3: derivations.tex, line 24, column 10
  4. Occurrence 4: derivations.tex, line 34, column 36
  5. Occurrence 5: derivations.tex, line 34, column 52
  6. Occurrence 6: proving-things.tex, line 16, column 9
  7. Occurrence 7: proving-things.tex, line 46, column 23
  8. Occurrence 8: proving-things.tex, line 51, column 9
  9. Occurrence 9: proving-things.tex, line 155, column 9
  10. Occurrence 10: proof-theoretic-notions.tex, line 32, column 4
  11. Occurrence 11: proof-theoretic-notions.tex, line 40, column 46
  12. Occurrence 12: proof-theoretic-notions.tex, line 71, column 53
  13. Occurrence 13: proof-theoretic-notions.tex, line 74, column 1
  14. Occurrence 14: proof-theoretic-notions.tex, line 164, column 52
  15. Occurrence 15: provability-consistency.tex, line 26, column 1
  16. Occurrence 16: provability-consistency.tex, line 27, column 27
  17. Occurrence 17: provability-consistency.tex, line 28, column 24
  18. Occurrence 18: provability-consistency.tex, line 107, column 23
  19. Occurrence 19: soundness.tex, line 53, column 36

Expression 101

⇒A\fCenter !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 102

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

Conventional reading: valuation v satisfies formula A

Meaning here: The valuation claim 'valuation v satisfies formula A' states exactly whether the named propositional valuation makes the formula true.

9 occurrences
  1. Occurrence 1: soundness.tex, line 46, column 1
  2. Occurrence 2: soundness.tex, line 65, column 1
  3. Occurrence 3: soundness.tex, line 119, column 3
  4. Occurrence 4: soundness.tex, line 126, column 21
  5. Occurrence 5: soundness.tex, line 172, column 3
  6. Occurrence 6: soundness.tex, line 283, column 11
  7. Occurrence 7: soundness.tex, line 304, column 3
  8. Occurrence 8: soundness.tex, line 326, column 25
  9. Occurrence 9: soundness.tex, line 363, column 1

Expression 103

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

Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 193, column 64

Expression 104

A→B⇒¬A∨B!A \lif !B \Sequent \lnot !A \lor !B

Conventional reading: antecedent containing the conditional whose antecedent is formula A; and whose consequent is formula B; sequent arrow; succedent containing the disjunction of the negation of formula A and formula B

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is formula A; and whose consequent is formula B; sequent arrow; succedent containing the disjunction of the negation of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 105

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

Conventional reading: Gamma syntactically derives the negation of formula A

Meaning here: In the current L K sequent calculus, 'Gamma syntactically derives the negation of formula A' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 106

C∈Γ0!C \in \Gamma_0

Conventional reading: formula C is a member of Gamma sub zero

Meaning here: The membership statement is read 'formula C is a member of Gamma sub zero'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 377, column 10

Expression 107

Γ⇒Δ,A∨B\Gamma \fCenter \Delta, !A \lor !B

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: propositional-rules.tex, line 63, column 10
  2. Occurrence 2: propositional-rules.tex, line 68, column 10
  3. Occurrence 3: soundness.tex, line 167, column 14

Expression 108

D,C⇒C!D, !C \fCenter !C

Conventional reading: antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C

Meaning here: The sequent read 'antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: derivations.tex, line 54, column 10
  2. Occurrence 2: derivations.tex, line 62, column 10
  3. Occurrence 3: derivations.tex, line 96, column 10
  4. Occurrence 4: derivations.tex, line 113, column 10

Expression 109

B,¬A∨B⇒!B, \lnot !A \lor !B \Sequent \quad

Conventional reading: antecedent containing first formula B, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula B, then the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 110

¬A,Γ⇒\lnot !A, \Gamma \Sequent \quad

Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 53, column 52
  2. Occurrence 2: provability-consistency.tex, line 57, column 28

Expression 111

A,Δ0⇒B!A, \Delta_0 \Sequent !B

Conventional reading: antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 112

A∧B⇒B!A \land !B \fCenter !B

Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 237, column 10
  2. Occurrence 2: provability-propositional.tex, line 46, column 16

Expression 113

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

Conventional reading: first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub n syntactically derives formula B

Meaning here: In the current L K sequent calculus, 'first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub n syntactically derives formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 114

⇒A∨¬A,A\fCenter !A \lor \lnot !A, !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing first the disjunction of formula A and the negation of formula A, then formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing first the disjunction of formula A and the negation of formula A, then formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 277, column 10
  2. Occurrence 2: proving-things.tex, line 292, column 10

Expression 115

Γ0={B,C}\Gamma_0 = \{!B, !C\}

Conventional reading: Gamma sub zero equals the set containing first formula B, then formula C

Meaning here: The identity read 'Gamma sub zero equals the set containing first formula B, then formula C' defines Gamma sub zero to be the set containing first formula B, then formula C, a finite premise set.

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

Expression 116

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: soundness.tex, line 204, column 60
  2. Occurrence 2: soundness.tex, line 206, column 59

Expression 117

v⊭A∧B\pSat/{v}{!A \land !B}

Conventional reading: valuation v does not satisfy the conjunction of formula A and formula B

Meaning here: The valuation claim 'valuation v does not satisfy the conjunction of formula A and formula B' states exactly whether the named propositional valuation makes the formula true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 148, column 16

Expression 118

C,C,B⇒A!C, !C, !B \fCenter !A

Conventional reading: antecedent containing first formula C, then formula C, and finally formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing first formula C, then formula C, and finally formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 119

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

Conventional reading: formula B syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: In the current L K sequent calculus, 'formula B syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 120

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

Conventional reading: first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B

Meaning here: The ordered finite formula sequence is read 'first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B'; the source uses that order in its sequent or inconsistency argument.

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

Expression 121

(A→B)→A⇒A(!A \lif !B) \lif !A \Sequent !A

Conventional reading: antecedent containing the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; and whose consequent is formula A; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; and whose consequent is formula A; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 122

Γ0′′=⟨C,C,B⟩\Gamma_0'' = \tuple{!C, !C, !B}

Conventional reading: Gamma sub zero double prime equals the finite sequence first formula C, then formula C, and finally formula B

Meaning here: The identity read 'Gamma sub zero double prime equals the finite sequence first formula C, then formula C, and finally formula B' defines Gamma sub zero double prime to be the finite sequence first formula C, then formula C, and finally formula B, an ordered finite sequence.

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

Expression 123

A!A

Conventional reading: formula A

Meaning here: The metavariable A denotes an arbitrary formula.

21 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 47, column 25
  2. Occurrence 2: rules-and-proofs.tex, line 48, column 37
  3. Occurrence 3: rules-and-proofs.tex, line 60, column 53
  4. Occurrence 4: rules-and-proofs.tex, line 69, column 44
  5. Occurrence 5: derivations.tex, line 46, column 63
  6. Occurrence 6: derivations.tex, line 73, column 1
  7. Occurrence 7: derivations.tex, line 90, column 30
  8. Occurrence 8: derivations.tex, line 105, column 51
  9. Occurrence 9: proving-things.tex, line 180, column 12
  10. Occurrence 10: proof-theoretic-notions.tex, line 31, column 16
  11. Occurrence 11: proof-theoretic-notions.tex, line 33, column 8
  12. Occurrence 12: proof-theoretic-notions.tex, line 37, column 16
  13. Occurrence 13: proof-theoretic-notions.tex, line 41, column 30
  14. Occurrence 14: proof-theoretic-notions.tex, line 136, column 12
  15. Occurrence 15: soundness.tex, line 22, column 27
  16. Occurrence 16: soundness.tex, line 133, column 46
  17. Occurrence 17: soundness.tex, line 158, column 65
  18. Occurrence 18: soundness.tex, line 161, column 46
  19. Occurrence 19: soundness.tex, line 183, column 52
  20. Occurrence 20: soundness.tex, line 348, column 22
  21. Occurrence 21: soundness.tex, line 361, column 52

Expression 124

⊥⇒\lfalse \Sequent \quad

Conventional reading: antecedent containing falsum; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing falsum; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 58, column 24

Expression 125

B,Π⇒Λ!B, \Pi \fCenter \Lambda

Conventional reading: antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda

Meaning here: The sequent read 'antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 77, column 7
  2. Occurrence 2: soundness.tex, line 314, column 12

Expression 126

A∧B⇒A!A \land !B \Sequent !A

Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: proving-things.tex, line 16, column 51
  2. Occurrence 2: proving-things.tex, line 46, column 64
  3. Occurrence 3: provability-propositional.tex, line 37, column 23

Expression 127

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

Conventional reading: formula B syntactically derives the disjunction of formula A and formula B

Meaning here: In the current L K sequent calculus, 'formula B syntactically derives the disjunction of formula A and formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 128

C,D⇒C∧D!C, !D \Sequent !C \land !D

Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D

Meaning here: The sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: derivations.tex, line 91, column 52

Expression 129

R∧\RightR{\land}

Conventional reading: right conjunction rule

Meaning here: The label 'right conjunction rule' names the side of the sequent and the connective or structural operation governed by this inference rule.

1 occurrence
  1. Occurrence 1: derivations.tex, line 81, column 12

Expression 130

v⊨A∧B\pSat{v}{!A \land !B}

Conventional reading: valuation v satisfies the conjunction of formula A and formula B

Meaning here: The valuation claim 'valuation v satisfies the conjunction of formula A and formula B' states exactly whether the named propositional valuation makes the formula true.

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

Expression 131

A⇒A!A \fCenter!A

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 132

⇒A,¬A\fCenter !A, \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 288, column 10
  2. Occurrence 2: provability-consistency.tex, line 62, column 12

Expression 133

¬(A1∧…∧Am)\lnot(!A_1 \land \dots \land !A_m)

Conventional reading: the negation of open parenthesis, the iterated conjunction from formula A sub one through formula A sub m, close parenthesis

Meaning here: The propositional formula is read 'the negation of open parenthesis, the iterated conjunction from formula A sub one through formula A sub m, close parenthesis'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 42, column 1

Expression 134

¬A⇒A→B\lnot !A \Sequent !A \lif !B

Conventional reading: antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 136

Γ,Δ,Π,Λ\Gamma, \Delta, \Pi, \Lambda

Conventional reading: first Gamma, then capital Delta, then capital Pi, and finally capital Lambda

Meaning here: The ordered finite formula sequence is read 'first Gamma, then capital Delta, then capital Pi, and finally capital Lambda'; the source uses that order in its sequent or inconsistency argument.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 15, column 24

Expression 137

v⊨Γ\pSat{v}{\Gamma}

Conventional reading: valuation v satisfies Gamma

Meaning here: The valuation claim 'valuation v satisfies Gamma' states that the named propositional valuation makes every formula in Gamma true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 362, column 4

Expression 138

Γ,Δ\Gamma, \Delta

Conventional reading: first Gamma, then capital Delta

Meaning here: The ordered finite formula sequence is read 'first Gamma, then capital Delta'; the source uses that order in its sequent or inconsistency argument.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 49, column 69

Expression 140

⇒(A→¬A)→¬A\Sequent (!A \lif \lnot !A) \lif \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is the negation of formula A, close parenthesis; and whose consequent is the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is the negation of formula A, close parenthesis; and whose consequent is the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 141

Γ⊢Ai\Gamma \Proves !A_i

Conventional reading: Gamma syntactically derives formula A sub i

Meaning here: In the current L K sequent calculus, 'Gamma syntactically derives formula A sub i' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 142

⇒¬(A→B)→¬B\Sequent \lnot(!A \lif !B) \lif \lnot !B

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; and whose consequent is the negation of formula B

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula B, close parenthesis; and whose consequent is the negation of formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 143

A∧¬C⇒¬(A→C)!A \land \lnot !C \Sequent \lnot (!A \lif !C)

Conventional reading: antecedent containing the conjunction of formula A and the negation of formula C; sequent arrow; succedent containing the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and the negation of formula C; sequent arrow; succedent containing the negation of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 144

Γ,A,B,Π⇒Δ\Gamma, !A, !B, \Pi \fCenter \Delta

Conventional reading: antecedent containing first Gamma, then formula A, then formula B, and finally capital Pi; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first Gamma, then formula A, then formula B, and finally capital Pi; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: structural-rules.tex, line 54, column 7
  2. Occurrence 2: derivations.tex, line 68, column 7

Expression 145

Γ0,Γ1⇒\Gamma_0,\Gamma_1 \fCenter

Conventional reading: antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 38, column 11

Expression 146

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

Conventional reading: first formula A, then the conditional whose antecedent is formula A; and whose consequent is formula B syntactically derives formula B

Meaning here: In the current L K sequent calculus, 'first formula A, then the conditional whose antecedent is formula A; and whose consequent is formula B syntactically derives formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 147

⇒A∨¬A\quad \Sequent !A \lor \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 148

C,D⇒D∧C!C, !D \fCenter !D \land !C

Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula D and formula C

Meaning here: The sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula D and formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: derivations.tex, line 117, column 11

Expression 151

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

Conventional reading: the negation of formula A is a member of Gamma

Meaning here: The membership statement is read 'the negation of formula A is a member of Gamma'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

3 occurrences
  1. Occurrence 1: provability-consistency.tex, line 76, column 30
  2. Occurrence 2: provability-consistency.tex, line 81, column 35
  3. Occurrence 3: provability-consistency.tex, line 96, column 9

Expression 152

Γ⇒Δ,A\Gamma \fCenter \Delta, !A

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

14 occurrences
  1. Occurrence 1: propositional-rules.tex, line 18, column 7
  2. Occurrence 2: propositional-rules.tex, line 44, column 7
  3. Occurrence 3: propositional-rules.tex, line 61, column 7
  4. Occurrence 4: propositional-rules.tex, line 76, column 7
  5. Occurrence 5: structural-rules.tex, line 33, column 10
  6. Occurrence 6: structural-rules.tex, line 47, column 10
  7. Occurrence 7: derivations.tex, line 83, column 7
  8. Occurrence 8: soundness.tex, line 88, column 14
  9. Occurrence 9: soundness.tex, line 108, column 12
  10. Occurrence 10: soundness.tex, line 165, column 12
  11. Occurrence 11: soundness.tex, line 273, column 12
  12. Occurrence 12: soundness.tex, line 293, column 12
  13. Occurrence 13: soundness.tex, line 302, column 54
  14. Occurrence 14: soundness.tex, line 312, column 12

Expression 154

Ξ=Δ,A∨B\Xi = \Delta, !A \lor !B

Conventional reading: capital Xi equals first capital Delta, then the disjunction of formula A and formula B

Meaning here: The identity read 'capital Xi equals first capital Delta, then the disjunction of formula A and formula B' identifies capital Xi, the succedent sequence of the soundness proof's end-sequent, with first capital Delta, then the disjunction of formula A and formula B.

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

Expression 155

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

Conventional reading: the union of Gamma and the set containing the negation of formula A

Meaning here: The premise-set union is read 'the union of Gamma and the set containing the negation of formula A' and forms the set containing every member of either named set.

4 occurrences
  1. Occurrence 1: provability-consistency.tex, line 47, column 25
  2. Occurrence 2: provability-consistency.tex, line 54, column 24
  3. Occurrence 3: provability-consistency.tex, line 56, column 4
  4. Occurrence 4: provability-consistency.tex, line 101, column 31

Expression 156

Γ⊢A\Gamma \Proves {!A}

Conventional reading: Gamma syntactically derives formula A

Meaning here: In the current L K sequent calculus, 'Gamma syntactically derives formula A' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 157

A∨B,Γ⇒Δ!A \lor !B, \Gamma \fCenter \Delta

Conventional reading: antecedent containing first the disjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first the disjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: propositional-rules.tex, line 57, column 11

Expression 158

A∈Δ!A \in \Delta

Conventional reading: formula A is a member of capital Delta

Meaning here: The membership statement is read 'formula A is a member of capital Delta'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

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

Expression 159

Γ0,¬A⇒\Gamma_0, \lnot !A \fCenter

Conventional reading: antecedent containing first Gamma sub zero, then the negation of formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first Gamma sub zero, then the negation of formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 94, column 15

Expression 160

Γ1,A⇒\Gamma_1, !A \Sequent \quad

Conventional reading: antecedent containing first Gamma sub one, then formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first Gamma sub one, then formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 161

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Conventional reading: Gamma sub zero is a subset of Gamma

Meaning here: The finite-premise-set inclusion is read 'Gamma sub zero is a subset of Gamma' and states that every member of the set on the left belongs to the set on the right.

15 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 39, column 15
  2. Occurrence 2: proof-theoretic-notions.tex, line 71, column 15
  3. Occurrence 3: proof-theoretic-notions.tex, line 73, column 41
  4. Occurrence 4: proof-theoretic-notions.tex, line 95, column 54
  5. Occurrence 5: proof-theoretic-notions.tex, line 109, column 43
  6. Occurrence 6: proof-theoretic-notions.tex, line 150, column 62
  7. Occurrence 7: proof-theoretic-notions.tex, line 160, column 7
  8. Occurrence 8: proof-theoretic-notions.tex, line 164, column 14
  9. Occurrence 9: provability-consistency.tex, line 41, column 7
  10. Occurrence 10: provability-consistency.tex, line 96, column 35
  11. Occurrence 11: provability-consistency.tex, line 106, column 23
  12. Occurrence 12: provability-consistency.tex, line 122, column 7
  13. Occurrence 13: soundness.tex, line 357, column 52
  14. Occurrence 14: soundness.tex, line 373, column 24
  15. Occurrence 15: soundness.tex, line 378, column 51

Expression 162

¬A∨B⇒A→B\lnot !A \lor !B \Sequent !A \lif !B

Conventional reading: antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 163

B,¬A,¬B⇒!B, \lnot !A, \lnot !B \fCenter

Conventional reading: antecedent containing first formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 164

⇒¬(A∨B)→(¬A∧¬B)\Sequent \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conjunction of the negation of formula A and the negation of formula B, close parenthesis

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is open parenthesis, the conjunction of the negation of formula A and the negation of formula B, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 165

B⇒A→B!B \Sequent !A \lif !B

Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 167

Γ0,Γ1⇒\Gamma_0, \Gamma_1 \fCenter

Conventional reading: antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 120, column 11

Expression 168

Γ⊨A\Gamma \Entails !A

Conventional reading: Gamma semantically entails formula A

Meaning here: The statement 'Gamma semantically entails formula A' says that every propositional valuation satisfying all indicated premises also satisfies the conclusion.

1 occurrence
  1. Occurrence 1: soundness.tex, line 353, column 29

Expression 169

¬A,A⇒\lnot !A, !A \fCenter

Conventional reading: antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 193, column 10
  2. Occurrence 2: provability-consistency.tex, line 90, column 14
  3. Occurrence 3: provability-propositional.tex, line 72, column 16
  4. Occurrence 4: provability-propositional.tex, line 121, column 18

Expression 170

¬A∈Θ\lnot !A \in \Theta

Conventional reading: the negation of formula A is a member of capital Theta

Meaning here: The membership statement is read 'the negation of formula A is a member of capital Theta'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 127, column 55

Expression 171

Γ=⟨A1,…,Am⟩\Gamma = \tuple{!A_1, \dots, !A_m}

Conventional reading: Gamma equals the finite sequence first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub m

Meaning here: The identity read 'Gamma equals the finite sequence first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub m' defines Gamma to be the finite sequence first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub m, an ordered finite sequence.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 31, column 30

Expression 173

v⊭A→B\pSat/{v}{!A \lif !B}

Conventional reading: valuation v does not satisfy the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The valuation claim 'valuation v does not satisfy the conditional whose antecedent is formula A; and whose consequent is formula B' states exactly whether the named propositional valuation makes the formula true.

2 occurrences
  1. Occurrence 1: soundness.tex, line 322, column 3
  2. Occurrence 2: soundness.tex, line 329, column 3

Expression 174

(A∨B)→C⇒A→C(!A \lor !B) \lif !C \Sequent !A \lif !C

Conventional reading: antecedent containing the conditional whose antecedent is open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is formula C; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula C

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is formula C; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 175

A,¬A,¬B⇒!A, \lnot !A, \lnot !B \fCenter

Conventional reading: antecedent containing first formula A, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 176

v⊭C\pSat/{v}{!C}

Conventional reading: valuation v does not satisfy formula C

Meaning here: The valuation claim 'valuation v does not satisfy formula C' states exactly whether the named propositional valuation makes the formula true.

14 occurrences
  1. Occurrence 1: soundness.tex, line 94, column 3
  2. Occurrence 2: soundness.tex, line 97, column 6
  3. Occurrence 3: soundness.tex, line 99, column 3
  4. Occurrence 4: soundness.tex, line 117, column 3
  5. Occurrence 5: soundness.tex, line 123, column 3
  6. Occurrence 6: soundness.tex, line 129, column 3
  7. Occurrence 7: soundness.tex, line 146, column 3
  8. Occurrence 8: soundness.tex, line 150, column 3
  9. Occurrence 9: soundness.tex, line 151, column 25
  10. Occurrence 10: soundness.tex, line 173, column 3
  11. Occurrence 11: soundness.tex, line 177, column 3
  12. Occurrence 12: soundness.tex, line 197, column 3
  13. Occurrence 13: soundness.tex, line 202, column 12
  14. Occurrence 14: soundness.tex, line 378, column 1

Expression 177

Γ,A\Gamma, !A

Conventional reading: first Gamma, then formula A

Meaning here: The ordered finite formula sequence is read 'first Gamma, then formula A'; the source uses that order in its sequent or inconsistency argument.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 46, column 54

Expression 178

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

Conventional reading: first formula A, then formula B syntactically derives the conjunction of formula A and formula B

Meaning here: In the current L K sequent calculus, 'first formula A, then formula B syntactically derives the conjunction of formula A and formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 180

v⊨A→B\pSat{v}{!A \lif !B}

Conventional reading: valuation v satisfies the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The valuation claim 'valuation v satisfies the conditional whose antecedent is formula A; and whose consequent is formula B' states exactly whether the named propositional valuation makes the formula true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 199, column 25

Expression 181

Γ⇒\Gamma \Sequent \quad

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 41, column 35

Expression 182

C∈Δ!C \in \Delta

Conventional reading: formula C is a member of capital Delta

Meaning here: The membership statement is read 'formula C is a member of capital Delta'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

10 occurrences
  1. Occurrence 1: soundness.tex, line 94, column 59
  2. Occurrence 2: soundness.tex, line 100, column 63
  3. Occurrence 3: soundness.tex, line 117, column 59
  4. Occurrence 4: soundness.tex, line 124, column 32
  5. Occurrence 5: soundness.tex, line 147, column 53
  6. Occurrence 6: soundness.tex, line 152, column 50
  7. Occurrence 7: soundness.tex, line 174, column 53
  8. Occurrence 8: soundness.tex, line 177, column 66
  9. Occurrence 9: soundness.tex, line 198, column 53
  10. Occurrence 10: soundness.tex, line 203, column 8

Expression 183

Γ⇒Δ,A,A\Gamma \fCenter \Delta, !A, !A

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, and finally formula A

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, and finally formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 45, column 7

Expression 184

¬A,Γ⇒Δ\lnot !A, \Gamma \Sequent \Delta

Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 185

A⇒A!A \Sequent !A

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

5 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 56, column 11
  2. Occurrence 2: proving-things.tex, line 37, column 64
  3. Occurrence 3: proving-things.tex, line 38, column 48
  4. Occurrence 4: proof-theoretic-notions.tex, line 84, column 21
  5. Occurrence 5: soundness.tex, line 62, column 40

Expression 186

Π⇒Λ\Pi \Sequent \Lambda

Conventional reading: antecedent containing capital Pi; sequent arrow; succedent containing capital Lambda

Meaning here: The sequent read 'antecedent containing capital Pi; sequent arrow; succedent containing capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 325, column 15

Expression 187

A⇒¬¬A!A \Sequent \lnot\lnot !A

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the negation of the negation of formula A

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing the negation of the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 189

B∈Γ0!B \in \Gamma_0

Conventional reading: formula B is a member of Gamma sub zero

Meaning here: The membership statement is read 'formula B is a member of Gamma sub zero'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 361, column 19

Expression 191

(A1∧⋯∧Am)→(B1∨⋯∨Bn)(!A_1 \land \cdots \land !A_m) \lif (!B_1 \lor \cdots \lor !B_n)

Conventional reading: the conditional whose antecedent is open parenthesis, the iterated conjunction from formula A sub one through formula A sub m, close parenthesis; and whose consequent is open parenthesis, the iterated disjunction from formula B sub one through formula B sub n, close parenthesis

Meaning here: The propositional formula is read 'the conditional whose antecedent is open parenthesis, the iterated conjunction from formula A sub one through formula A sub m, close parenthesis; and whose consequent is open parenthesis, the iterated disjunction from formula B sub one through formula B sub n, close parenthesis'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 34, column 1

Expression 193

Γ0⇒¬A\Gamma_0 \fCenter \lnot !A

Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing the negation of formula A

Meaning here: The sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 115, column 10

Expression 194

B⇒A∨B!B \fCenter !A \lor !B

Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 195

{A}⊆Γ\{!A\} \subseteq \Gamma

Conventional reading: the set containing formula A is a subset of Gamma

Meaning here: The finite-premise-set inclusion is read 'the set containing formula A is a subset of Gamma' and states that every member of the set on the left belongs to the set on the right.

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

Expression 196

⊬A\Proves/ !A

Conventional reading: formula A is not derivable with no premises

Meaning here: In the current L K sequent calculus, 'formula A is not derivable with no premises' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 197

¬A\lnot !A

Conventional reading: the negation of formula A

Meaning here: The propositional formula is read 'the negation of formula A'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

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

Expression 198

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

5 occurrences
  1. Occurrence 1: soundness.tex, line 77, column 26
  2. Occurrence 2: soundness.tex, line 104, column 21
  3. Occurrence 3: soundness.tex, line 114, column 42
  4. Occurrence 4: soundness.tex, line 171, column 9
  5. Occurrence 5: soundness.tex, line 325, column 46

Expression 200

B,A⇒B!B, !A \fCenter !B

Conventional reading: antecedent containing first formula B, then formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first formula B, then formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 83, column 10
  2. Occurrence 2: proving-things.tex, line 101, column 10
  3. Occurrence 3: proving-things.tex, line 122, column 10
  4. Occurrence 4: proving-things.tex, line 144, column 10

Expression 201

¬A,A⇒B\lnot !A, !A \fCenter !B

Conventional reading: antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 81, column 10
  2. Occurrence 2: proving-things.tex, line 96, column 10
  3. Occurrence 3: proving-things.tex, line 117, column 10
  4. Occurrence 4: proving-things.tex, line 139, column 10

Expression 202

Θ=Γ\Theta = \Gamma

Conventional reading: capital Theta equals Gamma

Meaning here: The identity read 'capital Theta equals Gamma' identifies capital Theta, the antecedent sequence of the soundness proof's end-sequent, with Gamma.

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

Expression 203

Γ,Π⇒Δ,Λ\Gamma, \Pi \fCenter \Delta, \Lambda

Conventional reading: antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda

Meaning here: The sequent read 'antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 277, column 15

Expression 204

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

Conventional reading: the negation of formula A syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: In the current L K sequent calculus, 'the negation of formula A syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 205

Γ⊢A\Gamma \Proves !A

Conventional reading: Gamma syntactically derives formula A

Meaning here: In the current L K sequent calculus, 'Gamma syntactically derives formula A' states derivability from the indicated premise set according to this chapter's sequent rules.

16 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 38, column 25
  2. Occurrence 2: proof-theoretic-notions.tex, line 80, column 26
  3. Occurrence 3: proof-theoretic-notions.tex, line 90, column 34
  4. Occurrence 4: proof-theoretic-notions.tex, line 95, column 9
  5. Occurrence 5: proof-theoretic-notions.tex, line 104, column 4
  6. Occurrence 6: proof-theoretic-notions.tex, line 109, column 4
  7. Occurrence 7: proof-theoretic-notions.tex, line 128, column 44
  8. Occurrence 8: proof-theoretic-notions.tex, line 150, column 12
  9. Occurrence 9: proof-theoretic-notions.tex, line 159, column 14
  10. Occurrence 10: provability-consistency.tex, line 20, column 6
  11. Occurrence 11: provability-consistency.tex, line 47, column 1
  12. Occurrence 12: provability-consistency.tex, line 51, column 15
  13. Occurrence 13: provability-consistency.tex, line 76, column 6
  14. Occurrence 14: provability-consistency.tex, line 81, column 11
  15. Occurrence 15: soundness.tex, line 353, column 4
  16. Occurrence 16: soundness.tex, line 357, column 4

Expression 206

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

Conventional reading: antecedent containing first the disjunction of formula A and formula B, then the negation of formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing first the disjunction of formula A and formula B, then the negation of formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 208

A∨¬A!A \lor \lnot !A

Conventional reading: the disjunction of formula A and the negation of formula A

Meaning here: The propositional formula is read 'the disjunction of formula A and the negation of formula A'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

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

Expression 209

¬A,Γ1⇒\lnot !A, \Gamma_1 \Sequent \quad

Conventional reading: antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 210

RContraction\RightR{\Contraction}

Conventional reading: right contraction rule

Meaning here: The label 'right contraction rule' names the side of the sequent and the connective or structural operation governed by this inference rule.

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

Expression 211

A→C⇒¬(A∧¬C)!A \lif !C \Sequent \lnot (!A \land \lnot !C)

Conventional reading: antecedent containing the conditional whose antecedent is formula A; and whose consequent is formula C; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and the negation of formula C, close parenthesis

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is formula A; and whose consequent is formula C; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and the negation of formula C, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 212

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

Conventional reading: the conjunction of formula A and formula B syntactically derives formula A

Meaning here: In the current L K sequent calculus, 'the conjunction of formula A and formula B syntactically derives formula A' states derivability from the indicated premise set according to this chapter's sequent rules.

2 occurrences
  1. Occurrence 1: provability-propositional.tex, line 21, column 57
  2. Occurrence 2: provability-propositional.tex, line 28, column 51

Expression 213

B⇒A→B!B \fCenter !A \lif !B

Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 214

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

Conventional reading: antecedent containing the conjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is formula C

Meaning here: The sequent read 'antecedent containing the conjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the disjunction of formula A and formula B, close parenthesis; and whose consequent is formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 215

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

Conventional reading: antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: propositional-rules.tex, line 35, column 10
  2. Occurrence 2: propositional-rules.tex, line 40, column 10
  3. Occurrence 3: soundness.tex, line 139, column 14

Expression 216

Γ0\Gamma_0

Conventional reading: Gamma sub zero

Meaning here: Gamma sub zero denotes a finite premise set; when the source writes it as a sequent antecedent, the source tacitly chooses a sequence containing its members.

7 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 40, column 25
  2. Occurrence 2: proof-theoretic-notions.tex, line 52, column 4
  3. Occurrence 3: proof-theoretic-notions.tex, line 64, column 31
  4. Occurrence 4: proof-theoretic-notions.tex, line 66, column 46
  5. Occurrence 5: proof-theoretic-notions.tex, line 97, column 54
  6. Occurrence 6: proof-theoretic-notions.tex, line 165, column 55
  7. Occurrence 7: provability-consistency.tex, line 25, column 18

Expression 218

B!B

Conventional reading: formula B

Meaning here: The metavariable B denotes an arbitrary formula.

11 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 69, column 56
  2. Occurrence 2: derivations.tex, line 73, column 10
  3. Occurrence 3: derivations.tex, line 90, column 47
  4. Occurrence 4: derivations.tex, line 106, column 19
  5. Occurrence 5: proving-things.tex, line 180, column 21
  6. Occurrence 6: soundness.tex, line 133, column 59
  7. Occurrence 7: soundness.tex, line 158, column 30
  8. Occurrence 8: soundness.tex, line 159, column 6
  9. Occurrence 9: soundness.tex, line 161, column 59
  10. Occurrence 10: soundness.tex, line 183, column 17
  11. Occurrence 11: soundness.tex, line 183, column 60

Expression 219

⇒¬A\fCenter \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 220

⇒A,A∨¬A\fCenter !A, !A \lor \lnot !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the disjunction of formula A and the negation of formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the disjunction of formula A and the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 221

 C∈Γ~!C \in \Gamma

Conventional reading: formula C is a member of Gamma

Meaning here: The membership statement is read 'formula C is a member of Gamma'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 197, column 51

Expression 222

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

Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: soundness.tex, line 76, column 13
  2. Occurrence 2: soundness.tex, line 144, column 3

Expression 225

¬B,B⇒\lnot !B, !B \fCenter

Conventional reading: antecedent containing first the negation of formula B, then formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula B, then formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 226

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

Conventional reading: formula A syntactically derives the disjunction of formula A and formula B

Meaning here: In the current L K sequent calculus, 'formula A syntactically derives the disjunction of formula A and formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 227

⇒(¬A∧¬B)→¬(A∨B)\Sequent (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conjunction of the negation of formula A and the negation of formula B, close parenthesis; and whose consequent is the negation of open parenthesis, the disjunction of formula A and formula B, close parenthesis

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conjunction of the negation of formula A and the negation of formula B, close parenthesis; and whose consequent is the negation of open parenthesis, the disjunction of formula A and formula B, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 228

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 229

A→B,A⇒B!A \lif !B, !A \fCenter !B

Conventional reading: antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 230

A∧B⇒B!A \land !B \Sequent !B

Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 231

B1∨…∨Bn!B_1 \lor \dots \lor !B_n

Conventional reading: the iterated disjunction from formula B sub one through formula B sub n

Meaning here: The propositional formula is read 'the iterated disjunction from formula B sub one through formula B sub n'; the spoken grouping preserves every conditional, disjunction, conjunction, and negation scope.

1 occurrence
  1. Occurrence 1: rules-and-proofs.tex, line 40, column 28

Expression 233

A⇒!A \fCenter

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 235

Γ⇒Δ\Gamma \Sequent \Delta

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

8 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 20, column 1
  2. Occurrence 2: rules-and-proofs.tex, line 32, column 44
  3. Occurrence 3: soundness.tex, line 44, column 1
  4. Occurrence 4: soundness.tex, line 90, column 28
  5. Occurrence 5: soundness.tex, line 157, column 14
  6. Occurrence 6: soundness.tex, line 285, column 28
  7. Occurrence 7: soundness.tex, line 301, column 54
  8. Occurrence 8: soundness.tex, line 324, column 55

Expression 236

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

Conventional reading: antecedent containing first the disjunction of the negation of formula A and the negation of formula B, then formula A; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the disjunction of the negation of formula A and the negation of formula B, then formula A; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 237

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

Conventional reading: antecedent containing the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula C; sequent arrow; succedent containing the disjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis

Meaning here: The sequent read 'antecedent containing the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula B, close parenthesis; and whose consequent is formula C; sequent arrow; succedent containing the disjunction of open parenthesis, the conditional whose antecedent is formula A; and whose consequent is formula C, close parenthesis and open parenthesis, the conditional whose antecedent is formula B; and whose consequent is formula C, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 238

B⇒B!B \fCenter !B

Conventional reading: antecedent containing formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

10 occurrences
  1. Occurrence 1: proving-things.tex, line 97, column 7
  2. Occurrence 2: proving-things.tex, line 118, column 7
  3. Occurrence 3: proving-things.tex, line 140, column 7
  4. Occurrence 4: proving-things.tex, line 235, column 7
  5. Occurrence 5: provability-propositional.tex, line 44, column 13
  6. Occurrence 6: provability-propositional.tex, line 51, column 13
  7. Occurrence 7: provability-propositional.tex, line 75, column 13
  8. Occurrence 8: provability-propositional.tex, line 92, column 13
  9. Occurrence 9: provability-propositional.tex, line 112, column 15
  10. Occurrence 10: provability-propositional.tex, line 129, column 15

Expression 239

A,Γ1⇒!A, \Gamma_1 \fCenter

Conventional reading: antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

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

Expression 240

⇒¬¬A→A\Sequent \lnot \lnot !A \lif !A

Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of the negation of formula A; and whose consequent is formula A

Meaning here: The sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of the negation of formula A; and whose consequent is formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 241

Γ1⊆Γ\Gamma_1 \subseteq \Gamma

Conventional reading: Gamma sub one is a subset of Gamma

Meaning here: The finite-premise-set inclusion is read 'Gamma sub one is a subset of Gamma' and states that every member of the set on the left belongs to the set on the right.

4 occurrences
  1. Occurrence 1: provability-consistency.tex, line 25, column 33
  2. Occurrence 2: provability-consistency.tex, line 41, column 39
  3. Occurrence 3: provability-consistency.tex, line 106, column 55
  4. Occurrence 4: provability-consistency.tex, line 122, column 39

Expression 242

A,A,Γ⇒Δ!A, !A, \Gamma \fCenter \Delta

Conventional reading: antecedent containing first formula A, then formula A, and finally Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first formula A, then formula A, and finally Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 40, column 7

Expression 243

C,D!C, !D

Conventional reading: first formula C, then formula D

Meaning here: The ordered finite formula sequence is read 'first formula C, then formula D'; the source uses that order in its sequent or inconsistency argument.

1 occurrence
  1. Occurrence 1: derivations.tex, line 90, column 1

Expression 244

Δ0⊆Δ\Delta_0 \subseteq \Delta

Conventional reading: capital Delta sub zero is a subset of capital Delta

Meaning here: The finite-premise-set inclusion is read 'capital Delta sub zero is a subset of capital Delta' and states that every member of the set on the left belongs to the set on the right.

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

Expression 245

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

Conventional reading: antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 246

A∧B⇒A!A \land !B \fCenter !A

Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 231, column 10
  2. Occurrence 2: provability-propositional.tex, line 42, column 16

Expression 247

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

Conventional reading: antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 248

¬A,Γ⇒\lnot !A, \Gamma \fCenter

Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 65, column 10

Expression 249

Γ⇒Δ,B,A,Λ\Gamma \fCenter \Delta, !B, !A, \Lambda

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B, then formula A, and finally capital Lambda

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B, then formula A, and finally capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 61, column 10

Expression 250

A⇒A!A \fCenter !A

Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

12 occurrences
  1. Occurrence 1: proving-things.tex, line 42, column 7
  2. Occurrence 2: proving-things.tex, line 133, column 7
  3. Occurrence 3: proving-things.tex, line 191, column 7
  4. Occurrence 4: proving-things.tex, line 286, column 7
  5. Occurrence 5: provability-consistency.tex, line 60, column 9
  6. Occurrence 6: provability-consistency.tex, line 88, column 11
  7. Occurrence 7: provability-propositional.tex, line 40, column 13
  8. Occurrence 8: provability-propositional.tex, line 50, column 13
  9. Occurrence 9: provability-propositional.tex, line 70, column 13
  10. Occurrence 10: provability-propositional.tex, line 88, column 13
  11. Occurrence 11: provability-propositional.tex, line 111, column 15
  12. Occurrence 12: provability-propositional.tex, line 119, column 15

Expression 251

C∈Θ!C \in \Theta

Conventional reading: formula C is a member of capital Theta

Meaning here: The membership statement is read 'formula C is a member of capital Theta'; each exact occurrence record identifies its target as either a premise set or an antecedent or succedent sequence.

6 occurrences
  1. Occurrence 1: soundness.tex, line 98, column 8
  2. Occurrence 2: soundness.tex, line 99, column 51
  3. Occurrence 3: soundness.tex, line 123, column 47
  4. Occurrence 4: soundness.tex, line 128, column 21
  5. Occurrence 5: soundness.tex, line 149, column 12
  6. Occurrence 6: soundness.tex, line 152, column 3

Expression 253

B,Π⇒Λ!B, \Pi \Sequent \Lambda

Conventional reading: antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda

Meaning here: The sequent read 'antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 254

Θ=¬A,Γ\Theta = \lnot !A, \Gamma

Conventional reading: capital Theta equals first the negation of formula A, then Gamma

Meaning here: The identity read 'capital Theta equals first the negation of formula A, then Gamma' identifies capital Theta, the antecedent sequence of the soundness proof's end-sequent, with first the negation of formula A, then Gamma.

1 occurrence
  1. Occurrence 1: soundness.tex, line 112, column 7

Expression 255

Π∖Λ\Pi \setminus \Lambda

Conventional reading: capital Pi set difference capital Lambda

Meaning here: The source prints 'capital Pi set difference capital Lambda'. This set-difference expression is preserved literally; the linked source disclosure notes that a sequent appears intended in the proof.

1 occurrence
  1. Occurrence 1: soundness.tex, line 288, column 28

Expression 256

A→B,A⇒B!A \lif !B, !A \Sequent !B

Conventional reading: antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 257

¬A∨B⇒A→B\lnot !A \lor !B \fCenter !A \lif !B

Conventional reading: antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

6 occurrences
  1. Occurrence 1: proving-things.tex, line 57, column 10
  2. Occurrence 2: proving-things.tex, line 73, column 37
  3. Occurrence 3: proving-things.tex, line 89, column 10
  4. Occurrence 4: proving-things.tex, line 107, column 10
  5. Occurrence 5: proving-things.tex, line 128, column 10
  6. Occurrence 6: proving-things.tex, line 150, column 10

Expression 258

A∨(B∨C)⇒(A∨B)∨C!A \lor (!B \lor !C) \Sequent (!A \lor !B) \lor !C

Conventional reading: antecedent containing the disjunction of formula A and open parenthesis, the disjunction of formula B and formula C, close parenthesis; sequent arrow; succedent containing the disjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and formula C

Meaning here: The sequent read 'antecedent containing the disjunction of formula A and open parenthesis, the disjunction of formula B and formula C, close parenthesis; sequent arrow; succedent containing the disjunction of open parenthesis, the disjunction of formula A and formula B, close parenthesis and formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 260

A→B,¬A→B⇒B!A \lif !B, \lnot !A \lif !B \Sequent !B

Conventional reading: antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then the conditional whose antecedent is the negation of formula A; and whose consequent is formula B; sequent arrow; succedent containing formula B

Meaning here: The sequent read 'antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then the conditional whose antecedent is the negation of formula A; and whose consequent is formula B; sequent arrow; succedent containing formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 262

Δ\Delta

Conventional reading: capital Delta

Meaning here: Capital Delta is context-sensitive: it denotes a sequent succedent sequence or a premise set, as stated by every exact occurrence record.

9 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 23, column 20
  2. Occurrence 2: rules-and-proofs.tex, line 25, column 26
  3. Occurrence 3: rules-and-proofs.tex, line 39, column 1
  4. Occurrence 4: rules-and-proofs.tex, line 41, column 1
  5. Occurrence 5: rules-and-proofs.tex, line 49, column 18
  6. Occurrence 6: derivations.tex, line 49, column 14
  7. Occurrence 7: derivations.tex, line 72, column 37
  8. Occurrence 8: derivations.tex, line 90, column 11
  9. Occurrence 9: proof-theoretic-notions.tex, line 98, column 25

Expression 263

π\pi

Conventional reading: pi

Meaning here: Pi denotes the sequent-calculus derivation currently under discussion.

11 occurrences
  1. Occurrence 1: provability-consistency.tex, line 82, column 22
  2. Occurrence 2: provability-consistency.tex, line 86, column 17
  3. Occurrence 3: soundness.tex, line 58, column 5
  4. Occurrence 4: soundness.tex, line 59, column 46
  5. Occurrence 5: soundness.tex, line 61, column 42
  6. Occurrence 6: soundness.tex, line 134, column 53
  7. Occurrence 7: soundness.tex, line 162, column 50
  8. Occurrence 8: soundness.tex, line 184, column 49
  9. Occurrence 9: soundness.tex, line 270, column 41
  10. Occurrence 10: soundness.tex, line 290, column 51
  11. Occurrence 11: soundness.tex, line 309, column 49

Expression 264

Γ⇒Δ,¬A\Gamma \fCenter \Delta, \lnot !A

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the negation of formula A

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the negation of formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: propositional-rules.tex, line 25, column 10

Expression 265

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

Conventional reading: antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: soundness.tex, line 155, column 34

Expression 266

v⊨A∨B\pSat{v}{!A \lor !B}

Conventional reading: valuation v satisfies the disjunction of formula A and formula B

Meaning here: The valuation claim 'valuation v satisfies the disjunction of formula A and formula B' states exactly whether the named propositional valuation makes the formula true.

1 occurrence
  1. Occurrence 1: soundness.tex, line 175, column 16

Expression 267

C,D⇒C!C, !D \fCenter !C

Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula C

Meaning here: The sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

3 occurrences
  1. Occurrence 1: derivations.tex, line 64, column 10
  2. Occurrence 2: derivations.tex, line 98, column 10
  3. Occurrence 3: derivations.tex, line 115, column 10

Expression 268

D,C⇒C!D, !C \Sequent !C

Conventional reading: antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C

Meaning here: The sequent read 'antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: derivations.tex, line 50, column 1

Expression 269

Γ⇒Δ,A,B,Λ\Gamma \fCenter \Delta, !A, !B, \Lambda

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, then formula B, and finally capital Lambda

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, then formula B, and finally capital Lambda' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

1 occurrence
  1. Occurrence 1: structural-rules.tex, line 59, column 7

Expression 270

¬A∨¬B⇒¬(A∧B)\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)

Conventional reading: antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis

Meaning here: The sequent read 'antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

6 occurrences
  1. Occurrence 1: proving-things.tex, line 162, column 10
  2. Occurrence 2: proving-things.tex, line 173, column 10
  3. Occurrence 3: proving-things.tex, line 187, column 10
  4. Occurrence 4: proving-things.tex, line 206, column 10
  5. Occurrence 5: proving-things.tex, line 225, column 10
  6. Occurrence 6: proving-things.tex, line 246, column 10

Expression 271

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

Conventional reading: the conjunction of formula A and formula B syntactically derives formula B

Meaning here: In the current L K sequent calculus, 'the conjunction of formula A and formula B syntactically derives formula B' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 272

Γ⊬A\Gamma \Proves/ !A

Conventional reading: Gamma does not syntactically derive formula A

Meaning here: In the current L K sequent calculus, 'Gamma does not syntactically derive formula A' states derivability from the indicated premise set according to this chapter's sequent rules.

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

Expression 273

B,C⇒A!B, !C \fCenter !A

Conventional reading: antecedent containing first formula B, then formula C; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing first formula B, then formula C; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

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

Expression 275

Γ0⇒A\Gamma_0 \Sequent !A

Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A

Meaning here: The sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A' names its complete ordered antecedent and succedent; an empty side is spoken explicitly. An unprimed Gamma or capital Delta sub zero or sub one in antecedent position denotes the corresponding finite premise set represented by a sequence of its members, with needed structural steps tacit.

9 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 65, column 20
  2. Occurrence 2: proof-theoretic-notions.tex, line 96, column 29
  3. Occurrence 3: proof-theoretic-notions.tex, line 98, column 57
  4. Occurrence 4: proof-theoretic-notions.tex, line 110, column 32
  5. Occurrence 5: proof-theoretic-notions.tex, line 160, column 57
  6. Occurrence 6: provability-consistency.tex, line 26, column 24
  7. Occurrence 7: provability-consistency.tex, line 27, column 56
  8. Occurrence 8: provability-consistency.tex, line 82, column 41
  9. Occurrence 9: soundness.tex, line 358, column 38

Expression 276

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

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 84, column 10
  2. Occurrence 2: soundness.tex, line 189, column 14

Expression 277

B,Γ⇒Δ!B, \Gamma \fCenter \Delta

Conventional reading: antecedent containing first formula B, then Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing first formula B, then Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: propositional-rules.tex, line 38, column 7
  2. Occurrence 2: propositional-rules.tex, line 55, column 7

Expression 278

Γ⇒Δ\Gamma \fCenter \Delta

Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing capital Delta

Meaning here: The sequent read 'antecedent containing Gamma; sequent arrow; succedent containing capital Delta' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

5 occurrences
  1. Occurrence 1: structural-rules.tex, line 26, column 7
  2. Occurrence 2: structural-rules.tex, line 31, column 7
  3. Occurrence 3: derivations.tex, line 42, column 7
  4. Occurrence 4: soundness.tex, line 81, column 12
  5. Occurrence 5: soundness.tex, line 86, column 12

Expression 279

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

Conventional reading: antecedent containing first formula A, then the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing no formulas

Meaning here: The sequent read 'antecedent containing first formula A, then the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing no formulas' names its complete ordered antecedent and succedent; an empty side is spoken explicitly.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 183, column 10
  2. Occurrence 2: proving-things.tex, line 202, column 10

112 formal objects

  1. Definition: Sequent — line 18 — rules-and-proofs.tex, line 18.
  2. Definition: Initial Sequent — line 52 — rules-and-proofs.tex, line 52.
  3. Definition of negation sequent rules — line 17 — propositional-rules.tex, line 17.
  4. Proof tree concluding antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 21 — propositional-rules.tex, line 21.
  5. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the negation of formula A — line 26 — propositional-rules.tex, line 26.
  6. Definition of conjunction sequent rules — line 31 — propositional-rules.tex, line 31.
  7. Rule table for conjunction — line 32 — propositional-rules.tex, line 32.
  8. Proof tree concluding antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 36 — propositional-rules.tex, line 36.
  9. Proof tree concluding antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 41 — propositional-rules.tex, line 41.
  10. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B — line 48 — propositional-rules.tex, line 48.
  11. Definition of disjunction sequent rules — line 53 — propositional-rules.tex, line 53.
  12. Proof tree concluding antecedent containing first the disjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 58 — propositional-rules.tex, line 58.
  13. Rule table for disjunction — line 60 — propositional-rules.tex, line 60.
  14. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B — line 64 — propositional-rules.tex, line 64.
  15. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B — line 69 — propositional-rules.tex, line 69.
  16. Definition of conditional sequent rules — line 75 — propositional-rules.tex, line 75.
  17. Proof tree concluding antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then Gamma, and finally capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda — line 80 — propositional-rules.tex, line 80.
  18. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B — line 85 — propositional-rules.tex, line 85.
  19. Definition of Weakening sequent rules — line 25 — structural-rules.tex, line 25.
  20. Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 29 — structural-rules.tex, line 29.
  21. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A — line 34 — structural-rules.tex, line 34.
  22. Definition of Contraction sequent rules — line 39 — structural-rules.tex, line 39.
  23. Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 43 — structural-rules.tex, line 43.
  24. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A — line 48 — structural-rules.tex, line 48.
  25. Definition of Exchange sequent rules — line 53 — structural-rules.tex, line 53.
  26. Proof tree concluding antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta — line 57 — structural-rules.tex, line 57.
  27. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B, then formula A, and finally capital Lambda — line 62 — structural-rules.tex, line 62.
  28. Definition of Exchange sequent rules — line 70 — structural-rules.tex, line 70.
  29. Proof tree concluding antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda — line 76 — structural-rules.tex, line 76.
  30. Definition: L K derivation — line 23 — derivations.tex, line 23.
  31. Example: Every initial sequent, e.g., antecedent containing formula C; sequent arrow; succedent… — line 37 — derivations.tex, line 37.
  32. Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 41 — derivations.tex, line 41.
  33. Proof tree concluding antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C — line 51 — derivations.tex, line 51.
  34. Proof tree concluding antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula C — line 59 — derivations.tex, line 59.
  35. Proof tree concluding antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta, followed by a printed trailing comma with no following formula — line 67 — derivations.tex, line 67.
  36. Proof tree concluding antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula D — line 75 — derivations.tex, line 75.
  37. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B — line 82 — derivations.tex, line 82.
  38. Proof tree concluding antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D — line 93 — derivations.tex, line 93.
  39. Proof tree concluding antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula D and formula C — line 107 — derivations.tex, line 107.
  40. Example: Give an L K derivation for the sequent antecedent containing the conjunction of formula A and… — line 15 — proving-things.tex, line 15.
  41. Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 20 — proving-things.tex, line 20.
  42. Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 31 — proving-things.tex, line 31.
  43. Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 41 — proving-things.tex, line 41.
  44. Example: Give an L K derivation for the sequent antecedent containing the disjunction of the negation of… — line 50 — proving-things.tex, line 50.
  45. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 55 — proving-things.tex, line 55.
  46. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 70 — proving-things.tex, line 70.
  47. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 79 — proving-things.tex, line 79.
  48. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 94 — proving-things.tex, line 94.
  49. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 113 — proving-things.tex, line 113.
  50. Proof tree concluding antecedent containing the disjunction of the negation of formula A and formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 132 — proving-things.tex, line 132.
  51. Example: Give an L K derivation of the sequent antecedent containing the disjunction of the negation of… — line 154 — proving-things.tex, line 154.
  52. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 160 — proving-things.tex, line 160.
  53. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 169 — proving-things.tex, line 169.
  54. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 181 — proving-things.tex, line 181.
  55. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 190 — proving-things.tex, line 190.
  56. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 213 — proving-things.tex, line 213.
  57. Proof tree concluding antecedent containing the disjunction of the negation of formula A and the negation of formula B; sequent arrow; succedent containing the negation of open parenthesis, the conjunction of formula A and formula B, close parenthesis — line 228 — proving-things.tex, line 228.
  58. Example: So far we haven't used the contraction rule, but it is sometimes required — line 252 — proving-things.tex, line 252.
  59. Proof tree concluding antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A — line 257 — proving-things.tex, line 257.
  60. Proof tree concluding antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A — line 262 — proving-things.tex, line 262.
  61. Proof tree concluding antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A — line 275 — proving-things.tex, line 275.
  62. Proof tree concluding antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A — line 285 — proving-things.tex, line 285.
  63. Exercise: Give derivations of the following sequents: Next item: antecedent containing the conjunction of… — line 300 — proving-things.tex, line 300.
  64. Exercise: Give derivations of the following sequents: Next item: antecedent containing the conditional… — line 310 — proving-things.tex, line 310.
  65. Exercise: Give derivations of the following sequents: Next item: antecedent containing the negation of… — line 328 — proving-things.tex, line 328.
  66. Definition: Theorems — line 30 — proof-theoretic-notions.tex, line 30.
  67. Definition: derivability — line 36 — proof-theoretic-notions.tex, line 36.
  68. Proof tree concluding antecedent containing first formula C, then formula C, and finally formula B; sequent arrow; succedent containing formula A — line 54 — proof-theoretic-notions.tex, line 54.
  69. Definition: Consistency — line 69 — proof-theoretic-notions.tex, line 69.
  70. Proposition: Reflexivity — line 78 — proof-theoretic-notions.tex, line 78.
  71. Proposition: Monotonicity — line 88 — proof-theoretic-notions.tex, line 88.
  72. Proposition: Transitivity — line 102 — proof-theoretic-notions.tex, line 102.
  73. Proof tree concluding antecedent containing first Gamma sub zero, then capital Delta sub zero; sequent arrow; succedent containing formula B — line 114 — proof-theoretic-notions.tex, line 114.
  74. Proposition: Gamma is inconsistent if and only if Gamma syntactically derives formula A for every sentence… — line 133 — proof-theoretic-notions.tex, line 133.
  75. Exercise: Prove the proposition that Gamma is inconsistent if and only if Gamma syntactically derives… — line 143 — proof-theoretic-notions.tex, line 143.
  76. Proposition: Compactness — line 147 — proof-theoretic-notions.tex, line 147.
  77. Proposition: If Gamma syntactically derives formula A and the union of Gamma and the set containing formula… — line 19 — provability-consistency.tex, line 19.
  78. Proof tree concluding antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas — line 30 — provability-consistency.tex, line 30.
  79. Proposition: Gamma syntactically derives formula A if and only if the union of Gamma and the set containing… — line 45 — provability-consistency.tex, line 45.
  80. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing formula A — line 59 — provability-consistency.tex, line 59.
  81. Exercise: Prove that Gamma syntactically derives the negation of formula A if and only if the union of… — line 71 — provability-consistency.tex, line 71.
  82. Proposition: If Gamma syntactically derives formula A and the negation of formula A is a member of Gamma,… — line 75 — provability-consistency.tex, line 75.
  83. Proof tree concluding antecedent containing first Gamma sub zero, then the negation of formula A; sequent arrow; succedent containing no formulas — line 84 — provability-consistency.tex, line 84.
  84. Proposition: If the union of Gamma and the set containing formula A and the union of Gamma and the set… — line 100 — provability-consistency.tex, line 100.
  85. Proof tree concluding antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas — line 110 — provability-consistency.tex, line 110.
  86. Proposition: Next item: Both the conjunction of formula A and formula B syntactically derives formula A and… — line 26 — provability-propositional.tex, line 26.
  87. Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B — line 39 — provability-propositional.tex, line 39.
  88. Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 43 — provability-propositional.tex, line 43.
  89. Proof tree concluding antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B — line 49 — provability-propositional.tex, line 49.
  90. Proposition: Next item: first the disjunction of formula A and formula B, then the negation of formula A,… — line 58 — provability-propositional.tex, line 58.
  91. Proof tree concluding antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas — line 69 — provability-propositional.tex, line 69.
  92. Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B — line 87 — provability-propositional.tex, line 87.
  93. Proof tree concluding antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B — line 91 — provability-propositional.tex, line 91.
  94. Proposition: Next item: first formula A, then the conditional whose antecedent is formula A; and whose… — line 99 — provability-propositional.tex, line 99.
  95. Proof tree concluding antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B — line 110 — provability-propositional.tex, line 110.
  96. Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 118 — provability-propositional.tex, line 118.
  97. Proof tree concluding antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 128 — provability-propositional.tex, line 128.
  98. Definition: A valuation v satisfies a sequent antecedent containing Gamma; sequent arrow; succedent… — line 41 — soundness.tex, line 41.
  99. Theorem: Soundness — line 52 — soundness.tex, line 52.
  100. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A — line 79 — soundness.tex, line 79.
  101. Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 84 — soundness.tex, line 84.
  102. Proof tree concluding antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 106 — soundness.tex, line 106.
  103. Proof tree concluding antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 135 — soundness.tex, line 135.
  104. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B — line 163 — soundness.tex, line 163.
  105. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B — line 185 — soundness.tex, line 185.
  106. Proof tree concluding antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda — line 271 — soundness.tex, line 271.
  107. Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B — line 291 — soundness.tex, line 291.
  108. Proof tree concluding antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then Gamma, and finally capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda — line 310 — soundness.tex, line 310.
  109. Exercise: Complete the proof of the sequent-calculus soundness theorem — line 341 — soundness.tex, line 341.
  110. Corollary: If formula A is derivable with no premises then formula A is a tautology — line 346 — soundness.tex, line 346.
  111. Corollary: If Gamma syntactically derives formula A then Gamma semantically entails formula A — line 351 — soundness.tex, line 351.
  112. Corollary: If Gamma is satisfiable, then it is consistent — line 366 — soundness.tex, line 366.

4 source references

  1. First-order sequent-calculus proposition on inconsistency — source line 144.
  2. Theorem: Soundness — line 52 — source line 342.
  3. Theorem: Soundness — line 52 — source line 359.
  4. Theorem: Soundness — line 52 — source line 374.

Four printed-source notes

The printed source is preserved without silent correction.

  1. proving-things.tex, lines 86, 104, 125, 147: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
  2. soundness.tex, line 157: The immediately preceding argument establishes validity of the conclusion with the conjunction on the left; this sentence instead names the premise sequent. Preserve the printed claim and attach a note that the preceding argument appears to establish the conclusion sequent with A and B conjoined on the left.
  3. soundness.tex, line 288: The proof discusses satisfaction of the right premise, but the printed expression is set difference rather than a sequent. Preserve and read the printed expression as capital Pi set difference capital Lambda, then disclose that capital Pi sequent arrow capital Lambda appears intended.
  4. derivations.tex, line 70: The printed conclusion ends with a comma after capital Delta but supplies no following succedent formula. Preserve and speak the printed trailing comma as having no following formula, then disclose that it appears to be stray punctuation.