The Open Logic Text — accessible offline edition

The Completeness Theorem — Explore equations

The Completeness Theorem

Reading preferences

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

Equation and object guide

All 112 stable expression records, 20 reader formal objects plus one source-only formal, and 65 resolved references are indexed here. SAR-002 source closure remains explicit.

112 expression records

Expression 1

Γ∗\Gamma^*

Conventional reading: Gamma star

Meaning here: Gamma star is the complete extension constructed from the original premise set; in the Lindenbaum proof it is the union of all finite stages.

22 derived occurrences; 22 source occurrences
  1. Occurrence 1: outline.tex, line 73, column 23
  2. Occurrence 2: outline.tex, line 76, column 4
  3. Occurrence 3: outline.tex, line 80, column 47
  4. Occurrence 4: outline.tex, line 153, column 18
  5. Occurrence 5: outline.tex, line 154, column 1
  6. Occurrence 6: outline.tex, line 159, column 20
  7. Occurrence 7: complete-consistent-sets.tex, line 37, column 5
  8. Occurrence 8: complete-consistent-sets.tex, line 47, column 4
  9. Occurrence 9: complete-consistent-sets.tex, line 48, column 39
  10. Occurrence 10: lindenbaums-lemma.tex, line 30, column 46
  11. Occurrence 11: lindenbaums-lemma.tex, line 76, column 27
  12. Occurrence 12: lindenbaums-lemma.tex, line 90, column 48
  13. Occurrence 13: lindenbaums-lemma.tex, line 94, column 8
  14. Occurrence 14: lindenbaums-lemma.tex, line 96, column 19
  15. Occurrence 15: construction-of-model.tex, line 32, column 54
  16. Occurrence 16: construction-of-model.tex, line 65, column 9
  17. Occurrence 17: construction-of-model.tex, line 174, column 21
  18. Occurrence 18: construction-of-model.tex, line 198, column 33
  19. Occurrence 19: compactness-direct.tex, line 20, column 5
  20. Occurrence 20: compactness-direct.tex, line 23, column 18
  21. Occurrence 21: compactness-direct.tex, line 94, column 5
  22. Occurrence 22: compactness-direct.tex, line 132, column 26

Expression 3

ss

Conventional reading: s

Meaning here: s is a variable assignment used to evaluate a formula with a free variable in the first-order source branch.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 4

M(Γ∗)⊨∀xA(x)\Sat{M(\Gamma^*)}{\lforall[x][!A(x)]}

Conventional reading: structure M of Gamma star satisfies the formula for every x, A of x

Meaning here: In the first-order source branch, the satisfaction statement read 'structure M of Gamma star satisfies the formula for every x, A of x' asserts truth in term model M of Gamma star.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 5

v(Γ∗)⊭⊥\pSat/{v(\Gamma^*)}{\lfalse}

Conventional reading: valuation v of Gamma star does not satisfy falsum

Meaning here: The non-satisfaction statement read 'valuation v of Gamma star does not satisfy falsum' says that the named formula is false under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 172, column 4

Expression 6

M(Γ∗),s⊨A(t)\Sat{M(\Gamma^*)}{!A(t)}[s]

Conventional reading: structure M of Gamma star satisfies A of t under assignment s

Meaning here: In the first-order source branch, the satisfaction statement read 'structure M of Gamma star satisfies A of t under assignment s' asserts truth in term model M of Gamma star under assignment s.

0 derived occurrences; 2 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 7

Γn+1=Γn∪{¬An}\Gamma_{n+1} = \Gamma_n \cup \{\lnot !A_n\}

Conventional reading: Gamma sub n plus one equals Gamma sub n union the singleton set containing not A sub n

Meaning here: This is one branch of the recursive definition: successor stage Gamma sub n plus one is stage Gamma sub n with not A sub n adjoined.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 49, column 30

Expression 8

An∉Γ∗!A_n \notin \Gamma^*

Conventional reading: A sub n does not belong to Gamma star

Meaning here: The nonmembership statement read 'A sub n does not belong to Gamma star' says that the displayed formula is absent from the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 94, column 23

Expression 10

v(Γ∗)⊨Γ\pSat{v(\Gamma^*)}{\Gamma}

Conventional reading: valuation v of Gamma star satisfies every formula in Gamma

Meaning here: The canonical valuation determined by Gamma star makes every formula in the original set Gamma true.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 164, column 1

Expression 11

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

Conventional reading: valuation v does not satisfy B

Meaning here: The non-satisfaction statement read 'valuation v does not satisfy B' says that the named formula is false under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 57, column 1

Expression 12

Γn⊆Γn+1\Gamma_n \subseteq \Gamma_{n+1}

Conventional reading: Gamma sub n is a subset of Gamma sub n plus one

Meaning here: The inclusion read 'Gamma sub n is a subset of Gamma sub n plus one' states that every member of the left-hand stage or finite subset also belongs to the right-hand set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 70, column 51

Expression 14

∈Γn\in \Gamma_n

Conventional reading: belongs to Gamma sub n

Meaning here: This source fragment completes the claim that the carried-over formula B belongs to stage set Gamma sub n.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 80, column 6

Expression 15

M(Γ∗)\Struct M(\Gamma^*)

Conventional reading: term model M of Gamma star

Meaning here: This names the term model constructed from Gamma star in the first-order source branch.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 16

v\pAssign{v}

Conventional reading: valuation v

Meaning here: This names a propositional valuation; with Gamma star as argument it is the canonical valuation whose value at p is determined by whether p belongs to Gamma star.

9 derived occurrences; 9 source occurrences
  1. Occurrence 1: introduction.tex, line 30, column 57
  2. Occurrence 2: outline.tex, line 46, column 18
  3. Occurrence 3: outline.tex, line 51, column 1
  4. Occurrence 4: outline.tex, line 56, column 4
  5. Occurrence 5: outline.tex, line 74, column 73
  6. Occurrence 6: compactness.tex, line 46, column 57
  7. Occurrence 7: compactness.tex, line 48, column 27
  8. Occurrence 8: compactness-direct.tex, line 122, column 57
  9. Occurrence 9: compactness-direct.tex, line 124, column 43

Expression 19

(A→B)∈Γ(!A \lif !B) \in \Gamma

Conventional reading: the conditional from A to B belongs to Gamma

Meaning here: The membership statement read 'the conditional from A to B belongs to Gamma' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: compactness-direct.tex, line 41, column 17

Expression 21

B∈Γ!B \in \Gamma

Conventional reading: B belongs to Gamma

Meaning here: The membership statement read 'B belongs to Gamma' says that the complete displayed formula belongs to the named set.

9 derived occurrences; 9 source occurrences
  1. Occurrence 1: complete-consistent-sets.tex, line 68, column 32
  2. Occurrence 2: complete-consistent-sets.tex, line 71, column 29
  3. Occurrence 3: complete-consistent-sets.tex, line 74, column 32
  4. Occurrence 4: complete-consistent-sets.tex, line 136, column 12
  5. Occurrence 5: complete-consistent-sets.tex, line 149, column 16
  6. Occurrence 6: complete-consistent-sets.tex, line 151, column 60
  7. Occurrence 7: compactness-direct.tex, line 36, column 32
  8. Occurrence 8: compactness-direct.tex, line 39, column 29
  9. Occurrence 9: compactness-direct.tex, line 42, column 32

Expression 22

DM\Domain{M}

Conventional reading: domain of structure M

Meaning here: This names the domain of the displayed structure; when Gamma star occurs, it is the domain of the term model built from that complete set.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 25

v(Γ∗)⊨p\pSat{v(\Gamma^*)}{p}

Conventional reading: valuation v of Gamma star satisfies propositional variable p

Meaning here: The satisfaction statement read 'valuation v of Gamma star satisfies propositional variable p' says that the named formula, variable, or premise set is true under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 187, column 38

Expression 27

(A∧B)∈Γ(!A \land !B) \in \Gamma

Conventional reading: the conjunction of A and B belongs to Gamma

Meaning here: The membership statement read 'the conjunction of A and B belongs to Gamma' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: compactness-direct.tex, line 35, column 18

Expression 28

M\Struct{M}

Conventional reading: structure M

Meaning here: This names the arbitrary structure M used in the first-order source discussion.

0 derived occurrences; 3 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 29

v(Γ∗)(p)=⊤if p∈Γ∗⊥if p∉Γ∗\pAssign v(\Gamma^*)(p) = \begin{cases} \True & \text{if $p \in \Gamma^*$}\\ \False & \text{if $p \notin \Gamma^*$} \end{cases}

Conventional reading: valuation v of Gamma star assigns verum to p when p belongs to Gamma star, and assigns falsum to p otherwise

Meaning here: This defines the canonical valuation: it gives p the value verum exactly when p is in Gamma star, and falsum otherwise.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 66, column 1

Expression 31

¬A∈Γ∗\lnot !A \in \Gamma^*

Conventional reading: not A belongs to Gamma star

Meaning here: The membership statement read 'not A belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 50, column 1

Expression 32

Γ′⊆Γn\Gamma' \subseteq \Gamma_n

Conventional reading: Gamma prime is a subset of Gamma sub n

Meaning here: The inclusion read 'Gamma prime is a subset of Gamma sub n' states that every member of the left-hand stage or finite subset also belongs to the right-hand set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 80, column 28

Expression 33

Γ\Gamma

Conventional reading: Gamma

Meaning here: Gamma denotes the set of formulas or sentences fixed by the surrounding completeness argument; each occurrence record identifies whether consistency, completeness, satisfiability, entailment, or inclusion is at issue.

61 derived occurrences; 61 source occurrences
  1. Occurrence 1: introduction.tex, line 20, column 1
  2. Occurrence 2: introduction.tex, line 29, column 19
  3. Occurrence 3: introduction.tex, line 53, column 48
  4. Occurrence 4: introduction.tex, line 54, column 59
  5. Occurrence 5: introduction.tex, line 55, column 48
  6. Occurrence 6: introduction.tex, line 57, column 1
  7. Occurrence 7: introduction.tex, line 57, column 30
  8. Occurrence 8: outline.tex, line 26, column 1
  9. Occurrence 9: outline.tex, line 27, column 16
  10. Occurrence 10: outline.tex, line 30, column 4
  11. Occurrence 11: outline.tex, line 32, column 21
  12. Occurrence 12: outline.tex, line 34, column 4
  13. Occurrence 13: outline.tex, line 49, column 13
  14. Occurrence 14: outline.tex, line 53, column 4
  15. Occurrence 15: outline.tex, line 54, column 18
  16. Occurrence 16: outline.tex, line 60, column 9
  17. Occurrence 17: outline.tex, line 62, column 28
  18. Occurrence 18: outline.tex, line 64, column 23
  19. Occurrence 19: outline.tex, line 67, column 4
  20. Occurrence 20: outline.tex, line 76, column 47
  21. Occurrence 21: outline.tex, line 80, column 5
  22. Occurrence 22: outline.tex, line 151, column 5
  23. Occurrence 23: complete-consistent-sets.tex, line 20, column 34
  24. Occurrence 24: complete-consistent-sets.tex, line 27, column 24
  25. Occurrence 25: complete-consistent-sets.tex, line 36, column 15
  26. Occurrence 26: complete-consistent-sets.tex, line 49, column 10
  27. Occurrence 27: complete-consistent-sets.tex, line 62, column 9
  28. Occurrence 28: complete-consistent-sets.tex, line 79, column 46
  29. Occurrence 29: complete-consistent-sets.tex, line 85, column 23
  30. Occurrence 30: complete-consistent-sets.tex, line 96, column 1
  31. Occurrence 31: complete-consistent-sets.tex, line 97, column 1
  32. Occurrence 32: complete-consistent-sets.tex, line 137, column 47
  33. Occurrence 33: complete-consistent-sets.tex, line 148, column 11
  34. Occurrence 34: lindenbaums-lemma.tex, line 29, column 5
  35. Occurrence 35: lindenbaums-lemma.tex, line 34, column 5
  36. Occurrence 36: completeness-thm.tex, line 21, column 5
  37. Occurrence 37: completeness-thm.tex, line 21, column 45
  38. Occurrence 38: completeness-thm.tex, line 26, column 9
  39. Occurrence 39: completeness-thm.tex, line 43, column 1
  40. Occurrence 40: completeness-thm.tex, line 53, column 9
  41. Occurrence 41: completeness-thm.tex, line 58, column 15
  42. Occurrence 42: compactness.tex, line 30, column 9
  43. Occurrence 43: compactness.tex, line 35, column 38
  44. Occurrence 44: compactness.tex, line 39, column 9
  45. Occurrence 45: compactness.tex, line 45, column 19
  46. Occurrence 46: compactness.tex, line 49, column 34
  47. Occurrence 47: compactness.tex, line 49, column 47
  48. Occurrence 48: compactness.tex, line 52, column 18
  49. Occurrence 49: compactness.tex, line 63, column 42
  50. Occurrence 50: compactness.tex, line 74, column 56
  51. Occurrence 51: compactness-direct.tex, line 18, column 31
  52. Occurrence 52: compactness-direct.tex, line 23, column 51
  53. Occurrence 53: compactness-direct.tex, line 24, column 4
  54. Occurrence 54: compactness-direct.tex, line 33, column 9
  55. Occurrence 55: compactness-direct.tex, line 92, column 62
  56. Occurrence 56: compactness-direct.tex, line 116, column 34
  57. Occurrence 57: compactness-direct.tex, line 121, column 4
  58. Occurrence 58: compactness-direct.tex, line 125, column 34
  59. Occurrence 59: compactness-direct.tex, line 125, column 47
  60. Occurrence 60: compactness-direct.tex, line 128, column 18
  61. Occurrence 61: compactness-direct.tex, line 131, column 1

Expression 35

¬An∈Γ∗\lnot !A_n \in \Gamma^*

Conventional reading: not A sub n belongs to Gamma star

Meaning here: The membership statement read 'not A sub n belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 95, column 54

Expression 36

A∉Γ∗!A \notin \Gamma^*

Conventional reading: A does not belong to Gamma star

Meaning here: The nonmembership statement read 'A does not belong to Gamma star' says that the displayed formula is absent from the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 50, column 29

Expression 37

A∧B∈Γ!A \land !B \in \Gamma

Conventional reading: the conjunction of A and B belongs to Gamma

Meaning here: The membership statement read 'the conjunction of A and B belongs to Gamma' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 67, column 41

Expression 39

M(Γ∗)⊨∃xA(x)\Sat{M(\Gamma^*)}{\lexists[x][!A(x)]}

Conventional reading: structure M of Gamma star satisfies the formula there exists an x such that A of x

Meaning here: In the first-order source branch, the satisfaction statement read 'structure M of Gamma star satisfies the formula there exists an x such that A of x' asserts truth in term model M of Gamma star.

0 derived occurrences; 2 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 41

∀xA(x)\lforall[x][!A(x)]

Conventional reading: for every x, A of x

Meaning here: This is the universal formula asserting that A holds of every value for x.

0 derived occurrences; 2 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 42

A→B∈Γ!A \lif !B \in \Gamma

Conventional reading: the conditional from A to B belongs to Gamma

Meaning here: The membership statement read 'the conditional from A to B belongs to Gamma' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 73, column 39

Expression 43

v(Γ∗)⊨A\pSat{v(\Gamma^*)}{\indfrm}

Conventional reading: valuation v of Gamma star satisfies the current induction formula

Meaning here: The satisfaction statement read 'valuation v of Gamma star satisfies the current induction formula' says that the named formula, variable, or premise set is true under the displayed valuation.

2 derived occurrences; 2 source occurrences
  1. Occurrence 1: construction-of-model.tex, line 194, column 6
  2. Occurrence 2: construction-of-model.tex, line 219, column 6

Expression 44

A∉Γ!A \notin \Gamma

Conventional reading: A does not belong to Gamma

Meaning here: The nonmembership statement read 'A does not belong to Gamma' says that the displayed formula is absent from the named set.

5 derived occurrences; 5 source occurrences
  1. Occurrence 1: complete-consistent-sets.tex, line 74, column 10
  2. Occurrence 2: complete-consistent-sets.tex, line 84, column 64
  3. Occurrence 3: complete-consistent-sets.tex, line 97, column 59
  4. Occurrence 4: complete-consistent-sets.tex, line 136, column 65
  5. Occurrence 5: compactness-direct.tex, line 42, column 10

Expression 45

DM(Γ∗)\Domain{M(\Gamma^*)}

Conventional reading: the domain of term model M of Gamma star

Meaning here: This names the domain of the displayed structure; when Gamma star occurs, it is the domain of the term model built from that complete set.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 46

⊥∉Γ∗\lfalse \notin \Gamma^*

Conventional reading: falsum does not belong to Gamma star

Meaning here: The nonmembership statement read 'falsum does not belong to Gamma star' says that the displayed formula is absent from the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 173, column 55

Expression 47

A!A

Conventional reading: A

Meaning here: A is the arbitrary formula or sentence currently tested for membership, truth, derivability, or semantic consequence.

19 derived occurrences; 19 source occurrences
  1. Occurrence 1: introduction.tex, line 19, column 26
  2. Occurrence 2: introduction.tex, line 54, column 34
  3. Occurrence 3: outline.tex, line 62, column 6
  4. Occurrence 4: outline.tex, line 68, column 59
  5. Occurrence 5: outline.tex, line 69, column 1
  6. Occurrence 6: outline.tex, line 70, column 51
  7. Occurrence 7: outline.tex, line 71, column 45
  8. Occurrence 8: outline.tex, line 138, column 6
  9. Occurrence 9: complete-consistent-sets.tex, line 21, column 46
  10. Occurrence 10: complete-consistent-sets.tex, line 27, column 18
  11. Occurrence 11: complete-consistent-sets.tex, line 27, column 45
  12. Occurrence 12: complete-consistent-sets.tex, line 38, column 14
  13. Occurrence 13: complete-consistent-sets.tex, line 38, column 27
  14. Occurrence 14: lindenbaums-lemma.tex, line 20, column 42
  15. Occurrence 15: lindenbaums-lemma.tex, line 20, column 55
  16. Occurrence 16: lindenbaums-lemma.tex, line 22, column 35
  17. Occurrence 17: construction-of-model.tex, line 169, column 62
  18. Occurrence 18: completeness-thm.tex, line 53, column 36
  19. Occurrence 19: compactness.tex, line 35, column 51

Expression 48

v(Γ∗)(p)=⊤\pAssign v(\Gamma^*)(p) = \True

Conventional reading: valuation v of Gamma star assigns verum to p

Meaning here: This says that the displayed valuation assigns truth value verum to propositional variable p.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 188, column 5

Expression 50

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

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

Meaning here: This asserts that the disjunction of A and B is derivable from premise set Gamma.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 162, column 1

Expression 51

Γn∪{An}\Gamma_n \cup \{!A_n\}

Conventional reading: Gamma sub n union the singleton set containing A sub n

Meaning here: The set read 'Gamma sub n union the singleton set containing A sub n' is formed by adjoining the displayed formula or negated formula to the named premise set.

3 derived occurrences; 3 source occurrences
  1. Occurrence 1: lindenbaums-lemma.tex, line 51, column 48
  2. Occurrence 2: lindenbaums-lemma.tex, line 95, column 1
  3. Occurrence 3: compactness-direct.tex, line 110, column 8

Expression 52

Γ0=Γ\Gamma_0 = \Gamma

Conventional reading: Gamma sub zero equals Gamma

Meaning here: The recursive construction starts with Gamma sub zero equal to the original set Gamma.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 36, column 8

Expression 57

Γn∪{¬An}\Gamma_n \cup \{\lnot !A_n\}

Conventional reading: Gamma sub n union the singleton set containing not A sub n

Meaning here: The set read 'Gamma sub n union the singleton set containing not A sub n' is formed by adjoining the displayed formula or negated formula to the named premise set.

3 derived occurrences; 3 source occurrences
  1. Occurrence 1: lindenbaums-lemma.tex, line 50, column 33
  2. Occurrence 2: lindenbaums-lemma.tex, line 52, column 15
  3. Occurrence 3: compactness-direct.tex, line 110, column 36

Expression 59

v(Γ∗)⊨A\pSat{v(\Gamma^*)}{!A}

Conventional reading: valuation v of Gamma star satisfies A

Meaning here: The satisfaction statement read 'valuation v of Gamma star satisfies A' says that the named formula, variable, or premise set is true under the displayed valuation.

4 derived occurrences; 4 source occurrences
  1. Occurrence 1: outline.tex, line 162, column 1
  2. Occurrence 2: construction-of-model.tex, line 165, column 1
  3. Occurrence 3: completeness-thm.tex, line 40, column 1
  4. Occurrence 4: completeness-thm.tex, line 42, column 10

Expression 61

Γ∗=⋃n≥0Γn\Gamma^* = \bigcup_{n \geq 0} \Gamma_n

Conventional reading: Gamma star equals the union of all Gamma sub n for n greater than or equal to zero

Meaning here: Gamma star is defined as the union of every stage Gamma sub n for natural-number indices n beginning at zero.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 45, column 5

Expression 64

M(Γ∗)⊨A(t)\Sat{M(\Gamma^*)}{!A(t)}

Conventional reading: structure M of Gamma star satisfies A of t

Meaning here: In the first-order source branch, the satisfaction statement read 'structure M of Gamma star satisfies A of t' asserts truth in term model M of Gamma star.

0 derived occurrences; 3 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 68

M(Γ∗)\Struct{M(\Gamma^*)}

Conventional reading: term model M of Gamma star

Meaning here: This names the term model constructed from Gamma star in the first-order source branch.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 69

L\Lang{L}

Conventional reading: language L

Meaning here: Calligraphic L names the language whose formulas are enumerated and extended in Lindenbaum's Lemma.

1 derived occurrence; 2 source occurrences
  1. Occurrence 1: lindenbaums-lemma.tex, line 29, column 28

Expression 70

C∈Γ∗!C \in \Gamma^*

Conventional reading: C belongs to Gamma star

Meaning here: The membership statement read 'C belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 222, column 58

Expression 71

A∈Γ!A \in \Gamma

Conventional reading: A belongs to Gamma

Meaning here: The membership statement read 'A belongs to Gamma' says that the complete displayed formula belongs to the named set.

15 derived occurrences; 15 source occurrences
  1. Occurrence 1: complete-consistent-sets.tex, line 21, column 59
  2. Occurrence 2: complete-consistent-sets.tex, line 64, column 63
  3. Occurrence 3: complete-consistent-sets.tex, line 68, column 12
  4. Occurrence 4: complete-consistent-sets.tex, line 71, column 10
  5. Occurrence 5: complete-consistent-sets.tex, line 82, column 36
  6. Occurrence 6: complete-consistent-sets.tex, line 98, column 13
  7. Occurrence 7: complete-consistent-sets.tex, line 135, column 60
  8. Occurrence 8: complete-consistent-sets.tex, line 148, column 68
  9. Occurrence 9: complete-consistent-sets.tex, line 151, column 41
  10. Occurrence 10: construction-of-model.tex, line 30, column 18
  11. Occurrence 11: completeness-thm.tex, line 41, column 61
  12. Occurrence 12: compactness.tex, line 47, column 56
  13. Occurrence 13: compactness-direct.tex, line 36, column 12
  14. Occurrence 14: compactness-direct.tex, line 39, column 10
  15. Occurrence 15: compactness-direct.tex, line 123, column 56

Expression 72

Γn+1=Γn∪{An}if Γn∪{An} is consistent;Γn∪{¬An}otherwise.\Gamma_{n+1} = \begin{cases} \Gamma_n \cup \{ !A_n \} & \textrm{if $\Gamma_n \cup \{!A_n\}$ is consistent;} \\ \Gamma_n \cup \{ \lnot !A_n \} & \textrm{otherwise.} \end{cases}

Conventional reading: Gamma sub n plus one equals Gamma sub n union the singleton set containing A sub n if that union is consistent; otherwise Gamma sub n plus one equals Gamma sub n union the singleton set containing not A sub n

Meaning here: The successor stage adds A sub n when that addition is consistent and otherwise adds the negation of A sub n; this preserves consistency while deciding every enumerated formula.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 37, column 1

Expression 75

Γn⊆Γn\Gamma_n \subseteq \Gamma_n

Conventional reading: Gamma sub n is a subset of Gamma sub n

Meaning here: The inclusion read 'Gamma sub n is a subset of Gamma sub n' states that every member of the left-hand stage or finite subset also belongs to the right-hand set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 72, column 60

Expression 79

(A∨B)∈Γ∗(!A \lor !B) \in \Gamma^*

Conventional reading: the disjunction of A and B belongs to Gamma star

Meaning here: The membership statement read 'the disjunction of A and B belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: complete-consistent-sets.tex, line 50, column 51

Expression 80

v(Γ∗)⊨B\pSat{v(\Gamma^*)}{!B}

Conventional reading: valuation v of Gamma star satisfies B

Meaning here: The satisfaction statement read 'valuation v of Gamma star satisfies B' says that the named formula, variable, or premise set is true under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 220, column 9

Expression 81

Γ⊢A\Gamma \Proves !A

Conventional reading: Gamma syntactically derives A

Meaning here: This asserts that formula A is derivable from premise set Gamma in the selected proof system.

9 derived occurrences; 9 source occurrences
  1. Occurrence 1: introduction.tex, line 20, column 63
  2. Occurrence 2: introduction.tex, line 52, column 27
  3. Occurrence 3: outline.tex, line 19, column 19
  4. Occurrence 4: outline.tex, line 20, column 35
  5. Occurrence 5: complete-consistent-sets.tex, line 64, column 37
  6. Occurrence 6: complete-consistent-sets.tex, line 82, column 10
  7. Occurrence 7: complete-consistent-sets.tex, line 84, column 14
  8. Occurrence 8: completeness-thm.tex, line 54, column 1
  9. Occurrence 9: completeness-thm.tex, line 80, column 1

Expression 82

Γ0\Gamma_0

Conventional reading: Gamma sub zero

Meaning here: Gamma sub zero is the initial stage or the finite subset named by the surrounding compactness statement.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 47, column 32

Expression 84

(B∨C)∈Γ∗(!B \lor !C) \in \Gamma^*

Conventional reading: the disjunction of B and C belongs to Gamma star

Meaning here: The membership statement read 'the disjunction of B and C belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 223, column 63

Expression 85

p∈Γ∗p \in \Gamma^*

Conventional reading: p belongs to Gamma star

Meaning here: The membership statement read 'p belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 189, column 23

Expression 86

∃xA(x)\lexists[x][!A(x)]

Conventional reading: there exists an x such that A of x

Meaning here: This is the existential formula asserting that A holds of at least one value for x.

0 derived occurrences; 1 source occurrence
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 87

i≤ni \le n

Conventional reading: i is less than or equal to n

Meaning here: The index i is at most n, so monotonicity places Gamma sub i inside Gamma sub n.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 79, column 34

Expression 88

v⊨p\pSat{v}{p}

Conventional reading: valuation v satisfies p

Meaning here: The satisfaction statement read 'valuation v satisfies p' says that the named formula, variable, or premise set is true under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 46, column 42

Expression 89

s(x)=ts(x) = t

Conventional reading: s of x equals t

Meaning here: The assignment s maps variable x to the closed term t.

0 derived occurrences; 2 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 93

v(p)=⊤\pAssign{v}(p) = \True

Conventional reading: valuation v assigns verum to p

Meaning here: This says that the displayed valuation assigns truth value verum to propositional variable p.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 47, column 22

Expression 94

tt

Conventional reading: t

Meaning here: t is a closed term used as a quantifier instance or witness in the first-order source branch.

0 derived occurrences; 3 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 95

Γ0⊨A\Gamma_0 \Entails !A

Conventional reading: Gamma sub zero semantically entails A

Meaning here: Every valuation satisfying the finite subset Gamma sub zero also satisfies A.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: compactness.tex, line 38, column 33

Expression 96

A(t)!A(t)

Conventional reading: A of t

Meaning here: A of t is the closed-term instance obtained by substituting the closed term t for the displayed variable of formula A.

0 derived occurrences; 3 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Expression 98

A∨B∈Γ!A \lor !B \in \Gamma

Conventional reading: the disjunction of A and B belongs to Gamma

Meaning here: The membership statement read 'the disjunction of A and B belongs to Gamma' says that the complete displayed formula belongs to the named set.

5 derived occurrences; 5 source occurrences
  1. Occurrence 1: outline.tex, line 62, column 46
  2. Occurrence 2: complete-consistent-sets.tex, line 70, column 39
  3. Occurrence 3: complete-consistent-sets.tex, line 135, column 23
  4. Occurrence 4: complete-consistent-sets.tex, line 136, column 37
  5. Occurrence 5: complete-consistent-sets.tex, line 162, column 59

Expression 101

v(Γ∗)⊨C\pSat{v(\Gamma^*)}{!C}

Conventional reading: valuation v of Gamma star satisfies C

Meaning here: The satisfaction statement read 'valuation v of Gamma star satisfies C' says that the named formula, variable, or premise set is true under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 221, column 5

Expression 104

Γ⊆Γ∗\Gamma \subseteq \Gamma^*

Conventional reading: Gamma is a subset of Gamma star

Meaning here: The inclusion read 'Gamma is a subset of Gamma star' states that every member of the left-hand stage or finite subset also belongs to the right-hand set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 77, column 7

Expression 105

FrmL\Frm[L]

Conventional reading: the formulas of language L

Meaning here: This is the collection of every formula of language L, the collection enumerated in the Lindenbaum construction.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 93, column 23

Expression 106

v⊨¬B\pSat{v}{\lnot !B}

Conventional reading: valuation v satisfies not B

Meaning here: The satisfaction statement read 'valuation v satisfies not B' says that the named formula, variable, or premise set is true under the displayed valuation.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: outline.tex, line 58, column 1

Expression 107

=Γn∪{¬An}= \Gamma_n \cup \{\lnot !A_n\}

Conventional reading: equals Gamma sub n union the singleton set containing not A sub n

Meaning here: This source fragment supplies the alternative value Gamma sub n union the singleton containing not A sub n.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: lindenbaums-lemma.tex, line 69, column 67

Expression 108

(A∨B)∈Γ(!A \lor !B) \in \Gamma

Conventional reading: the disjunction of A and B belongs to Gamma

Meaning here: The membership statement read 'the disjunction of A and B belongs to Gamma' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: compactness-direct.tex, line 38, column 17

Expression 109

¬B∈Γ∗\lnot !B \in \Gamma^*

Conventional reading: not B belongs to Gamma star

Meaning here: The membership statement read 'not B belongs to Gamma star' says that the complete displayed formula belongs to the named set.

1 derived occurrence; 1 source occurrence
  1. Occurrence 1: construction-of-model.tex, line 200, column 26

Expression 112

M(Γ∗),s⊨A(x)\Sat{M(\Gamma^*)}{!A(x)}[s]

Conventional reading: structure M of Gamma star satisfies A of x under assignment s

Meaning here: In the first-order source branch, the satisfaction statement read 'structure M of Gamma star satisfies A of x under assignment s' asserts truth in term model M of Gamma star under assignment s.

0 derived occurrences; 3 source occurrences
  1. Source-only occurrence set; omitted from derived Read/Listen under SAR-002.

Formal objects

  1. Definition: Complete set — complete-consistent-sets.tex, line 19.
  2. Proposition: Properties of complete consistent sets — complete-consistent-sets.tex, line 60.
  3. Exercise: Complete the complete-set proposition proof — complete-consistent-sets.tex, line 218; preserved unsolved prompt.
  4. Lemma: Lindenbaum's Lemma — lindenbaums-lemma.tex, line 27.
  5. Definition: Canonical valuation from Gamma star — construction-of-model.tex, line 63.
  6. Lemma: Truth Lemma for the canonical valuation — construction-of-model.tex, line 163.
  7. Exercise: Complete the propositional Truth Lemma proof — construction-of-model.tex, line 273; preserved unsolved prompt.
  8. Theorem: Model-existence form of completeness — completeness-thm.tex, line 19.
  9. Corollary: Semantic-consequence form of completeness — completeness-thm.tex, line 51.
  10. Exercise: Recover model-existence completeness — completeness-thm.tex, line 92; preserved unsolved prompt.
  11. Exercise: Trace proof-system rules used for completeness — completeness-thm.tex, line 113; preserved unsolved prompt.
  12. Definition: Finitely satisfiable set — compactness.tex, line 29.
  13. Theorem: Compactness in two forms — compactness.tex, line 33.
  14. Exercise: Prove entailment compactness — compactness.tex, line 85; preserved unsolved prompt.
  15. Proposition: Complete finitely satisfiable sets — compactness-direct.tex, line 31.
  16. Exercise: Prove the finite-satisfiability connective proposition — compactness-direct.tex, line 53; preserved unsolved prompt.
  17. Lemma: Finite-satisfiability Lindenbaum extension — compactness-direct.tex, line 91.
  18. Exercise: Prove the finite-satisfiability Lindenbaum lemma — compactness-direct.tex, line 107; preserved unsolved prompt.
  19. Theorem: Direct compactness — compactness-direct.tex, line 115.
  20. Exercise: Rewrite the Truth Lemma for direct compactness — compactness-direct.tex, line 154; preserved unsolved prompt.
  21. Source-only formal object: Source-only proposition: Quantifiers in the term model — omitted from derived Read/Listen by SAR-002; source line 116.

65 resolved references

  1. the proposition about complete consistent sets — outline.tex, line 139.
  2. Lindenbaum's Lemma — outline.tex, line 153.
  3. the canonical valuation definition — outline.tex, line 159.
  4. the Truth Lemma — outline.tex, line 163.
  5. the complete-consistent-set closure-under-derivability proposition — complete-consistent-sets.tex, line 162.
  6. the proposition about complete consistent sets — complete-consistent-sets.tex, line 219.
  7. the proposition about complete consistent sets — construction-of-model.tex, line 225.
  8. the complete-consistent-set disjunction proposition — construction-of-model.tex, line 225.
  9. the Truth Lemma — construction-of-model.tex, line 274.
  10. Lindenbaum's Lemma — completeness-thm.tex, line 28.
  11. the Truth Lemma — completeness-thm.tex, line 39.
  12. the semantic-consequence corollary to the Completeness Theorem — completeness-thm.tex, line 58.
  13. the model-existence Completeness Theorem — completeness-thm.tex, line 59.
  14. the model-existence Completeness Theorem — completeness-thm.tex, line 60.
  15. the proposition relating entailment to unsatisfiability — completeness-thm.tex, line 67.
  16. the model-existence Completeness Theorem — completeness-thm.tex, line 69.
  17. the semantic-consequence corollary to the Completeness Theorem — completeness-thm.tex, line 93.
  18. the model-existence Completeness Theorem — completeness-thm.tex, line 94.
  19. the model-existence Completeness Theorem — completeness-thm.tex, line 120.
  20. the model-existence Completeness Theorem — compactness.tex, line 74.
  21. the Compactness Theorem — compactness.tex, line 86.
  22. the proposition about complete finitely satisfiable sets — compactness-direct.tex, line 54.
  23. the finite-satisfiability Lindenbaum lemma — compactness-direct.tex, line 108.
  24. the finite-satisfiability Lindenbaum lemma — compactness-direct.tex, line 130.
  25. the canonical valuation definition — compactness-direct.tex, line 135.
  26. the Truth Lemma — compactness-direct.tex, line 139.
  27. the proposition about complete finitely satisfiable sets — compactness-direct.tex, line 140. Reader correction: Source correction: in the propositional edition, a conditional in the source removes the replacement target from this sentence. This reader supplies the intended finite-satisfiability proposition; the source file is unchanged.
  28. the Truth Lemma — compactness-direct.tex, line 156.
  29. the direct Compactness Theorem — compactness-direct.tex, line 157.
  30. the proof-theoretic notions section for sequent calculus — complete-consistent-sets.tex, line 58.
  31. the proof-theoretic notions section for natural deduction — complete-consistent-sets.tex, line 58.
  32. the proof-theoretic notions section for axiomatic derivation — complete-consistent-sets.tex, line 58.
  33. the proof-theoretic notions section for tableaux — complete-consistent-sets.tex, line 58.
  34. the sequent calculus proposition that derivability plus an explicit negation yields inconsistency — complete-consistent-sets.tex, line 92.
  35. the natural deduction proposition that derivability plus an explicit negation yields inconsistency — complete-consistent-sets.tex, line 92.
  36. the axiomatic derivation proposition that derivability plus an explicit negation yields inconsistency — complete-consistent-sets.tex, line 92.
  37. the tableaux proposition that derivability plus an explicit negation yields inconsistency — complete-consistent-sets.tex, line 92.
  38. the sequent calculus proposition about disjunction and derivability — complete-consistent-sets.tex, line 144.
  39. the natural deduction proposition about disjunction and derivability — complete-consistent-sets.tex, line 144.
  40. the axiomatic derivation proposition about disjunction and derivability — complete-consistent-sets.tex, line 144.
  41. the tableaux proposition about disjunction and derivability — complete-consistent-sets.tex, line 144.
  42. the sequent calculus proposition about disjunction and derivability — complete-consistent-sets.tex, line 158.
  43. the natural deduction proposition about disjunction and derivability — complete-consistent-sets.tex, line 158.
  44. the axiomatic derivation proposition about disjunction and derivability — complete-consistent-sets.tex, line 158.
  45. the tableaux proposition about disjunction and derivability — complete-consistent-sets.tex, line 158.
  46. the axiomatic derivation proposition that two inconsistent one-formula extensions make the original set inconsistent — lindenbaums-lemma.tex, line 59.
  47. the sequent calculus proposition that two inconsistent one-formula extensions make the original set inconsistent — lindenbaums-lemma.tex, line 59.
  48. the natural deduction proposition that two inconsistent one-formula extensions make the original set inconsistent — lindenbaums-lemma.tex, line 59.
  49. the tableaux proposition that two inconsistent one-formula extensions make the original set inconsistent — lindenbaums-lemma.tex, line 59.
  50. the proof-compactness proposition for axiomatic derivation — lindenbaums-lemma.tex, line 87.
  51. the proof-compactness proposition for sequent calculus — lindenbaums-lemma.tex, line 87.
  52. the proof-compactness proposition for natural deduction — lindenbaums-lemma.tex, line 87.
  53. the proof-compactness proposition for tableaux — lindenbaums-lemma.tex, line 87.
  54. the axiomatic derivation proposition equating derivability of A with inconsistency after adjoining not A — completeness-thm.tex, line 76.
  55. the sequent calculus proposition equating derivability of A with inconsistency after adjoining not A — completeness-thm.tex, line 76.
  56. the natural deduction proposition equating derivability of A with inconsistency after adjoining not A — completeness-thm.tex, line 76.
  57. the tableaux proposition equating derivability of A with inconsistency after adjoining not A — completeness-thm.tex, line 76.
  58. the axiomatic derivation soundness corollary that satisfiability implies consistency — compactness.tex, line 59.
  59. the sequent calculus soundness corollary that satisfiability implies consistency — compactness.tex, line 59.
  60. the natural deduction soundness corollary that satisfiability implies consistency — compactness.tex, line 59.
  61. the tableaux soundness corollary that satisfiability implies consistency — compactness.tex, line 59.
  62. the proof-compactness proposition for axiomatic derivation — compactness.tex, line 70.
  63. the proof-compactness proposition for sequent calculus — compactness.tex, line 70.
  64. the proof-compactness proposition for natural deduction — compactness.tex, line 70.
  65. the proof-compactness proposition for tableaux — compactness.tex, line 70.