Expression 1
Inline MathML variant
Block MathML variant
Conventional reading: conjunction
Meaning here: The logical notation read 'conjunction' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
5 occurrences
- Occurrence 1: propositional-rules.tex, line 29, column 23
- Occurrence 2: proving-things.tex, line 27, column 46
- Occurrence 3: proving-things.tex, line 28, column 25
- Occurrence 4: proving-things.tex, line 28, column 53
- Occurrence 5: proving-things.tex, line 248, column 32
Expression 2
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 331, column 7
Expression 3
Inline MathML variant
Block MathML variant
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 relation read 'the union of Gamma sub zero, and capital Delta sub zero is a subset of the union of Gamma, and capital Delta' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 124, column 7
Expression 4
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument constant a
Meaning here: The first-order sequent read 'antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 90, column 12
Expression 5
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument constant a
Meaning here: The first-order sequent read 'antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 49, column 10
- Occurrence 2: proving-things-quant.tex, line 67, column 10
Expression 6
Inline MathML variant
Block MathML variant
Conventional reading: lowercase s
Meaning here: The symbol read 'lowercase s' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
5 occurrences
- Occurrence 1: soundness.tex, line 250, column 52
- Occurrence 2: soundness.tex, line 250, column 65
- Occurrence 3: soundness.tex, line 263, column 3
- Occurrence 4: identity.tex, line 35, column 4
- Occurrence 5: soundness-identity.tex, line 33, column 35
Expression 7
Inline MathML variant
Block MathML variant
Conventional reading: the disjunction of the negation of formula A and formula B
Meaning here: The first-order formula read 'the disjunction of the negation of formula A and formula B' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: proving-things.tex, line 76, column 12
Expression 8
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument term t; sequent arrow; succedent containing for some variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing formula A with argument term t; sequent arrow; succedent containing for some variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 42, column 29
Expression 9
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument term t; sequent arrow; succedent containing for some variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing formula A with argument term t; sequent arrow; succedent containing for some variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 47, column 14
Expression 10
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: proving-things.tex, line 22, column 10
- Occurrence 2: proving-things.tex, line 34, column 10
- Occurrence 3: proving-things.tex, line 44, column 10
Expression 11
Inline MathML variant
Block MathML variant
Conventional reading: term t sub one is identical to variable x
Meaning here: The identity expression read 'term t sub one is identical to variable x' states equality of the named first-order terms or semantic values.
1 occurrence
- Occurrence 1: identity.tex, line 64, column 46
Expression 12
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 332, column 7
Expression 13
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 90, column 16
Expression 14
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 305, column 7
Expression 15
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 57, column 10
Expression 16
Inline MathML variant
Block MathML variant
Conventional reading: structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub two
Meaning here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub two' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 40, column 1
Expression 17
Inline MathML variant
Block MathML variant
Conventional reading: capital Pi
Meaning here: Capital Pi denotes a second antecedent sequence in a sequent rule or derivation.
1 occurrence
- Occurrence 1: derivations.tex, line 72, column 19
Expression 18
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero prime
Meaning here: Gamma sub zero prime denotes a reordered or contracted antecedent sequence used in the proof-theoretic construction.
3 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 39, column 58
- Occurrence 2: proof-theoretic-notions.tex, line 46, column 32
- Occurrence 3: proof-theoretic-notions.tex, line 49, column 18
Expression 19
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 101, column 10
Expression 20
Inline MathML variant
Block MathML variant
Conventional reading: s applied to variable x is identical to the value of constant a in structure M prime under variable assignment lowercase s
Meaning here: The semantic term read 's applied to variable x is identical to the value of constant a in structure M prime under variable assignment lowercase s' specifies an interpretation, term value, or assignment relation in a first-order structure.
1 occurrence
- Occurrence 1: soundness.tex, line 259, column 8
Expression 21
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then atomic formula P applied to constant a, then constant a
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then atomic formula P applied to constant a, then constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 76, column 1
Expression 22
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: provability-consistency.tex, line 92, column 14
- Occurrence 2: provability-propositional.tex, line 123, column 18
Expression 23
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing open parenthesis, the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing for some variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent is formula B, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing open parenthesis, the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing for some variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent is formula B, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 104, column 7
Expression 24
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A with argument constant a, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A with argument constant a, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 37, column 7
Expression 25
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 196, column 10
Expression 26
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of for some variable x, formula A with argument variable x; and whose consequent is for every variable x, the negation of formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of for some variable x, formula A with argument variable x; and whose consequent is for every variable x, the negation of formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 94, column 7
Expression 27
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 34, column 10
- Occurrence 2: proving-things-quant.tex, line 44, column 10
Expression 28
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula A with argument term t
Meaning here: The satisfaction claim read 'structure M satisfies formula A with argument term t' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 222, column 39
Expression 29
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of Gamma
Meaning here: The relation read 'formula C is a member of Gamma' concerns the exact premise sets or formula sequences named by the source.
13 occurrences
- Occurrence 1: soundness.tex, line 93, column 24
- Occurrence 2: soundness.tex, line 97, column 54
- Occurrence 3: soundness.tex, line 116, column 23
- Occurrence 4: soundness.tex, line 122, column 17
- Occurrence 5: soundness.tex, line 146, column 51
- Occurrence 6: soundness.tex, line 150, column 66
- Occurrence 7: soundness.tex, line 173, column 51
- Occurrence 8: soundness.tex, line 176, column 17
- Occurrence 9: soundness.tex, line 201, column 64
- Occurrence 10: soundness.tex, line 219, column 50
- Occurrence 11: soundness.tex, line 241, column 27
- Occurrence 12: soundness.tex, line 245, column 57
- Occurrence 13: soundness.tex, line 254, column 54
Expression 30
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first lowercase s is identical to term t, then formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument term t
Meaning here: The first-order sequent read 'antecedent containing first lowercase s is identical to term t, then formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 42, column 10
Expression 31
Inline MathML variant
Block MathML variant
Conventional reading: the result of substituting term t for variable x in formula A
Meaning here: The substitution expression read 'the result of substituting term t for variable x in formula A' replaces the stated free variable by the stated term, subject to the source convention.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 59, column 41
Expression 32
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument term t
Meaning here: The first-order sequent read 'antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 49, column 30
Expression 33
Inline MathML variant
Block MathML variant
Conventional reading: capital Theta equals first the conjunction of formula A and formula B, then Gamma
Meaning here: The metalevel equality read 'capital Theta equals first the conjunction of formula A and formula B, then Gamma' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: soundness.tex, line 141, column 7
Expression 34
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 64, column 12
Expression 35
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula D; sequent arrow; succedent containing formula D
Meaning here: The first-order sequent read 'antecedent containing formula D; sequent arrow; succedent containing formula D' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: derivations.tex, line 76, column 7
- Occurrence 2: derivations.tex, line 99, column 7
- Occurrence 3: derivations.tex, line 108, column 7
Expression 36
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives formula A with argument constant c
Meaning here: The statement read 'Gamma syntactically derives formula A with argument constant c' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 20, column 28
Expression 37
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for every variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for some variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for every variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for some variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 93, column 7
Expression 38
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 177, column 57
Expression 39
Inline MathML variant
Block MathML variant
Conventional reading: n equals zero
Meaning here: The metalevel equality read 'n equals zero' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 41, column 26
Expression 40
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula C, then formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing first formula C, then formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 60, column 12
Expression 41
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 315, column 7
Expression 42
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 38, column 21
- Occurrence 2: proving-things.tex, line 39, column 48
Expression 43
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then capital Pi; sequent arrow; succedent containing capital Lambda
Meaning here: The first-order sequent read 'antecedent containing first formula A, then capital Pi; sequent arrow; succedent containing capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 275, column 12
Expression 44
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula C; sequent arrow; succedent containing formula C
Meaning here: The first-order sequent read 'antecedent containing formula C; sequent arrow; succedent containing formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: derivations.tex, line 52, column 7
- Occurrence 2: derivations.tex, line 60, column 7
- Occurrence 3: derivations.tex, line 94, column 7
- Occurrence 4: derivations.tex, line 111, column 7
Expression 45
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy formula A with argument term t
Meaning here: The satisfaction claim read 'structure M does not satisfy formula A with argument term t' is evaluated in the named first-order structure and, when printed, the named variable assignment.
2 occurrences
- Occurrence 1: soundness.tex, line 219, column 3
- Occurrence 2: soundness.tex, line 223, column 3
Expression 46
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula B, then formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula B, then formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 198, column 10
Expression 47
Inline MathML variant
Block MathML variant
Conventional reading: n
Meaning here: The natural number n is the number of inferences in the derivation used by the soundness induction.
2 occurrences
- Occurrence 1: soundness.tex, line 59, column 39
- Occurrence 2: soundness.tex, line 71, column 14
Expression 48
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 214, column 14
Expression 49
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument term t
Meaning here: The first-order sequent read 'antecedent containing for every variable x, formula A with argument variable x; sequent arrow; succedent containing formula A with argument term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 54, column 14
Expression 50
Inline MathML variant
Block MathML variant
Conventional reading: capital Theta equals first formula A, then Gamma
Meaning here: The metalevel equality read 'capital Theta equals first formula A, then Gamma' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: soundness.tex, line 98, column 38
Expression 51
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 322, column 7
Expression 52
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 79, column 11
- Occurrence 2: soundness.tex, line 316, column 15
Expression 53
Inline MathML variant
Block MathML variant
Conventional reading: structure M
Meaning here: The expression read 'structure M' denotes the named first-order structure.
11 occurrences
- Occurrence 1: soundness.tex, line 42, column 29
- Occurrence 2: soundness.tex, line 48, column 63
- Occurrence 3: soundness.tex, line 63, column 36
- Occurrence 4: soundness.tex, line 142, column 30
- Occurrence 5: soundness.tex, line 154, column 54
- Occurrence 6: soundness.tex, line 217, column 55
- Occurrence 7: soundness.tex, line 225, column 28
- Occurrence 8: soundness.tex, line 240, column 17
- Occurrence 9: soundness.tex, line 299, column 39
- Occurrence 10: soundness-identity.tex, line 19, column 25
- Occurrence 11: soundness-identity.tex, line 26, column 16
Expression 54
Inline MathML variant
Block MathML variant
Conventional reading: pi sub one
Meaning here: Pi sub one denotes the second cited sequent-calculus derivation.
8 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 112, column 45
- Occurrence 2: proof-theoretic-notions.tex, line 119, column 15
- Occurrence 3: provability-consistency.tex, line 29, column 20
- Occurrence 4: provability-consistency.tex, line 35, column 13
- Occurrence 5: provability-consistency.tex, line 57, column 17
- Occurrence 6: provability-consistency.tex, line 64, column 15
- Occurrence 7: provability-consistency.tex, line 107, column 62
- Occurrence 8: provability-consistency.tex, line 117, column 13
Expression 55
Inline MathML variant
Block MathML variant
Conventional reading: formula A syntactically derives formula B
Meaning here: The statement read 'formula A syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 128, column 68
Expression 56
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: proving-things.tex, line 72, column 10
- Occurrence 2: proving-things.tex, line 87, column 10
- Occurrence 3: proving-things.tex, line 105, column 10
- Occurrence 4: proving-things.tex, line 126, column 10
- Occurrence 5: proving-things.tex, line 148, column 10
Expression 57
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 44, column 10
Expression 58
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda
Meaning here: The first-order sequent read 'antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: soundness.tex, line 321, column 3
- Occurrence 2: soundness.tex, line 323, column 60
Expression 59
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the disjunction of for some variable x, formula A with argument variable x and for some variable y, formula B with argument variable y, close parenthesis; and whose consequent is for some variable z, open parenthesis, the disjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the disjunction of for some variable x, formula A with argument variable x and for some variable y, formula B with argument variable y, close parenthesis; and whose consequent is for some variable z, open parenthesis, the disjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 90, column 7
Expression 60
Inline MathML variant
Block MathML variant
Conventional reading: negation
Meaning here: The logical notation read 'negation' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
6 occurrences
- Occurrence 1: propositional-rules.tex, line 15, column 23
- Occurrence 2: proving-things.tex, line 60, column 45
- Occurrence 3: proving-things.tex, line 63, column 7
- Occurrence 4: proving-things.tex, line 111, column 21
- Occurrence 5: proving-things.tex, line 165, column 27
- Occurrence 6: proving-things.tex, line 248, column 61
Expression 61
Inline MathML variant
Block MathML variant
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
- Occurrence 1: structural-rules.tex, line 71, column 1
Expression 62
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the negation of formula A with argument constant a; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing the negation of formula A with argument constant a; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 55, column 10
Expression 63
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing first formula A, then formula B
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing first formula A, then formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 135, column 10
Expression 64
Inline MathML variant
Block MathML variant
Conventional reading: left weakening rule
Meaning here: The rule label read 'left weakening rule' names the exact side and logical or structural operator printed by the source.
1 occurrence
- Occurrence 1: derivations.tex, line 40, column 1
Expression 65
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 27, column 61
Expression 66
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 72, column 13
- Occurrence 2: proof-theoretic-notions.tex, line 74, column 32
- Occurrence 3: proof-theoretic-notions.tex, line 165, column 19
- Occurrence 4: soundness.tex, line 374, column 4
- Occurrence 5: soundness.tex, line 375, column 1
Expression 67
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 26, column 51
Expression 68
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula D
Meaning here: The first-order sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula D' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: derivations.tex, line 78, column 10
- Occurrence 2: derivations.tex, line 101, column 10
- Occurrence 3: derivations.tex, line 110, column 10
Expression 69
Inline MathML variant
Block MathML variant
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 first-order sequent 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: derivations.tex, line 70, column 10
Expression 70
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: provability-consistency.tex, line 52, column 28
- Occurrence 2: provability-consistency.tex, line 58, column 33
Expression 71
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies the conditional whose antecedent is formula A; and whose consequent is formula B
Meaning here: The satisfaction claim read 'structure M satisfies the conditional whose antecedent is formula A; and whose consequent is formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 199, column 25
Expression 72
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing for every variable x, for every variable y, open parenthesis, the conditional whose antecedent states that open parenthesis, the conjunction whose first conjunct states that variable x is identical to variable y; and whose second conjunct is formula A with argument variable x, close parenthesis; and whose consequent is formula A with argument variable y, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 70, column 7
Expression 73
Inline MathML variant
Block MathML variant
Conventional reading: pi sub zero
Meaning here: Pi sub zero denotes the first cited sequent-calculus derivation.
8 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 110, column 21
- Occurrence 2: proof-theoretic-notions.tex, line 116, column 15
- Occurrence 3: provability-consistency.tex, line 28, column 8
- Occurrence 4: provability-consistency.tex, line 32, column 13
- Occurrence 5: provability-consistency.tex, line 52, column 17
- Occurrence 6: provability-consistency.tex, line 107, column 50
- Occurrence 7: provability-consistency.tex, line 112, column 13
- Occurrence 8: provability-quantifiers.tex, line 25, column 5
Expression 74
Inline MathML variant
Block MathML variant
Conventional reading: variable x
Meaning here: The symbol read 'variable x' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 58, column 14
- Occurrence 2: quantifier-rules.tex, line 72, column 14
Expression 75
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 316, column 7
Expression 76
Inline MathML variant
Block MathML variant
Conventional reading: left negation rule
Meaning here: The rule label read 'left negation rule' names the exact side and logical or structural operator printed by the source.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 53, column 1
Expression 77
Inline MathML variant
Block MathML variant
Conventional reading: constant c
Meaning here: The symbol read 'constant c' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
2 occurrences
- Occurrence 1: provability-quantifiers.tex, line 19, column 40
- Occurrence 2: provability-quantifiers.tex, line 28, column 28
Expression 78
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 48, column 50
Expression 79
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy the negation of formula A
Meaning here: The satisfaction claim read 'structure M does not satisfy the negation of formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 127, column 3
Expression 80
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies the disjunction of formula A and formula B
Meaning here: The satisfaction claim read 'structure M satisfies the disjunction of formula A and formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 175, column 16
Expression 81
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 85, column 25
Expression 82
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub two
Meaning here: The first-order sequent read 'antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub two' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 55, column 7
Expression 83
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant a
Meaning here: The first-order sequent read 'antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: quantifier-rules.tex, line 88, column 9
- Occurrence 2: quantifier-rules.tex, line 95, column 9
- Occurrence 3: proving-things-quant.tex, line 65, column 7
Expression 84
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime, under variable assignment lowercase s, satisfies formula A with argument variable x
Meaning here: The satisfaction claim read 'structure M prime, under variable assignment lowercase s, satisfies formula A with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 261, column 10
Expression 85
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero double prime; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero double prime; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 48, column 1
Expression 86
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 20, column 10
- Occurrence 2: soundness.tex, line 110, column 14
Expression 87
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula B
Meaning here: The satisfaction claim read 'structure M satisfies formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
2 occurrences
- Occurrence 1: soundness.tex, line 196, column 3
- Occurrence 2: soundness.tex, line 306, column 3
Expression 88
Inline MathML variant
Block MathML variant
Conventional reading: formula A with argument term t syntactically derives for some variable x, formula A with argument variable x
Meaning here: The statement read 'formula A with argument term t syntactically derives for some variable x, formula A with argument variable x' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 35, column 17
Expression 89
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 85, column 54
Expression 90
Inline MathML variant
Block MathML variant
Conventional reading: identity sign
Meaning here: The logical notation read 'identity sign' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 23, column 50
Expression 91
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: propositional-rules.tex, line 47, column 11
- Occurrence 2: derivations.tex, line 86, column 11
- Occurrence 3: soundness.tex, line 297, column 15
Expression 92
Inline MathML variant
Block MathML variant
Conventional reading: first lowercase s is identical to term t, then formula A with argument lowercase s syntactically derives formula A with argument term t
Meaning here: The statement read 'first lowercase s is identical to term t, then formula A with argument lowercase s syntactically derives formula A with argument term t' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: identity.tex, line 35, column 39
Expression 93
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 117, column 10
- Occurrence 2: provability-consistency.tex, line 33, column 8
- Occurrence 3: provability-consistency.tex, line 87, column 12
Expression 94
Inline MathML variant
Block MathML variant
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 metalevel equality read 'capital Delta equals the finite sequence first formula B sub one, continuing through the omitted intermediate entries, and finally formula B sub n' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 32, column 1
Expression 95
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero prime equals the finite sequence first formula B, then formula B, and finally formula C
Meaning here: The metalevel equality read 'Gamma sub zero prime equals the finite sequence first formula B, then formula B, and finally formula C' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 50, column 11
Expression 96
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 218, column 10
- Occurrence 2: proving-things.tex, line 239, column 10
Expression 97
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 108, column 4
Expression 98
Inline MathML variant
Block MathML variant
Conventional reading: atomic formula P applied to term t, then variable x
Meaning here: The atomic first-order formula read 'atomic formula P applied to term t, then variable x' preserves the predicate and ordered term arguments.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 67, column 4
Expression 99
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 85, column 11
- Occurrence 2: proving-things.tex, line 103, column 11
- Occurrence 3: proving-things.tex, line 124, column 11
- Occurrence 4: proving-things.tex, line 146, column 11
Expression 100
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant a
Meaning here: The first-order sequent read 'antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 24, column 16
- Occurrence 2: proving-things-quant.tex, line 62, column 22
Expression 101
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy the conjunction of formula A and formula B
Meaning here: The satisfaction claim read 'structure M does not satisfy the conjunction of formula A and formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 148, column 16
Expression 102
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then formula B, and finally formula C; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing first formula B, then formula B, and finally formula C; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 56, column 10
Expression 103
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub two is identical to term t sub three, then term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub three
Meaning here: The first-order sequent read 'antecedent containing first term t sub two is identical to term t sub three, then term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub three' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 59, column 10
Expression 104
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 279, column 10
- Occurrence 2: proving-things.tex, line 294, column 10
Expression 105
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 118, column 8
Expression 106
Inline MathML variant
Block MathML variant
Conventional reading: structure M
Meaning here: The expression read 'structure M' denotes the named first-order structure.
25 occurrences
- Occurrence 1: soundness.tex, line 92, column 29
- Occurrence 2: soundness.tex, line 115, column 41
- Occurrence 3: soundness.tex, line 120, column 49
- Occurrence 4: soundness.tex, line 156, column 31
- Occurrence 5: soundness.tex, line 170, column 30
- Occurrence 6: soundness.tex, line 179, column 26
- Occurrence 7: soundness.tex, line 181, column 21
- Occurrence 8: soundness.tex, line 193, column 15
- Occurrence 9: soundness.tex, line 204, column 21
- Occurrence 10: soundness.tex, line 206, column 15
- Occurrence 11: soundness.tex, line 224, column 8
- Occurrence 12: soundness.tex, line 244, column 11
- Occurrence 13: soundness.tex, line 252, column 46
- Occurrence 14: soundness.tex, line 279, column 19
- Occurrence 15: soundness.tex, line 281, column 18
- Occurrence 16: soundness.tex, line 284, column 19
- Occurrence 17: soundness.tex, line 287, column 15
- Occurrence 18: soundness.tex, line 289, column 15
- Occurrence 19: soundness.tex, line 301, column 15
- Occurrence 20: soundness.tex, line 319, column 30
- Occurrence 21: soundness.tex, line 320, column 27
- Occurrence 22: soundness.tex, line 323, column 15
- Occurrence 23: soundness.tex, line 360, column 27
- Occurrence 24: soundness.tex, line 376, column 27
- Occurrence 25: soundness.tex, line 380, column 13
Expression 107
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then formula B; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 99, column 10
- Occurrence 2: proving-things.tex, line 120, column 10
- Occurrence 3: proving-things.tex, line 142, column 10
- Occurrence 4: provability-propositional.tex, line 131, column 18
Expression 108
Inline MathML variant
Block MathML variant
Conventional reading: first formula A, then Gamma
Meaning here: The sequence read 'first formula A, then Gamma' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 47, column 64
Expression 109
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 125, column 18
Expression 110
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 303, column 7
Expression 111
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument constant a; sequent arrow; succedent containing for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing formula A with argument constant a; sequent arrow; succedent containing for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 97, column 12
Expression 112
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub two
Meaning here: The first-order sequent read 'antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub two' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: identity.tex, line 25, column 10
- Occurrence 2: identity.tex, line 28, column 7
Expression 113
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A with argument constant c
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A with argument constant c' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 25, column 48
Expression 114
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 155, column 50
Expression 115
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 261, column 10
- Occurrence 2: proving-things.tex, line 268, column 10
- Occurrence 3: proving-things.tex, line 281, column 10
- Occurrence 4: proving-things.tex, line 296, column 10
Expression 116
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 113, column 8
Expression 117
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 127, column 18
Expression 118
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing capital Theta; sequent arrow; succedent containing capital Xi
Meaning here: The first-order sequent read 'antecedent containing capital Theta; sequent arrow; succedent containing capital Xi' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
9 occurrences
- Occurrence 1: soundness.tex, line 53, column 59
- Occurrence 2: soundness.tex, line 54, column 21
- Occurrence 3: soundness.tex, line 58, column 33
- Occurrence 4: soundness.tex, line 75, column 48
- Occurrence 5: soundness.tex, line 102, column 36
- Occurrence 6: soundness.tex, line 119, column 62
- Occurrence 7: soundness.tex, line 129, column 57
- Occurrence 8: soundness.tex, line 180, column 47
- Occurrence 9: soundness.tex, line 182, column 3
Expression 119
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy formula A
Meaning here: The satisfaction claim read 'structure M does not satisfy formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.
5 occurrences
- Occurrence 1: soundness.tex, line 45, column 1
- Occurrence 2: soundness.tex, line 64, column 1
- Occurrence 3: soundness.tex, line 145, column 3
- Occurrence 4: soundness.tex, line 195, column 22
- Occurrence 5: soundness.tex, line 282, column 33
Expression 120
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: propositional-rules.tex, line 45, column 7
- Occurrence 2: propositional-rules.tex, line 66, column 7
- Occurrence 3: derivations.tex, line 84, column 7
- Occurrence 4: soundness.tex, line 295, column 12
Expression 121
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy formula C
Meaning here: The satisfaction claim read 'structure M does not satisfy formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.
17 occurrences
- Occurrence 1: soundness.tex, line 94, column 3
- Occurrence 2: soundness.tex, line 97, column 6
- Occurrence 3: soundness.tex, line 99, column 3
- Occurrence 4: soundness.tex, line 117, column 3
- Occurrence 5: soundness.tex, line 123, column 3
- Occurrence 6: soundness.tex, line 129, column 3
- Occurrence 7: soundness.tex, line 146, column 3
- Occurrence 8: soundness.tex, line 150, column 3
- Occurrence 9: soundness.tex, line 151, column 25
- Occurrence 10: soundness.tex, line 173, column 3
- Occurrence 11: soundness.tex, line 177, column 3
- Occurrence 12: soundness.tex, line 197, column 3
- Occurrence 13: soundness.tex, line 202, column 12
- Occurrence 14: soundness.tex, line 219, column 26
- Occurrence 15: soundness.tex, line 241, column 3
- Occurrence 16: soundness.tex, line 247, column 3
- Occurrence 17: soundness.tex, line 378, column 1
Expression 122
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 304, column 58
Expression 123
Inline MathML variant
Block MathML variant
Conventional reading: right universal quantifier rule
Meaning here: The rule label read 'right universal quantifier rule' names the exact side and logical or structural operator printed by the source.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 76, column 52
- Occurrence 2: provability-quantifiers.tex, line 27, column 1
Expression 124
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma sub zero; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 83, column 11
Expression 125
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula C
Meaning here: The satisfaction claim read 'structure M satisfies formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.
17 occurrences
- Occurrence 1: soundness.tex, line 95, column 21
- Occurrence 2: soundness.tex, line 100, column 17
- Occurrence 3: soundness.tex, line 101, column 29
- Occurrence 4: soundness.tex, line 118, column 12
- Occurrence 5: soundness.tex, line 125, column 3
- Occurrence 6: soundness.tex, line 147, column 7
- Occurrence 7: soundness.tex, line 153, column 8
- Occurrence 8: soundness.tex, line 174, column 7
- Occurrence 9: soundness.tex, line 178, column 25
- Occurrence 10: soundness.tex, line 198, column 7
- Occurrence 11: soundness.tex, line 201, column 3
- Occurrence 12: soundness.tex, line 203, column 25
- Occurrence 13: soundness.tex, line 220, column 7
- Occurrence 14: soundness.tex, line 241, column 51
- Occurrence 15: soundness.tex, line 246, column 12
- Occurrence 16: soundness-identity.tex, line 28, column 8
- Occurrence 17: soundness-identity.tex, line 32, column 14
Expression 126
Inline MathML variant
Block MathML variant
Conventional reading: disjunction
Meaning here: The logical notation read 'disjunction' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
4 occurrences
- Occurrence 1: propositional-rules.tex, line 51, column 23
- Occurrence 2: proving-things.tex, line 60, column 54
- Occurrence 3: proving-things.tex, line 61, column 42
- Occurrence 4: proving-things.tex, line 165, column 5
Expression 127
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 53, column 17
Expression 128
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 221, column 11
- Occurrence 2: proving-things.tex, line 242, column 11
Expression 129
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 338, column 7
Expression 130
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub two is identical to term t sub one
Meaning here: The first-order sequent read 'antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub two is identical to term t sub one' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 53, column 10
Expression 131
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 67, column 13
Expression 132
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma sub zero, then capital Delta sub zero; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first Gamma sub zero, then capital Delta sub zero; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 122, column 13
Expression 133
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first Gamma, then formula B, then formula A, and finally capital Pi; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: structural-rules.tex, line 56, column 10
Expression 134
Inline MathML variant
Block MathML variant
Conventional reading: the union of the set containing formula A, and capital Delta syntactically derives formula B
Meaning here: The statement read 'the union of the set containing formula A, and capital Delta syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 104, column 28
- Occurrence 2: proof-theoretic-notions.tex, line 110, column 60
Expression 135
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime satisfies formula C
Meaning here: The satisfaction claim read 'structure M prime satisfies formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 255, column 3
Expression 136
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: proving-things.tex, line 171, column 10
- Occurrence 2: proving-things.tex, line 185, column 10
- Occurrence 3: proving-things.tex, line 204, column 10
- Occurrence 4: proving-things.tex, line 223, column 10
- Occurrence 5: proving-things.tex, line 244, column 10
Expression 137
Inline MathML variant
Block MathML variant
Conventional reading: the interpretation of constant a in structure M prime equals s applied to variable x
Meaning here: The semantic term read 'the interpretation of constant a in structure M prime equals s applied to variable x' specifies an interpretation, term value, or assignment relation in a first-order structure.
1 occurrence
- Occurrence 1: soundness.tex, line 253, column 3
Expression 138
Inline MathML variant
Block MathML variant
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.
34 occurrences
- Occurrence 1: rules-and-proofs.tex, line 23, column 7
- Occurrence 2: rules-and-proofs.tex, line 24, column 42
- Occurrence 3: rules-and-proofs.tex, line 38, column 43
- Occurrence 4: rules-and-proofs.tex, line 39, column 25
- Occurrence 5: rules-and-proofs.tex, line 46, column 4
- Occurrence 6: rules-and-proofs.tex, line 47, column 50
- Occurrence 7: rules-and-proofs.tex, line 49, column 4
- Occurrence 8: derivations.tex, line 49, column 1
- Occurrence 9: derivations.tex, line 72, column 6
- Occurrence 10: derivations.tex, line 89, column 57
- Occurrence 11: proof-theoretic-notions.tex, line 38, column 15
- Occurrence 12: proof-theoretic-notions.tex, line 41, column 61
- Occurrence 13: proof-theoretic-notions.tex, line 70, column 20
- Occurrence 14: proof-theoretic-notions.tex, line 72, column 43
- Occurrence 15: proof-theoretic-notions.tex, line 135, column 1
- Occurrence 16: proof-theoretic-notions.tex, line 152, column 35
- Occurrence 17: proof-theoretic-notions.tex, line 153, column 22
- Occurrence 18: proof-theoretic-notions.tex, line 163, column 14
- Occurrence 19: proof-theoretic-notions.tex, line 166, column 24
- Occurrence 20: provability-consistency.tex, line 21, column 22
- Occurrence 21: provability-consistency.tex, line 42, column 50
- Occurrence 22: provability-consistency.tex, line 76, column 58
- Occurrence 23: provability-consistency.tex, line 97, column 14
- Occurrence 24: provability-consistency.tex, line 102, column 22
- Occurrence 25: provability-consistency.tex, line 123, column 50
- Occurrence 26: provability-quantifiers.tex, line 20, column 4
- Occurrence 27: provability-quantifiers.tex, line 28, column 50
- Occurrence 28: soundness.tex, line 237, column 21
- Occurrence 29: soundness.tex, line 255, column 46
- Occurrence 30: soundness.tex, line 368, column 4
- Occurrence 31: soundness.tex, line 372, column 44
- Occurrence 32: soundness.tex, line 379, column 41
- Occurrence 33: soundness.tex, line 380, column 52
- Occurrence 34: soundness.tex, line 381, column 1
Expression 139
Inline MathML variant
Block MathML variant
Conventional reading: syntactic derivability
Meaning here: The logical notation read 'syntactic derivability' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
2 occurrences
- Occurrence 1: provability-propositional.tex, line 19, column 51
- Occurrence 2: provability-quantifiers.tex, line 14, column 31
Expression 140
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
8 occurrences
- Occurrence 1: propositional-rules.tex, line 23, column 7
- Occurrence 2: propositional-rules.tex, line 33, column 7
- Occurrence 3: propositional-rules.tex, line 54, column 7
- Occurrence 4: structural-rules.tex, line 28, column 10
- Occurrence 5: structural-rules.tex, line 42, column 10
- Occurrence 6: derivations.tex, line 44, column 10
- Occurrence 7: soundness.tex, line 83, column 14
- Occurrence 8: soundness.tex, line 137, column 12
Expression 141
Inline MathML variant
Block MathML variant
Conventional reading: s applied to variable x is identical to the value of term t sub one in structure M
Meaning here: The semantic term read 's applied to variable x is identical to the value of term t sub one in structure M' specifies an interpretation, term value, or assignment relation in a first-order structure.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 34, column 1
Expression 142
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for every variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is for some variable y, formula A with argument variable y; and whose consequent is formula B
Meaning here: The first-order sequent read 'antecedent containing for every variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is formula B, close parenthesis; sequent arrow; succedent containing the conditional whose antecedent is for some variable y, formula A with argument variable y; and whose consequent is formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 92, column 7
Expression 143
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 39, column 59
Expression 144
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 32, column 30
Expression 145
Inline MathML variant
Block MathML variant
Conventional reading: capital Xi equals capital Delta
Meaning here: The metalevel equality read 'capital Xi equals capital Delta' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
3 occurrences
- Occurrence 1: soundness.tex, line 112, column 41
- Occurrence 2: soundness.tex, line 141, column 44
- Occurrence 3: soundness.tex, line 154, column 9
Expression 146
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument constant a
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument constant a' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 21, column 7
- Occurrence 2: soundness.tex, line 232, column 12
Expression 147
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 82, column 7
- Occurrence 2: soundness.tex, line 187, column 12
Expression 148
Inline MathML variant
Block MathML variant
Conventional reading: term t sub two
Meaning here: The symbol read 'term t sub two' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
1 occurrence
- Occurrence 1: identity.tex, line 20, column 36
Expression 149
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the empty sequence; sequent arrow; succedent containing term t is identical to term t
Meaning here: The first-order sequent read 'antecedent containing the empty sequence; sequent arrow; succedent containing term t is identical to term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: identity.tex, line 17, column 31
- Occurrence 2: soundness-identity.tex, line 18, column 30
Expression 150
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing first formula B, then formula A
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing first formula B, then formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 115, column 10
- Occurrence 2: proving-things.tex, line 137, column 10
Expression 151
Inline MathML variant
Block MathML variant
Conventional reading: Gamma is a subset of capital Delta
Meaning here: The relation read 'Gamma is a subset of capital Delta' concerns the exact premise sets or formula sequences named by the source.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 90, column 4
- Occurrence 2: proof-theoretic-notions.tex, line 97, column 22
Expression 152
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime, under variable assignment lowercase s, satisfies formula A with argument constant a
Meaning here: The satisfaction claim read 'structure M prime, under variable assignment lowercase s, satisfies formula A with argument constant a' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 258, column 3
Expression 153
Inline MathML variant
Block MathML variant
Conventional reading: zero
Meaning here: The number zero.
1 occurrence
- Occurrence 1: soundness.tex, line 61, column 32
Expression 154
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: derivations.tex, line 103, column 11
Expression 155
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing for some variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is for every variable y, formula A with argument variable y, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing for some variable x, open parenthesis, the conditional whose antecedent is formula A with argument variable x; and whose consequent is for every variable y, formula A with argument variable y, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 105, column 7
Expression 156
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 120, column 10
Expression 157
Inline MathML variant
Block MathML variant
Conventional reading: the union of Gamma, and capital Delta syntactically derives formula B
Meaning here: The statement read 'the union of Gamma, and capital Delta syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 105, column 11
- Occurrence 2: proof-theoretic-notions.tex, line 125, column 7
Expression 158
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B
Meaning here: The relation read 'formula C is a member of first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 200, column 21
Expression 159
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 215, column 10
- Occurrence 2: proving-things.tex, line 233, column 10
Expression 160
Inline MathML variant
Block MathML variant
Conventional reading: left exchange rule
Meaning here: The rule label read 'left exchange rule' names the exact side and logical or structural operator printed by the source.
1 occurrence
- Occurrence 1: derivations.tex, line 56, column 36
Expression 161
Inline MathML variant
Block MathML variant
Conventional reading: the sequent calculus L K
Meaning here: L K is the classical sequent calculus defined and used in this chapter.
23 occurrences
- Occurrence 1: rules-and-proofs.tex, line 66, column 50
- Occurrence 2: derivations.tex, line 23, column 14
- Occurrence 3: derivations.tex, line 24, column 10
- Occurrence 4: derivations.tex, line 34, column 36
- Occurrence 5: derivations.tex, line 34, column 52
- Occurrence 6: proving-things.tex, line 16, column 9
- Occurrence 7: proving-things.tex, line 46, column 23
- Occurrence 8: proving-things.tex, line 51, column 9
- Occurrence 9: proving-things.tex, line 155, column 9
- Occurrence 10: proving-things-quant.tex, line 14, column 9
- Occurrence 11: proof-theoretic-notions.tex, line 32, column 4
- Occurrence 12: proof-theoretic-notions.tex, line 40, column 46
- Occurrence 13: proof-theoretic-notions.tex, line 71, column 53
- Occurrence 14: proof-theoretic-notions.tex, line 74, column 1
- Occurrence 15: proof-theoretic-notions.tex, line 164, column 52
- Occurrence 16: provability-consistency.tex, line 26, column 1
- Occurrence 17: provability-consistency.tex, line 27, column 27
- Occurrence 18: provability-consistency.tex, line 28, column 24
- Occurrence 19: provability-consistency.tex, line 107, column 23
- Occurrence 20: provability-quantifiers.tex, line 25, column 19
- Occurrence 21: soundness.tex, line 53, column 36
- Occurrence 22: identity.tex, line 47, column 1
- Occurrence 23: soundness-identity.tex, line 14, column 1
Expression 162
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 259, column 10
Expression 163
Inline MathML variant
Block MathML variant
Conventional reading: variable x is identical to term t sub one
Meaning here: The identity expression read 'variable x is identical to term t sub one' states equality of the named first-order terms or semantic values.
1 occurrence
- Occurrence 1: identity.tex, line 63, column 52
Expression 164
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument term t; sequent arrow; succedent containing formula A with argument term t
Meaning here: The first-order sequent read 'antecedent containing formula A with argument term t; sequent arrow; succedent containing formula A with argument term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: provability-quantifiers.tex, line 45, column 11
- Occurrence 2: provability-quantifiers.tex, line 52, column 11
Expression 165
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the negation of for some variable x, for every variable y, open parenthesis, the conjunction of open parenthesis, the conditional whose antecedent is formula A with arguments variable x and variable y; and whose consequent is the negation of formula A with arguments variable y and variable y, close parenthesis and open parenthesis, the conditional whose antecedent is the negation of formula A with arguments variable y and variable y; and whose consequent is formula A with arguments variable x and variable y, close parenthesis, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the negation of for some variable x, for every variable y, open parenthesis, the conjunction of open parenthesis, the conditional whose antecedent is formula A with arguments variable x and variable y; and whose consequent is the negation of formula A with arguments variable y and variable y, close parenthesis and open parenthesis, the conditional whose antecedent is the negation of formula A with arguments variable y and variable y; and whose consequent is formula A with arguments variable x and variable y, close parenthesis, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 95, column 7
Expression 166
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 193, column 64
Expression 167
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 333, column 7
Expression 168
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives the negation of formula A
Meaning here: The statement read 'Gamma syntactically derives the negation of formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 72, column 12
Expression 169
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy the conditional whose antecedent is formula A; and whose consequent is formula B
Meaning here: The satisfaction claim read 'structure M does not satisfy the conditional whose antecedent is formula A; and whose consequent is formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
2 occurrences
- Occurrence 1: soundness.tex, line 322, column 3
- Occurrence 2: soundness.tex, line 329, column 3
Expression 170
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of Gamma sub zero
Meaning here: The relation read 'formula C is a member of Gamma sub zero' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 377, column 10
Expression 171
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: propositional-rules.tex, line 63, column 10
- Occurrence 2: propositional-rules.tex, line 68, column 10
- Occurrence 3: soundness.tex, line 167, column 14
Expression 172
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C
Meaning here: The first-order sequent read 'antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: derivations.tex, line 54, column 10
- Occurrence 2: derivations.tex, line 62, column 10
- Occurrence 3: derivations.tex, line 96, column 10
- Occurrence 4: derivations.tex, line 113, column 10
Expression 173
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 178, column 49
Expression 174
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: provability-consistency.tex, line 53, column 52
- Occurrence 2: provability-consistency.tex, line 57, column 28
Expression 175
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first formula A, then capital Delta sub zero; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 112, column 56
Expression 176
Inline MathML variant
Block MathML variant
Conventional reading: identity sign
Meaning here: The logical notation read 'identity sign' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
8 occurrences
- Occurrence 1: identity.tex, line 16, column 35
- Occurrence 2: identity.tex, line 20, column 15
- Occurrence 3: identity.tex, line 24, column 13
- Occurrence 4: identity.tex, line 29, column 13
- Occurrence 5: identity.tex, line 41, column 13
- Occurrence 6: identity.tex, line 47, column 24
- Occurrence 7: identity.tex, line 52, column 13
- Occurrence 8: identity.tex, line 58, column 13
Expression 177
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 237, column 10
- Occurrence 2: provability-propositional.tex, line 46, column 16
Expression 178
Inline MathML variant
Block MathML variant
Conventional reading: first formula A sub one, continuing through the omitted intermediate formulas, and finally formula A sub n syntactically derives formula B
Meaning here: The statement read 'first formula A sub one, continuing through the omitted intermediate formulas, and finally formula A sub n syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 129, column 64
Expression 179
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for every variable x, atomic formula P applied to constant a, then variable x
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for every variable x, atomic formula P applied to constant a, then variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 75, column 7
Expression 180
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies for every variable x, formula A with argument variable x
Meaning here: The satisfaction claim read 'structure M satisfies for every variable x, formula A with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.
3 occurrences
- Occurrence 1: soundness.tex, line 222, column 3
- Occurrence 2: soundness.tex, line 240, column 34
- Occurrence 3: soundness.tex, line 248, column 3
Expression 181
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 277, column 10
- Occurrence 2: proving-things.tex, line 292, column 10
Expression 182
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero equals the set containing first formula B, then formula C
Meaning here: The metalevel equality read 'Gamma sub zero equals the set containing first formula B, then formula C' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 49, column 49
Expression 183
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: soundness.tex, line 204, column 60
- Occurrence 2: soundness.tex, line 206, column 59
Expression 184
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula C, then formula C, and finally formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing first formula C, then formula C, and finally formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 62, column 12
Expression 185
Inline MathML variant
Block MathML variant
Conventional reading: formula B syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B
Meaning here: The statement read 'formula B syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 103, column 44
Expression 186
Inline MathML variant
Block MathML variant
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 sequence read 'first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 60, column 9
Expression 187
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 337, column 7
Expression 188
Inline MathML variant
Block MathML variant
Conventional reading: formula A with argument variable x
Meaning here: The first-order formula read 'formula A with argument variable x' preserves its metavariables, connectives, term arguments, and written grouping.
9 occurrences
- Occurrence 1: quantifier-rules.tex, line 58, column 52
- Occurrence 2: provability-quantifiers.tex, line 20, column 16
- Occurrence 3: provability-quantifiers.tex, line 28, column 62
- Occurrence 4: soundness.tex, line 209, column 16
- Occurrence 5: soundness.tex, line 229, column 16
- Occurrence 6: soundness.tex, line 237, column 12
- Occurrence 7: soundness.tex, line 261, column 60
- Occurrence 8: identity.tex, line 64, column 1
- Occurrence 9: identity.tex, line 64, column 32
Expression 189
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero double prime equals the finite sequence first formula C, then formula C, and finally formula B
Meaning here: The metalevel equality read 'Gamma sub zero double prime equals the finite sequence first formula C, then formula C, and finally formula B' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 50, column 48
Expression 190
Inline MathML variant
Block MathML variant
Conventional reading: formula A
Meaning here: The first-order formula read 'formula A' preserves its metavariables, connectives, term arguments, and written grouping.
26 occurrences
- Occurrence 1: rules-and-proofs.tex, line 47, column 25
- Occurrence 2: rules-and-proofs.tex, line 48, column 37
- Occurrence 3: rules-and-proofs.tex, line 60, column 53
- Occurrence 4: rules-and-proofs.tex, line 69, column 44
- Occurrence 5: quantifier-rules.tex, line 57, column 33
- Occurrence 6: quantifier-rules.tex, line 66, column 36
- Occurrence 7: quantifier-rules.tex, line 66, column 48
- Occurrence 8: quantifier-rules.tex, line 74, column 36
- Occurrence 9: derivations.tex, line 46, column 63
- Occurrence 10: derivations.tex, line 73, column 1
- Occurrence 11: derivations.tex, line 90, column 30
- Occurrence 12: derivations.tex, line 105, column 51
- Occurrence 13: proving-things.tex, line 180, column 12
- Occurrence 14: proving-things-quant.tex, line 63, column 21
- Occurrence 15: proof-theoretic-notions.tex, line 31, column 16
- Occurrence 16: proof-theoretic-notions.tex, line 33, column 8
- Occurrence 17: proof-theoretic-notions.tex, line 37, column 16
- Occurrence 18: proof-theoretic-notions.tex, line 41, column 30
- Occurrence 19: proof-theoretic-notions.tex, line 136, column 12
- Occurrence 20: soundness.tex, line 22, column 27
- Occurrence 21: soundness.tex, line 133, column 46
- Occurrence 22: soundness.tex, line 158, column 65
- Occurrence 23: soundness.tex, line 161, column 46
- Occurrence 24: soundness.tex, line 183, column 52
- Occurrence 25: soundness.tex, line 348, column 22
- Occurrence 26: soundness.tex, line 361, column 52
Expression 191
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing falsum; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing falsum; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 58, column 24
Expression 192
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda
Meaning here: The first-order sequent read 'antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 77, column 7
- Occurrence 2: soundness.tex, line 314, column 12
Expression 193
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: proving-things.tex, line 16, column 51
- Occurrence 2: proving-things.tex, line 46, column 64
- Occurrence 3: provability-propositional.tex, line 37, column 23
Expression 194
Inline MathML variant
Block MathML variant
Conventional reading: formula B syntactically derives the disjunction of formula A and formula B
Meaning here: The statement read 'formula B syntactically derives the disjunction of formula A and formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 61, column 42
Expression 195
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula C and formula D' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: derivations.tex, line 91, column 52
Expression 196
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula A with argument term t sub two
Meaning here: The satisfaction claim read 'structure M satisfies formula A with argument term t sub two' is evaluated in the named first-order structure and, when printed, the named variable assignment.
2 occurrences
- Occurrence 1: soundness-identity.tex, line 28, column 50
- Occurrence 2: soundness-identity.tex, line 41, column 1
Expression 197
Inline MathML variant
Block MathML variant
Conventional reading: variable assignment lowercase s agrees with variable assignment lowercase s except possibly at variable x
Meaning here: The semantic term read 'variable assignment lowercase s agrees with variable assignment lowercase s except possibly at variable x' specifies an interpretation, term value, or assignment relation in a first-order structure.
2 occurrences
- Occurrence 1: soundness.tex, line 258, column 58
- Occurrence 2: soundness-identity.tex, line 35, column 30
Expression 198
Inline MathML variant
Block MathML variant
Conventional reading: right conjunction rule
Meaning here: The rule label read 'right conjunction rule' names the exact side and logical or structural operator printed by the source.
1 occurrence
- Occurrence 1: derivations.tex, line 81, column 12
Expression 199
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub one
Meaning here: The first-order sequent read 'antecedent containing term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub one' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 51, column 10
Expression 200
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A with argument term t, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A with argument term t, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 16, column 7
- Occurrence 2: soundness.tex, line 212, column 12
Expression 201
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 229, column 7
Expression 202
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing first formula A, then the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 288, column 10
- Occurrence 2: provability-consistency.tex, line 62, column 12
Expression 203
Inline MathML variant
Block MathML variant
Conventional reading: the negation of open parenthesis, the conjunction beginning with formula A sub one, continuing through the omitted intermediate conjunctions, and ending with formula A sub m, close parenthesis
Meaning here: The first-order formula read 'the negation of open parenthesis, the conjunction beginning with formula A sub one, continuing through the omitted intermediate conjunctions, and ending with formula A sub m, close parenthesis' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 42, column 1
Expression 204
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of for every variable x, formula A with argument variable x; and whose consequent is for some variable x, the negation of formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is the negation of for every variable x, formula A with argument variable x; and whose consequent is for some variable x, the negation of formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 103, column 7
Expression 205
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 116, column 25
Expression 206
Inline MathML variant
Block MathML variant
Conventional reading: m equals zero
Meaning here: The metalevel equality read 'm equals zero' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 39, column 50
Expression 207
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub two is identical to term t sub three, then term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub two
Meaning here: The first-order sequent read 'antecedent containing first term t sub two is identical to term t sub three, then term t sub one is identical to term t sub two; sequent arrow; succedent containing term t sub one is identical to term t sub two' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 57, column 10
Expression 208
Inline MathML variant
Block MathML variant
Conventional reading: first Gamma, then capital Delta, then capital Pi, and finally capital Lambda
Meaning here: The sequence read 'first Gamma, then capital Delta, then capital Pi, and finally capital Lambda' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 15, column 24
Expression 209
Inline MathML variant
Block MathML variant
Conventional reading: first Gamma, then capital Delta
Meaning here: The sequence read 'first Gamma, then capital Delta' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 49, column 69
Expression 210
Inline MathML variant
Block MathML variant
Conventional reading: S
Meaning here: The metavariable S denotes a sequent, especially the end-sequent of a derivation.
5 occurrences
- Occurrence 1: derivations.tex, line 24, column 50
- Occurrence 2: derivations.tex, line 28, column 45
- Occurrence 3: derivations.tex, line 29, column 40
- Occurrence 4: derivations.tex, line 33, column 18
- Occurrence 5: derivations.tex, line 34, column 6
Expression 211
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 317, column 7
Expression 212
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives formula A sub i
Meaning here: The statement read 'Gamma syntactically derives formula A sub i' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 130, column 29
Expression 213
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 318, column 7
Expression 214
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A with argument term t, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A with argument term t, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 218, column 21
Expression 215
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 320, column 7
Expression 216
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first Gamma, then formula A, then formula B, and finally capital Pi; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: structural-rules.tex, line 54, column 7
- Occurrence 2: derivations.tex, line 68, column 7
Expression 217
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the result of substituting term t for variable x in formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the result of substituting term t for variable x in formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 62, column 9
Expression 218
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 38, column 11
Expression 219
Inline MathML variant
Block MathML variant
Conventional reading: universal quantifier
Meaning here: The logical notation read 'universal quantifier' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 13, column 23
- Occurrence 2: proving-things-quant.tex, line 26, column 45
Expression 220
Inline MathML variant
Block MathML variant
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: The statement read 'first formula A, then the conditional whose antecedent is formula A; and whose consequent is formula B syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: provability-propositional.tex, line 22, column 19
- Occurrence 2: provability-propositional.tex, line 101, column 46
Expression 221
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub two
Meaning here: The first-order sequent read 'antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub two' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 25, column 4
Expression 222
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 23, column 10
- Occurrence 2: soundness.tex, line 234, column 14
Expression 223
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first for every variable x, formula A with argument variable x, then the negation of formula A with argument constant a; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first for every variable x, formula A with argument variable x, then the negation of formula A with argument constant a; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 53, column 10
- Occurrence 2: proving-things-quant.tex, line 71, column 10
Expression 224
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the disjunction of formula A and the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 255, column 7
Expression 225
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing the conjunction of formula D and formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: derivations.tex, line 117, column 11
Expression 226
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero prime; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero prime; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 41, column 1
- Occurrence 2: proof-theoretic-notions.tex, line 47, column 9
Expression 227
Inline MathML variant
Block MathML variant
Conventional reading: formula C
Meaning here: The first-order formula read 'formula C' preserves its metavariables, connectives, term arguments, and written grouping.
6 occurrences
- Occurrence 1: derivations.tex, line 49, column 32
- Occurrence 2: derivations.tex, line 72, column 49
- Occurrence 3: derivations.tex, line 73, column 38
- Occurrence 4: derivations.tex, line 90, column 38
- Occurrence 5: derivations.tex, line 106, column 33
- Occurrence 6: soundness.tex, line 379, column 25
Expression 228
Inline MathML variant
Block MathML variant
Conventional reading: the negation of formula A is a member of Gamma
Meaning here: The relation read 'the negation of formula A is a member of Gamma' concerns the exact premise sets or formula sequences named by the source.
3 occurrences
- Occurrence 1: provability-consistency.tex, line 76, column 30
- Occurrence 2: provability-consistency.tex, line 81, column 35
- Occurrence 3: provability-consistency.tex, line 96, column 9
Expression 229
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula A with argument term t sub one
Meaning here: The satisfaction claim read 'structure M satisfies formula A with argument term t sub one' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 32, column 35
Expression 230
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
14 occurrences
- Occurrence 1: propositional-rules.tex, line 18, column 7
- Occurrence 2: propositional-rules.tex, line 44, column 7
- Occurrence 3: propositional-rules.tex, line 61, column 7
- Occurrence 4: propositional-rules.tex, line 76, column 7
- Occurrence 5: structural-rules.tex, line 33, column 10
- Occurrence 6: structural-rules.tex, line 47, column 10
- Occurrence 7: derivations.tex, line 83, column 7
- Occurrence 8: soundness.tex, line 88, column 14
- Occurrence 9: soundness.tex, line 108, column 12
- Occurrence 10: soundness.tex, line 165, column 12
- Occurrence 11: soundness.tex, line 273, column 12
- Occurrence 12: soundness.tex, line 293, column 12
- Occurrence 13: soundness.tex, line 302, column 54
- Occurrence 14: soundness.tex, line 312, column 12
Expression 231
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of capital Xi
Meaning here: The relation read 'formula C is a member of capital Xi' concerns the exact premise sets or formula sequences named by the source.
4 occurrences
- Occurrence 1: soundness.tex, line 101, column 15
- Occurrence 2: soundness.tex, line 102, column 8
- Occurrence 3: soundness.tex, line 125, column 45
- Occurrence 4: soundness.tex, line 153, column 50
Expression 232
Inline MathML variant
Block MathML variant
Conventional reading: capital Xi equals first capital Delta, then the disjunction of formula A and formula B
Meaning here: The metalevel equality read 'capital Xi equals first capital Delta, then the disjunction of formula A and formula B' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: soundness.tex, line 169, column 29
Expression 233
Inline MathML variant
Block MathML variant
Conventional reading: the union of Gamma, and the set containing the negation of formula A
Meaning here: The relation read 'the union of Gamma, and the set containing the negation of formula A' concerns the exact premise sets or formula sequences named by the source.
4 occurrences
- Occurrence 1: provability-consistency.tex, line 47, column 25
- Occurrence 2: provability-consistency.tex, line 54, column 24
- Occurrence 3: provability-consistency.tex, line 56, column 4
- Occurrence 4: provability-consistency.tex, line 101, column 31
Expression 234
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives formula A
Meaning here: The statement read 'Gamma syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 135, column 30
Expression 235
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the disjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first the disjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: propositional-rules.tex, line 57, column 11
Expression 236
Inline MathML variant
Block MathML variant
Conventional reading: formula A is a member of capital Delta
Meaning here: The relation read 'formula A is a member of capital Delta' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 46, column 47
Expression 237
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma sub zero, then the negation of formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first Gamma sub zero, then the negation of formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 94, column 15
Expression 238
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma sub one, then formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first Gamma sub one, then formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 28, column 53
Expression 239
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero is a subset of Gamma
Meaning here: The relation read 'Gamma sub zero is a subset of Gamma' concerns the exact premise sets or formula sequences named by the source.
16 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 39, column 15
- Occurrence 2: proof-theoretic-notions.tex, line 71, column 15
- Occurrence 3: proof-theoretic-notions.tex, line 73, column 41
- Occurrence 4: proof-theoretic-notions.tex, line 95, column 54
- Occurrence 5: proof-theoretic-notions.tex, line 109, column 43
- Occurrence 6: proof-theoretic-notions.tex, line 150, column 62
- Occurrence 7: proof-theoretic-notions.tex, line 160, column 7
- Occurrence 8: proof-theoretic-notions.tex, line 164, column 14
- Occurrence 9: provability-consistency.tex, line 41, column 7
- Occurrence 10: provability-consistency.tex, line 96, column 35
- Occurrence 11: provability-consistency.tex, line 106, column 23
- Occurrence 12: provability-consistency.tex, line 122, column 7
- Occurrence 13: provability-quantifiers.tex, line 26, column 17
- Occurrence 14: soundness.tex, line 357, column 52
- Occurrence 15: soundness.tex, line 373, column 24
- Occurrence 16: soundness.tex, line 378, column 51
Expression 240
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 51, column 51
Expression 241
Inline MathML variant
Block MathML variant
Conventional reading: for every variable x, formula A with argument variable x syntactically derives formula A with argument term t
Meaning here: The statement read 'for every variable x, formula A with argument variable x syntactically derives formula A with argument term t' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 36, column 18
Expression 242
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first for some variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first for some variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 39, column 10
Expression 243
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 79, column 16
Expression 244
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 324, column 7
Expression 245
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 116, column 60
Expression 246
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then atomic formula P applied to term t, then term t
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then atomic formula P applied to term t, then term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 68, column 39
Expression 247
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives formula B
Meaning here: The statement read 'Gamma syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 129, column 19
- Occurrence 2: proof-theoretic-notions.tex, line 131, column 1
Expression 248
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first Gamma sub zero, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 120, column 11
Expression 249
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub one
Meaning here: The first-order sequent read 'antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub one' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 24, column 4
Expression 250
Inline MathML variant
Block MathML variant
Conventional reading: Gamma semantically entails formula A
Meaning here: The statement read 'Gamma semantically entails formula A' is first-order semantic consequence over the named structures and assignments.
1 occurrence
- Occurrence 1: soundness.tex, line 353, column 29
Expression 251
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 193, column 10
- Occurrence 2: provability-consistency.tex, line 90, column 14
- Occurrence 3: provability-propositional.tex, line 72, column 16
- Occurrence 4: provability-propositional.tex, line 121, column 18
Expression 252
Inline MathML variant
Block MathML variant
Conventional reading: the negation of formula A is a member of capital Theta
Meaning here: The relation read 'the negation of formula A is a member of capital Theta' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 127, column 55
Expression 253
Inline MathML variant
Block MathML variant
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 metalevel equality read 'Gamma equals the finite sequence first formula A sub one, continuing through the omitted intermediate entries, and finally formula A sub m' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 31, column 30
Expression 254
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 313, column 7
Expression 255
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 74, column 16
Expression 256
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 18, column 10
Expression 257
Inline MathML variant
Block MathML variant
Conventional reading: structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub one
Meaning here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula A with argument term t sub one' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 35, column 1
Expression 258
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies Gamma
Meaning here: The satisfaction claim read 'structure M satisfies Gamma' is evaluated in the named first-order structure and, when printed, the named variable assignment.
3 occurrences
- Occurrence 1: soundness.tex, line 362, column 4
- Occurrence 2: soundness-identity.tex, line 27, column 46
- Occurrence 3: soundness-identity.tex, line 31, column 30
Expression 259
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing term t sub one is identical to term t sub one
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing term t sub one is identical to term t sub one' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 49, column 7
Expression 260
Inline MathML variant
Block MathML variant
Conventional reading: first Gamma, then formula A
Meaning here: The sequence read 'first Gamma, then formula A' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 46, column 54
Expression 261
Inline MathML variant
Block MathML variant
Conventional reading: first formula A, then formula B syntactically derives the conjunction of formula A and formula B
Meaning here: The statement read 'first formula A, then formula B syntactically derives the conjunction of formula A and formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 30, column 47
Expression 262
Inline MathML variant
Block MathML variant
Conventional reading: the disjunction of formula A and formula B
Meaning here: The first-order formula read 'the disjunction of formula A and formula B' preserves its metavariables, connectives, term arguments, and written grouping.
2 occurrences
- Occurrence 1: soundness.tex, line 160, column 68
- Occurrence 2: soundness.tex, line 182, column 51
Expression 263
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime satisfies formula A with argument constant a
Meaning here: The satisfaction claim read 'structure M prime satisfies formula A with argument constant a' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 257, column 3
Expression 264
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub one
Meaning here: The first-order sequent read 'antecedent containing first term t sub one is identical to term t sub two, then Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t sub one' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: identity.tex, line 23, column 7
- Occurrence 2: identity.tex, line 30, column 10
Expression 265
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 75, column 10
Expression 266
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 41, column 35
Expression 267
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of capital Delta
Meaning here: The relation read 'formula C is a member of capital Delta' concerns the exact premise sets or formula sequences named by the source.
16 occurrences
- Occurrence 1: soundness.tex, line 94, column 59
- Occurrence 2: soundness.tex, line 100, column 63
- Occurrence 3: soundness.tex, line 117, column 59
- Occurrence 4: soundness.tex, line 124, column 32
- Occurrence 5: soundness.tex, line 147, column 53
- Occurrence 6: soundness.tex, line 152, column 50
- Occurrence 7: soundness.tex, line 174, column 53
- Occurrence 8: soundness.tex, line 177, column 66
- Occurrence 9: soundness.tex, line 198, column 53
- Occurrence 10: soundness.tex, line 203, column 8
- Occurrence 11: soundness.tex, line 220, column 30
- Occurrence 12: soundness.tex, line 242, column 8
- Occurrence 13: soundness.tex, line 246, column 39
- Occurrence 14: soundness.tex, line 256, column 3
- Occurrence 15: soundness-identity.tex, line 28, column 31
- Occurrence 16: soundness-identity.tex, line 31, column 68
Expression 268
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, and finally formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, and finally formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: structural-rules.tex, line 45, column 7
Expression 269
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 105, column 3
Expression 270
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, formula A with argument variable x; sequent arrow; succedent containing for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 92, column 12
- Occurrence 2: quantifier-rules.tex, line 99, column 12
Expression 271
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: rules-and-proofs.tex, line 56, column 11
- Occurrence 2: proving-things.tex, line 37, column 64
- Occurrence 3: proving-things.tex, line 38, column 48
- Occurrence 4: proof-theoretic-notions.tex, line 84, column 21
- Occurrence 5: soundness.tex, line 62, column 40
Expression 272
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing capital Pi; sequent arrow; succedent containing capital Lambda
Meaning here: The first-order sequent read 'antecedent containing capital Pi; sequent arrow; succedent containing capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 325, column 15
Expression 273
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing the negation of the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing the negation of the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 306, column 7
Expression 274
Inline MathML variant
Block MathML variant
Conventional reading: formula A is a member of Gamma
Meaning here: The relation read 'formula A is a member of Gamma' concerns the exact premise sets or formula sequences named by the source.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 80, column 4
- Occurrence 2: soundness.tex, line 45, column 49
Expression 275
Inline MathML variant
Block MathML variant
Conventional reading: formula B is a member of Gamma sub zero
Meaning here: The relation read 'formula B is a member of Gamma sub zero' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 361, column 19
Expression 276
Inline MathML variant
Block MathML variant
Conventional reading: the union of Gamma sub zero, and Gamma sub one is a subset of Gamma
Meaning here: The relation read 'the union of Gamma sub zero, and Gamma sub one is a subset of Gamma' concerns the exact premise sets or formula sequences named by the source.
2 occurrences
- Occurrence 1: provability-consistency.tex, line 42, column 1
- Occurrence 2: provability-consistency.tex, line 123, column 1
Expression 277
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy formula B
Meaning here: The satisfaction claim read 'structure M does not satisfy formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 328, column 3
Expression 278
Inline MathML variant
Block MathML variant
Conventional reading: the conditional whose antecedent is open parenthesis, the conjunction beginning with formula A sub one, continuing through the omitted intermediate conjunctions, and ending with formula A sub m, close parenthesis; and whose consequent is open parenthesis, the disjunction beginning with formula B sub one, continuing through the omitted intermediate disjunctions, and ending with formula B sub n, close parenthesis
Meaning here: The first-order formula read 'the conditional whose antecedent is open parenthesis, the conjunction beginning with formula A sub one, continuing through the omitted intermediate conjunctions, and ending with formula A sub m, close parenthesis; and whose consequent is open parenthesis, the disjunction beginning with formula B sub one, continuing through the omitted intermediate disjunctions, and ending with formula B sub n, close parenthesis' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 34, column 1
Expression 279
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis; sequent arrow; succedent containing for some variable x, open parenthesis, the conjunction whose first conjunct is formula A with argument variable x; and whose second conjunct states that for every variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent states that variable y is identical to variable x, close parenthesis, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing the conjunction whose first conjunct is for some variable x, formula A with argument variable x; and whose second conjunct states that for every variable y, for every variable z, open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A with argument variable y and formula A with argument variable z, close parenthesis; and whose consequent states that variable y is identical to variable z, close parenthesis; sequent arrow; succedent containing for some variable x, open parenthesis, the conjunction whose first conjunct is formula A with argument variable x; and whose second conjunct states that for every variable y, open parenthesis, the conditional whose antecedent is formula A with argument variable y; and whose consequent states that variable y is identical to variable x, close parenthesis, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 71, column 7
Expression 280
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first term t sub one is identical to term t sub two, then term t sub two is identical to term t sub three; sequent arrow; succedent containing term t sub one is identical to term t sub three
Meaning here: The first-order sequent read 'antecedent containing first term t sub one is identical to term t sub two, then term t sub two is identical to term t sub three; sequent arrow; succedent containing term t sub one is identical to term t sub three' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 61, column 10
Expression 281
Inline MathML variant
Block MathML variant
Conventional reading: term t sub one
Meaning here: The symbol read 'term t sub one' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
1 occurrence
- Occurrence 1: identity.tex, line 20, column 26
Expression 282
Inline MathML variant
Block MathML variant
Conventional reading: the conjunction of formula A and formula B
Meaning here: The first-order formula read 'the conjunction of formula A and formula B' preserves its metavariables, connectives, term arguments, and written grouping.
3 occurrences
- Occurrence 1: soundness.tex, line 132, column 68
- Occurrence 2: soundness.tex, line 149, column 37
- Occurrence 3: soundness.tex, line 157, column 65
Expression 283
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 115, column 10
Expression 284
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable z, open parenthesis, the conjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable z, open parenthesis, the conjunction of formula A with argument variable z and formula B with argument variable z, close parenthesis' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 88, column 7
Expression 285
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 94, column 16
Expression 286
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies term t sub one is identical to term t sub two
Meaning here: The satisfaction claim read 'structure M satisfies term t sub one is identical to term t sub two' is evaluated in the named first-order structure and, when printed, the named variable assignment.
3 occurrences
- Occurrence 1: soundness-identity.tex, line 27, column 17
- Occurrence 2: soundness-identity.tex, line 31, column 1
- Occurrence 3: soundness-identity.tex, line 37, column 1
Expression 287
Inline MathML variant
Block MathML variant
Conventional reading: structure M, under variable assignment lowercase s, satisfies formula A with argument variable x
Meaning here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula A with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.
4 occurrences
- Occurrence 1: soundness.tex, line 250, column 3
- Occurrence 2: soundness.tex, line 262, column 42
- Occurrence 3: soundness.tex, line 264, column 3
- Occurrence 4: soundness-identity.tex, line 36, column 38
Expression 288
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing for some variable x, the negation of formula A with argument variable x; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 14, column 50
Expression 289
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant b
Meaning here: The first-order sequent read 'antecedent containing formula A with argument constant a; sequent arrow; succedent containing formula A with argument constant b' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things-quant.tex, line 28, column 28
Expression 290
Inline MathML variant
Block MathML variant
Conventional reading: the set containing formula A is a subset of Gamma
Meaning here: The relation read 'the set containing formula A is a subset of Gamma' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 84, column 60
Expression 291
Inline MathML variant
Block MathML variant
Conventional reading: no premises does not syntactically derive formula A
Meaning here: The statement read 'no premises does not syntactically derive formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 33, column 30
Expression 292
Inline MathML variant
Block MathML variant
Conventional reading: the negation of formula A
Meaning here: The first-order formula read 'the negation of formula A' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: proving-things.tex, line 283, column 62
Expression 293
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: soundness.tex, line 77, column 26
- Occurrence 2: soundness.tex, line 104, column 21
- Occurrence 3: soundness.tex, line 114, column 42
- Occurrence 4: soundness.tex, line 171, column 9
- Occurrence 5: soundness.tex, line 325, column 46
Expression 294
Inline MathML variant
Block MathML variant
Conventional reading: no premises syntactically derives formula A
Meaning here: The statement read 'no premises syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 32, column 61
- Occurrence 2: soundness.tex, line 348, column 4
Expression 295
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then formula A; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first formula B, then formula A; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 83, column 10
- Occurrence 2: proving-things.tex, line 101, column 10
- Occurrence 3: proving-things.tex, line 122, column 10
- Occurrence 4: proving-things.tex, line 144, column 10
Expression 296
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
4 occurrences
- Occurrence 1: proving-things.tex, line 81, column 10
- Occurrence 2: proving-things.tex, line 96, column 10
- Occurrence 3: proving-things.tex, line 117, column 10
- Occurrence 4: proving-things.tex, line 139, column 10
Expression 297
Inline MathML variant
Block MathML variant
Conventional reading: capital Theta equals Gamma
Meaning here: The metalevel equality read 'capital Theta equals Gamma' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: soundness.tex, line 169, column 7
Expression 298
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda
Meaning here: The first-order sequent read 'antecedent containing first Gamma, then capital Pi; sequent arrow; succedent containing first capital Delta, then capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 277, column 15
Expression 299
Inline MathML variant
Block MathML variant
Conventional reading: the negation of formula A syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B
Meaning here: The statement read 'the negation of formula A syntactically derives the conditional whose antecedent is formula A; and whose consequent is formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 103, column 10
Expression 300
Inline MathML variant
Block MathML variant
Conventional reading: constant a
Meaning here: The symbol read 'constant a' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
14 occurrences
- Occurrence 1: quantifier-rules.tex, line 28, column 35
- Occurrence 2: quantifier-rules.tex, line 30, column 6
- Occurrence 3: quantifier-rules.tex, line 31, column 67
- Occurrence 4: quantifier-rules.tex, line 48, column 34
- Occurrence 5: quantifier-rules.tex, line 49, column 66
- Occurrence 6: quantifier-rules.tex, line 74, column 14
- Occurrence 7: quantifier-rules.tex, line 83, column 14
- Occurrence 8: proving-things-quant.tex, line 26, column 26
- Occurrence 9: proving-things-quant.tex, line 62, column 67
- Occurrence 10: proving-things-quant.tex, line 80, column 68
- Occurrence 11: soundness.tex, line 229, column 42
- Occurrence 12: soundness.tex, line 236, column 57
- Occurrence 13: soundness.tex, line 255, column 24
- Occurrence 14: soundness.tex, line 261, column 38
Expression 301
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives formula A
Meaning here: The statement read 'Gamma syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
16 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 38, column 25
- Occurrence 2: proof-theoretic-notions.tex, line 80, column 26
- Occurrence 3: proof-theoretic-notions.tex, line 90, column 34
- Occurrence 4: proof-theoretic-notions.tex, line 95, column 9
- Occurrence 5: proof-theoretic-notions.tex, line 104, column 4
- Occurrence 6: proof-theoretic-notions.tex, line 109, column 4
- Occurrence 7: proof-theoretic-notions.tex, line 128, column 44
- Occurrence 8: proof-theoretic-notions.tex, line 150, column 12
- Occurrence 9: proof-theoretic-notions.tex, line 159, column 14
- Occurrence 10: provability-consistency.tex, line 20, column 6
- Occurrence 11: provability-consistency.tex, line 47, column 1
- Occurrence 12: provability-consistency.tex, line 51, column 15
- Occurrence 13: provability-consistency.tex, line 76, column 6
- Occurrence 14: provability-consistency.tex, line 81, column 11
- Occurrence 15: soundness.tex, line 353, column 4
- Occurrence 16: soundness.tex, line 357, column 4
Expression 302
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 321, column 7
Expression 303
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero syntactically derives formula A
Meaning here: The statement read 'Gamma sub zero syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 151, column 33
- Occurrence 2: proof-theoretic-notions.tex, line 161, column 55
Expression 304
Inline MathML variant
Block MathML variant
Conventional reading: the disjunction of formula A and the negation of formula A
Meaning here: The first-order formula read 'the disjunction of formula A and the negation of formula A' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: proving-things.tex, line 273, column 55
Expression 305
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 108, column 38
Expression 306
Inline MathML variant
Block MathML variant
Conventional reading: right contraction rule
Meaning here: The rule label read 'right contraction rule' names the exact side and logical or structural operator printed by the source.
2 occurrences
- Occurrence 1: proving-things.tex, line 340, column 24
- Occurrence 2: proving-things-quant.tex, line 107, column 24
Expression 307
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies term t is identical to term t
Meaning here: The satisfaction claim read 'structure M satisfies term t is identical to term t' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 19, column 38
Expression 308
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, atomic formula P applied to term t, then variable x
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then for some variable x, atomic formula P applied to term t, then variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 67, column 42
Expression 309
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 319, column 7
Expression 310
Inline MathML variant
Block MathML variant
Conventional reading: the conjunction of formula A and formula B syntactically derives formula A
Meaning here: The statement read 'the conjunction of formula A and formula B syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: provability-propositional.tex, line 21, column 57
- Occurrence 2: provability-propositional.tex, line 28, column 51
Expression 311
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime
Meaning here: The expression read 'structure M prime' denotes the named first-order structure.
2 occurrences
- Occurrence 1: soundness.tex, line 252, column 13
- Occurrence 2: soundness.tex, line 259, column 55
Expression 312
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 133, column 18
Expression 313
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 314, column 7
Expression 314
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: propositional-rules.tex, line 35, column 10
- Occurrence 2: propositional-rules.tex, line 40, column 10
- Occurrence 3: soundness.tex, line 139, column 14
Expression 315
Inline MathML variant
Block MathML variant
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
- Occurrence 1: proof-theoretic-notions.tex, line 40, column 25
- Occurrence 2: proof-theoretic-notions.tex, line 52, column 4
- Occurrence 3: proof-theoretic-notions.tex, line 64, column 31
- Occurrence 4: proof-theoretic-notions.tex, line 66, column 46
- Occurrence 5: proof-theoretic-notions.tex, line 97, column 54
- Occurrence 6: proof-theoretic-notions.tex, line 165, column 55
- Occurrence 7: provability-consistency.tex, line 25, column 18
Expression 316
Inline MathML variant
Block MathML variant
Conventional reading: conditional
Meaning here: The logical notation read 'conditional' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
3 occurrences
- Occurrence 1: propositional-rules.tex, line 73, column 23
- Occurrence 2: proving-things.tex, line 61, column 1
- Occurrence 3: proving-things.tex, line 61, column 53
Expression 317
Inline MathML variant
Block MathML variant
Conventional reading: formula B
Meaning here: The first-order formula read 'formula B' preserves its metavariables, connectives, term arguments, and written grouping.
11 occurrences
- Occurrence 1: rules-and-proofs.tex, line 69, column 56
- Occurrence 2: derivations.tex, line 73, column 10
- Occurrence 3: derivations.tex, line 90, column 47
- Occurrence 4: derivations.tex, line 106, column 19
- Occurrence 5: proving-things.tex, line 180, column 21
- Occurrence 6: soundness.tex, line 133, column 59
- Occurrence 7: soundness.tex, line 158, column 30
- Occurrence 8: soundness.tex, line 159, column 6
- Occurrence 9: soundness.tex, line 161, column 59
- Occurrence 10: soundness.tex, line 183, column 17
- Occurrence 11: soundness.tex, line 183, column 60
Expression 318
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing no formulas; sequent arrow; succedent containing the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing no formulas; sequent arrow; succedent containing the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 266, column 10
Expression 319
Inline MathML variant
Block MathML variant
Conventional reading: the value of term t sub one in structure M is identical to the value of term t sub two in structure M
Meaning here: The semantic term read 'the value of term t sub one in structure M is identical to the value of term t sub two in structure M' specifies an interpretation, term value, or assignment relation in a first-order structure.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 37, column 35
Expression 320
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 290, column 10
Expression 321
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of Gamma
Meaning here: The relation read 'formula C is a member of Gamma' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 197, column 51
Expression 322
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: soundness.tex, line 76, column 13
- Occurrence 2: soundness.tex, line 144, column 3
Expression 323
Inline MathML variant
Block MathML variant
Conventional reading: right disjunction rule
Meaning here: The rule label read 'right disjunction rule' names the exact side and logical or structural operator printed by the source.
2 occurrences
- Occurrence 1: proving-things.tex, line 255, column 51
- Occurrence 2: proving-things.tex, line 283, column 18
Expression 324
Inline MathML variant
Block MathML variant
Conventional reading: capital Delta syntactically derives formula A
Meaning here: The statement read 'capital Delta syntactically derives formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
2 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 90, column 60
- Occurrence 2: proof-theoretic-notions.tex, line 99, column 30
Expression 325
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula B, then formula B; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula B, then formula B; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 77, column 16
Expression 326
Inline MathML variant
Block MathML variant
Conventional reading: formula A syntactically derives the disjunction of formula A and formula B
Meaning here: The statement read 'formula A syntactically derives the disjunction of formula A and formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 61, column 14
Expression 327
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 323, column 7
Expression 328
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 180, column 3
Expression 329
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 114, column 19
Expression 330
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 37, column 53
Expression 331
Inline MathML variant
Block MathML variant
Conventional reading: the disjunction beginning with formula B sub one, continuing through the omitted intermediate disjunctions, and ending with formula B sub n
Meaning here: The first-order formula read 'the disjunction beginning with formula B sub one, continuing through the omitted intermediate disjunctions, and ending with formula B sub n' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 40, column 28
Expression 332
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub zero double prime
Meaning here: Gamma sub zero double prime denotes the next reordered antecedent sequence in that construction.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 48, column 34
Expression 333
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 264, column 10
Expression 334
Inline MathML variant
Block MathML variant
Conventional reading: structure M does not satisfy for every variable x, formula A with argument variable x
Meaning here: The satisfaction claim read 'structure M does not satisfy for every variable x, formula A with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 223, column 22
Expression 335
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies formula A
Meaning here: The satisfaction claim read 'structure M satisfies formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.
9 occurrences
- Occurrence 1: soundness.tex, line 46, column 1
- Occurrence 2: soundness.tex, line 65, column 1
- Occurrence 3: soundness.tex, line 119, column 3
- Occurrence 4: soundness.tex, line 126, column 21
- Occurrence 5: soundness.tex, line 172, column 3
- Occurrence 6: soundness.tex, line 283, column 11
- Occurrence 7: soundness.tex, line 304, column 3
- Occurrence 8: soundness.tex, line 326, column 25
- Occurrence 9: soundness.tex, line 363, column 1
Expression 336
Inline MathML variant
Block MathML variant
Conventional reading: i
Meaning here: The index i selects a formula from a finite indexed family.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 130, column 60
Expression 337
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
8 occurrences
- Occurrence 1: rules-and-proofs.tex, line 20, column 1
- Occurrence 2: rules-and-proofs.tex, line 32, column 44
- Occurrence 3: soundness.tex, line 44, column 1
- Occurrence 4: soundness.tex, line 90, column 28
- Occurrence 5: soundness.tex, line 157, column 14
- Occurrence 6: soundness.tex, line 285, column 28
- Occurrence 7: soundness.tex, line 301, column 54
- Occurrence 8: soundness.tex, line 324, column 55
Expression 338
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 200, column 11
Expression 339
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 336, column 7
Expression 340
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula B; sequent arrow; succedent containing formula B
Meaning here: The first-order sequent read 'antecedent containing formula B; sequent arrow; succedent containing formula B' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
10 occurrences
- Occurrence 1: proving-things.tex, line 97, column 7
- Occurrence 2: proving-things.tex, line 118, column 7
- Occurrence 3: proving-things.tex, line 140, column 7
- Occurrence 4: proving-things.tex, line 235, column 7
- Occurrence 5: provability-propositional.tex, line 44, column 13
- Occurrence 6: provability-propositional.tex, line 51, column 13
- Occurrence 7: provability-propositional.tex, line 75, column 13
- Occurrence 8: provability-propositional.tex, line 92, column 13
- Occurrence 9: provability-propositional.tex, line 112, column 15
- Occurrence 10: provability-propositional.tex, line 129, column 15
Expression 341
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first formula A, then Gamma sub one; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 36, column 8
Expression 342
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 334, column 7
Expression 343
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument lowercase s
Meaning here: The first-order sequent read 'antecedent containing formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument lowercase s' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 38, column 7
Expression 344
Inline MathML variant
Block MathML variant
Conventional reading: Gamma sub one is a subset of Gamma
Meaning here: The relation read 'Gamma sub one is a subset of Gamma' concerns the exact premise sets or formula sequences named by the source.
4 occurrences
- Occurrence 1: provability-consistency.tex, line 25, column 33
- Occurrence 2: provability-consistency.tex, line 41, column 39
- Occurrence 3: provability-consistency.tex, line 106, column 55
- Occurrence 4: provability-consistency.tex, line 122, column 39
Expression 345
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula A, then formula A, and finally Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula A, then formula A, and finally Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: structural-rules.tex, line 40, column 7
Expression 346
Inline MathML variant
Block MathML variant
Conventional reading: first formula C, then formula D
Meaning here: The sequence read 'first formula C, then formula D' preserves the formula order and any printed empty or trailing position.
1 occurrence
- Occurrence 1: derivations.tex, line 90, column 1
Expression 347
Inline MathML variant
Block MathML variant
Conventional reading: capital Delta sub zero is a subset of capital Delta
Meaning here: The relation read 'capital Delta sub zero is a subset of capital Delta' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 111, column 54
Expression 348
Inline MathML variant
Block MathML variant
Conventional reading: structure M prime does not satisfy formula C
Meaning here: The satisfaction claim read 'structure M prime does not satisfy formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 256, column 20
Expression 349
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 81, column 17
Expression 350
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 231, column 10
- Occurrence 2: provability-propositional.tex, line 42, column 16
Expression 351
Inline MathML variant
Block MathML variant
Conventional reading: s applied to variable x is identical to the value of term t sub two in structure M
Meaning here: The semantic term read 's applied to variable x is identical to the value of term t sub two in structure M' specifies an interpretation, term value, or assignment relation in a first-order structure.
1 occurrence
- Occurrence 1: soundness-identity.tex, line 38, column 11
Expression 352
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 67, column 48
Expression 353
Inline MathML variant
Block MathML variant
Conventional reading: term t
Meaning here: The symbol read 'term t' receives its exact term, variable, constant, or assignment role from each bound source occurrence.
9 occurrences
- Occurrence 1: quantifier-rules.tex, line 27, column 22
- Occurrence 2: quantifier-rules.tex, line 48, column 8
- Occurrence 3: quantifier-rules.tex, line 66, column 11
- Occurrence 4: quantifier-rules.tex, line 71, column 33
- Occurrence 5: quantifier-rules.tex, line 81, column 10
- Occurrence 6: soundness.tex, line 209, column 42
- Occurrence 7: identity.tex, line 17, column 4
- Occurrence 8: identity.tex, line 35, column 12
- Occurrence 9: soundness-identity.tex, line 20, column 20
Expression 354
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-consistency.tex, line 65, column 10
Expression 355
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula B, then formula A, and finally capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: structural-rules.tex, line 61, column 10
Expression 356
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula A; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing formula A; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
12 occurrences
- Occurrence 1: proving-things.tex, line 42, column 7
- Occurrence 2: proving-things.tex, line 133, column 7
- Occurrence 3: proving-things.tex, line 191, column 7
- Occurrence 4: proving-things.tex, line 286, column 7
- Occurrence 5: provability-consistency.tex, line 60, column 9
- Occurrence 6: provability-consistency.tex, line 88, column 11
- Occurrence 7: provability-propositional.tex, line 40, column 13
- Occurrence 8: provability-propositional.tex, line 50, column 13
- Occurrence 9: provability-propositional.tex, line 70, column 13
- Occurrence 10: provability-propositional.tex, line 88, column 13
- Occurrence 11: provability-propositional.tex, line 111, column 15
- Occurrence 12: provability-propositional.tex, line 119, column 15
Expression 357
Inline MathML variant
Block MathML variant
Conventional reading: Gamma syntactically derives for every variable x, formula A with argument variable x
Meaning here: The statement read 'Gamma syntactically derives for every variable x, formula A with argument variable x' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-quantifiers.tex, line 20, column 57
Expression 358
Inline MathML variant
Block MathML variant
Conventional reading: formula A with argument term t
Meaning here: The first-order formula read 'formula A with argument term t' preserves its metavariables, connectives, term arguments, and written grouping.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 59, column 15
Expression 359
Inline MathML variant
Block MathML variant
Conventional reading: formula C is a member of capital Theta
Meaning here: The relation read 'formula C is a member of capital Theta' concerns the exact premise sets or formula sequences named by the source.
6 occurrences
- Occurrence 1: soundness.tex, line 98, column 8
- Occurrence 2: soundness.tex, line 99, column 51
- Occurrence 3: soundness.tex, line 123, column 47
- Occurrence 4: soundness.tex, line 128, column 21
- Occurrence 5: soundness.tex, line 149, column 12
- Occurrence 6: soundness.tex, line 152, column 3
Expression 360
Inline MathML variant
Block MathML variant
Conventional reading: the union of Gamma, and the set containing formula A
Meaning here: The relation read 'the union of Gamma, and the set containing formula A' concerns the exact premise sets or formula sequences named by the source.
3 occurrences
- Occurrence 1: provability-consistency.tex, line 20, column 30
- Occurrence 2: provability-consistency.tex, line 72, column 42
- Occurrence 3: provability-consistency.tex, line 101, column 6
Expression 361
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda
Meaning here: The first-order sequent read 'antecedent containing first formula B, then capital Pi; sequent arrow; succedent containing capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 327, column 3
Expression 362
Inline MathML variant
Block MathML variant
Conventional reading: structure M satisfies the conjunction of formula A and formula B
Meaning here: The satisfaction claim read 'structure M satisfies the conjunction of formula A and formula B' is evaluated in the named first-order structure and, when printed, the named variable assignment.
1 occurrence
- Occurrence 1: soundness.tex, line 307, column 3
Expression 363
Inline MathML variant
Block MathML variant
Conventional reading: capital Theta equals first the negation of formula A, then Gamma
Meaning here: The metalevel equality read 'capital Theta equals first the negation of formula A, then Gamma' identifies the exact derivation count, sequence, premise family, or semantic quantity named on its two sides.
1 occurrence
- Occurrence 1: soundness.tex, line 112, column 7
Expression 364
Inline MathML variant
Block MathML variant
Conventional reading: capital Pi set difference capital Lambda
Meaning here: The relation read 'capital Pi set difference capital Lambda' concerns the exact premise sets or formula sequences named by the source.
1 occurrence
- Occurrence 1: soundness.tex, line 288, column 28
Expression 365
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 109, column 23
Expression 366
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
6 occurrences
- Occurrence 1: proving-things.tex, line 57, column 10
- Occurrence 2: proving-things.tex, line 73, column 37
- Occurrence 3: proving-things.tex, line 89, column 10
- Occurrence 4: proving-things.tex, line 107, column 10
- Occurrence 5: proving-things.tex, line 128, column 10
- Occurrence 6: proving-things.tex, line 150, column 10
Expression 367
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 304, column 7
Expression 368
Inline MathML variant
Block MathML variant
Conventional reading: language L
Meaning here: The first-order language L in which the displayed sentences are formed.
1 occurrence
- Occurrence 1: rules-and-proofs.tex, line 24, column 31
Expression 369
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proving-things.tex, line 335, column 7
Expression 370
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first for every variable x, formula A with argument variable x, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: soundness.tex, line 216, column 39
- Occurrence 2: soundness.tex, line 224, column 36
- Occurrence 3: soundness.tex, line 226, column 3
Expression 371
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing formula C; sequent arrow; succedent containing formula C
Meaning here: The first-order sequent read 'antecedent containing formula C; sequent arrow; succedent containing formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: derivations.tex, line 38, column 30
- Occurrence 2: derivations.tex, line 48, column 29
Expression 372
Inline MathML variant
Block MathML variant
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.
10 occurrences
- Occurrence 1: rules-and-proofs.tex, line 23, column 20
- Occurrence 2: rules-and-proofs.tex, line 25, column 26
- Occurrence 3: rules-and-proofs.tex, line 39, column 1
- Occurrence 4: rules-and-proofs.tex, line 41, column 1
- Occurrence 5: rules-and-proofs.tex, line 49, column 18
- Occurrence 6: derivations.tex, line 49, column 14
- Occurrence 7: derivations.tex, line 72, column 37
- Occurrence 8: derivations.tex, line 90, column 11
- Occurrence 9: proof-theoretic-notions.tex, line 98, column 25
- Occurrence 10: soundness.tex, line 237, column 34
Expression 373
Inline MathML variant
Block MathML variant
Conventional reading: pi
Meaning here: Pi denotes the sequent-calculus derivation currently under discussion.
13 occurrences
- Occurrence 1: provability-consistency.tex, line 82, column 22
- Occurrence 2: provability-consistency.tex, line 86, column 17
- Occurrence 3: soundness.tex, line 58, column 5
- Occurrence 4: soundness.tex, line 59, column 46
- Occurrence 5: soundness.tex, line 61, column 42
- Occurrence 6: soundness.tex, line 134, column 53
- Occurrence 7: soundness.tex, line 162, column 50
- Occurrence 8: soundness.tex, line 184, column 49
- Occurrence 9: soundness.tex, line 209, column 56
- Occurrence 10: soundness.tex, line 229, column 56
- Occurrence 11: soundness.tex, line 270, column 41
- Occurrence 12: soundness.tex, line 290, column 51
- Occurrence 13: soundness.tex, line 309, column 49
Expression 374
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the negation of formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the negation of formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: propositional-rules.tex, line 25, column 10
Expression 375
Inline MathML variant
Block MathML variant
Conventional reading: existential quantifier
Meaning here: The logical notation read 'existential quantifier' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 34, column 23
- Occurrence 2: proving-things-quant.tex, line 27, column 1
Expression 376
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: soundness.tex, line 155, column 34
Expression 377
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula C
Meaning here: The first-order sequent read 'antecedent containing first formula C, then formula D; sequent arrow; succedent containing formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
3 occurrences
- Occurrence 1: derivations.tex, line 64, column 10
- Occurrence 2: derivations.tex, line 98, column 10
- Occurrence 3: derivations.tex, line 115, column 10
Expression 378
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C
Meaning here: The first-order sequent read 'antecedent containing first formula D, then formula C; sequent arrow; succedent containing formula C' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: derivations.tex, line 50, column 1
Expression 379
Inline MathML variant
Block MathML variant
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 first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A, then formula B, and finally capital Lambda' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: structural-rules.tex, line 59, column 7
Expression 380
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
6 occurrences
- Occurrence 1: proving-things.tex, line 162, column 10
- Occurrence 2: proving-things.tex, line 173, column 10
- Occurrence 3: proving-things.tex, line 187, column 10
- Occurrence 4: proving-things.tex, line 206, column 10
- Occurrence 5: proving-things.tex, line 225, column 10
- Occurrence 6: proving-things.tex, line 246, column 10
Expression 381
Inline MathML variant
Block MathML variant
Conventional reading: formula A with argument constant a
Meaning here: The first-order formula read 'formula A with argument constant a' preserves its metavariables, connectives, term arguments, and written grouping.
2 occurrences
- Occurrence 1: quantifier-rules.tex, line 83, column 53
- Occurrence 2: soundness.tex, line 258, column 31
Expression 382
Inline MathML variant
Block MathML variant
Conventional reading: the conjunction of formula A and formula B syntactically derives formula B
Meaning here: The statement read 'the conjunction of formula A and formula B syntactically derives formula B' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: provability-propositional.tex, line 29, column 13
Expression 383
Inline MathML variant
Block MathML variant
Conventional reading: Gamma does not syntactically derive formula A
Meaning here: The statement read 'Gamma does not syntactically derive formula A' is first-order syntactic derivability in the L K sequent calculus, including the stated premises and formula scope.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 42, column 10
Expression 384
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then formula C; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing first formula B, then formula C; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: proof-theoretic-notions.tex, line 58, column 12
Expression 385
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first the negation of formula A with argument constant a, then for every variable x, formula A with argument variable x; sequent arrow; succedent containing no formulas
Meaning here: The first-order sequent read 'antecedent containing first the negation of formula A with argument constant a, then for every variable x, formula A with argument variable x; sequent arrow; succedent containing no formulas' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 51, column 10
- Occurrence 2: proving-things-quant.tex, line 69, column 10
Expression 386
Inline MathML variant
Block MathML variant
Conventional reading: formula D
Meaning here: The first-order formula read 'formula D' preserves its metavariables, connectives, term arguments, and written grouping.
4 occurrences
- Occurrence 1: derivations.tex, line 47, column 49
- Occurrence 2: derivations.tex, line 73, column 29
- Occurrence 3: derivations.tex, line 90, column 55
- Occurrence 4: derivations.tex, line 106, column 10
Expression 387
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A
Meaning here: The first-order sequent read 'antecedent containing Gamma sub zero; sequent arrow; succedent containing formula A' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
9 occurrences
- Occurrence 1: proof-theoretic-notions.tex, line 65, column 20
- Occurrence 2: proof-theoretic-notions.tex, line 96, column 29
- Occurrence 3: proof-theoretic-notions.tex, line 98, column 57
- Occurrence 4: proof-theoretic-notions.tex, line 110, column 32
- Occurrence 5: proof-theoretic-notions.tex, line 160, column 57
- Occurrence 6: provability-consistency.tex, line 26, column 24
- Occurrence 7: provability-consistency.tex, line 27, column 56
- Occurrence 8: provability-consistency.tex, line 82, column 41
- Occurrence 9: soundness.tex, line 358, column 38
Expression 388
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 84, column 10
- Occurrence 2: soundness.tex, line 189, column 14
Expression 389
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first formula B, then Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing first formula B, then Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: propositional-rules.tex, line 38, column 7
- Occurrence 2: propositional-rules.tex, line 55, column 7
Expression 390
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing capital Delta
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing capital Delta' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
5 occurrences
- Occurrence 1: structural-rules.tex, line 26, column 7
- Occurrence 2: structural-rules.tex, line 31, column 7
- Occurrence 3: derivations.tex, line 42, column 7
- Occurrence 4: soundness.tex, line 81, column 12
- Occurrence 5: soundness.tex, line 86, column 12
Expression 391
Inline MathML variant
Block MathML variant
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 first-order 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' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things.tex, line 183, column 10
- Occurrence 2: proving-things.tex, line 202, column 10
Expression 392
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing the negation of formula A with argument constant a; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x
Meaning here: The first-order sequent read 'antecedent containing the negation of formula A with argument constant a; sequent arrow; succedent containing the negation of for every variable x, formula A with argument variable x' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
2 occurrences
- Occurrence 1: proving-things-quant.tex, line 42, column 10
- Occurrence 2: proving-things-quant.tex, line 73, column 10
Expression 393
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing first lowercase s is identical to term t, then formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument lowercase s
Meaning here: The first-order sequent read 'antecedent containing first lowercase s is identical to term t, then formula A with argument lowercase s; sequent arrow; succedent containing formula A with argument lowercase s' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: identity.tex, line 40, column 10
Expression 394
Inline MathML variant
Block MathML variant
Conventional reading: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t
Meaning here: The first-order sequent read 'antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A with argument term t' preserves the ordered antecedent and succedent exactly. It is a syntactic sequent; validity is asserted only where the surrounding source says so.
1 occurrence
- Occurrence 1: quantifier-rules.tex, line 42, column 7