The Completeness Theorem — Explore equations

Reading preferences

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

Equation and formal-object guide

Every expression, formal object, occurrence, and resolved reference remains available for inspection.

309 expression records

Expression 1

c_{0}

c_{0}

Read as: c sub zero

Means here: c sub zero is the displayed constant symbol; in Henkin contexts it is chosen fresh as a witness constant.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 58

Expression 2

\forall x_{n} \neg A_{n} (x_{n}) ⊢ \neg \exists x_{n} A_{n} (x_{n})

\forall x_{n} \neg A_{n} (x_{n}) ⊢ \neg \exists x_{n} A_{n} (x_{n})

Read as: for every x sub n, not A sub n open parenthesis x sub n close parenthesis syntactically derives not there exists x sub n, A sub n open parenthesis x sub n close parenthesis

Means here: The statement read 'for every x sub n, not A sub n open parenthesis x sub n close parenthesis syntactically derives not there exists x sub n, A sub n open parenthesis x sub n close parenthesis' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 139

Expression 3

Γ^{*}

Γ^{*}

Read as: Gamma star

Means here: Gamma star is the constructed extension used by the current proof: a complete consistent saturated set in the Henkin completeness proof, or the corresponding complete finitely satisfiable set in the direct compactness proof.

36 occurrence(s)

Expression 4

R (t_{1}, \dots, t_{n}) \in Γ^{*} iff R ({t_{1}}^{'}, \dots, {t_{n}}^{'}) \in Γ^{*} .

R (t_{1}, \dots, t_{n}) \in Γ^{*} iff R ({t_{1}}^{'}, \dots, {t_{n}}^{'}) \in Γ^{*} .

Read as: R applied to t sub one comma and so on comma t sub n is in Gamma star if and only if R applied to t sub one prime comma and so on comma t sub n prime is in Gamma star

Means here: The membership statement read 'R applied to t sub one comma and so on comma t sub n is in Gamma star if and only if R applied to t sub one prime comma and so on comma t sub n prime is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — identity.tex, line 148

Expression 5

0

0

Read as: object-language constant zero

Means here: The expression read 'object-language constant zero' is object-language notation, distinguished from the corresponding metalanguage number or operation.

2 occurrence(s)

Expression 6

n = 0

n = 0

Read as: n equals zero

Means here: The equality or identity statement read 'n equals zero' fixes the exact objects identified by the surrounding definition or proof step.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 66

Expression 7

s

s

Read as: s

Means here: s is the variable assignment used to evaluate a formula with a free variable.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 132

Expression 8

Trm (L^{'})

Trm (L^{'})

Read as: the terms of language L prime

Means here: This is the set of terms of the displayed language; in the quotient construction the surrounding source restricts to closed terms.

1 occurrence(s)

Occurrence 1 — downward-ls.tex, line 45

Expression 9

⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})} iff R (t_{1}, \dots, t_{n}) \in Γ^{*} .

⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})} iff R (t_{1}, \dots, t_{n}) \in Γ^{*} .

Read as: the tuple t sub one comma and so on comma t sub n is in the interpretation of R in term model M of Gamma star if and only if R applied to t sub one comma and so on comma t sub n is in Gamma star

Means here: The interpretation statement read 'the tuple t sub one comma and so on comma t sub n is in the interpretation of R in term model M of Gamma star if and only if R applied to t sub one comma and so on comma t sub n is in Gamma star' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 55

Expression 10

M (Γ^{*}) ⊨ \forall x A (x)

M (Γ^{*}) ⊨ \forall x A (x)

Read as: term model M of Gamma star satisfies the universal formula, for every x, A of x

Means here: The satisfaction statement read 'term model M of Gamma star satisfies the universal formula, for every x, A of x' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 122

Expression 11

x_{n}

x_{n}

Read as: x sub n

Means here: x sub n is the displayed first-order variable, indexed when it belongs to the formula enumeration.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 102

Expression 12

t_{i + 1}

t_{i + 1}

Read as: t sub i plus one

Means here: t sub i plus one is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

4 occurrence(s)

Expression 13

ℚ

ℚ

Read as: the rational numbers

Means here: The expression read 'the rational numbers' names the displayed standard number system or numerical construction.

2 occurrence(s)

Expression 14

M (Γ^{*}), s ⊨ A (t)

M (Γ^{*}), s ⊨ A (t)

Read as: term model M of Gamma star satisfies A of t under assignment s

Means here: The satisfaction statement read 'term model M of Gamma star satisfies A of t under assignment s' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

2 occurrence(s)

Expression 15

Γ_{n + 1} = Γ_{n} \cup {D_{n}}

Γ_{n + 1} = Γ_{n} \cup {D_{n}}

Read as: Gamma sub n plus one equals Gamma sub n union D sub n

Means here: The union read 'Gamma sub n plus one equals Gamma sub n union D sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 96

Expression 16

Γ_{n + 1} = Γ_{n} \cup {\neg A_{n}}

Γ_{n + 1} = Γ_{n} \cup {\neg A_{n}}

Read as: Gamma sub n plus one equals Gamma sub n union not A sub n

Means here: The union read 'Gamma sub n plus one equals Gamma sub n union not A sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 49

Expression 17

⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})}

⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})}

Read as: the tuple t sub one comma and so on comma t sub n is in the interpretation of R in term model M of Gamma star

Means here: The interpretation statement read 'the tuple t sub one comma and so on comma t sub n is in the interpretation of R in term model M of Gamma star' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 183

Expression 18

k \in Z^{+}

k \in Z^{+}

Read as: k is in the positive integers

Means here: The membership statement read 'k is in the positive integers' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 131

Expression 19

c^{M (Γ^{*})} = c

c^{M (Γ^{*})} = c

Read as: the interpretation of c in term model M of Gamma star equals c

Means here: The interpretation statement read 'the interpretation of c in term model M of Gamma star equals c' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 47

Expression 20

A (t) \in Γ

A (t) \in Γ

Read as: A of t is in Gamma

Means here: The membership statement read 'A of t is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

5 occurrence(s)

Expression 21

d_{0}

d_{0}

Read as: object-language symbol d sub zero

Means here: The expression read 'object-language symbol d sub zero' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 35

Expression 22

A_{n} \notin Γ^{*}

A_{n} \notin Γ^{*}

Read as: A sub n is not in Gamma star

Means here: The nonmembership statement read 'A sub n is not in Gamma star' says the complete displayed formula or object is absent from the named set.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 94

Expression 23

{[t]}_{\approx} = {t^{'} : t^{'} \in Trm (L), t \approx t^{'}}

{[t]}_{\approx} = {t^{'} : t^{'} \in Trm (L), t \approx t^{'}}

Read as: the equivalence class of t under the term-model relation approx equals the set of t prime such that t prime is in the terms of language L comma t is equivalent under the term-model relation approx to t prime

Means here: This defines the approx-equivalence class of t as all closed terms t prime related to t by approx.

1 occurrence(s)

Occurrence 1 — identity.tex, line 90

Expression 24

t = t^{'}

t = t^{'}

Read as: t equals t prime

Means here: The equality or identity statement read 't equals t prime' fixes the exact objects identified by the surrounding definition or proof step.

4 occurrence(s)

Expression 25

M (Γ^{*}) ⊭ ⊥

M (Γ^{*}) ⊭ ⊥

Read as: term model M of Gamma star does not satisfy falsum

Means here: The non-satisfaction statement read 'term model M of Gamma star does not satisfy falsum' says the displayed formula is false in the named structure and assignment.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 172

Expression 26

Γ_{n} \subseteq Γ_{n + 1}

Γ_{n} \subseteq Γ_{n + 1}

Read as: Gamma sub n is a subset of Gamma sub n plus one

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

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 70

Expression 27

r \cdot k < 1

r \cdot k < 1

Read as: r times k is less than one

Means here: The order statement read 'r times k is less than one' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 138

Expression 28

Γ_{n} ⊢ \forall x_{n} \neg A_{n} (x_{n})

Γ_{n} ⊢ \forall x_{n} \neg A_{n} (x_{n})

Read as: Gamma sub n syntactically derives for every x sub n, not A sub n open parenthesis x sub n close parenthesis

Means here: The statement read 'Gamma sub n syntactically derives for every x sub n, not A sub n open parenthesis x sub n close parenthesis' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

2 occurrence(s)

Expression 29

M ⊨ Γ \cup Δ

M ⊨ Γ \cup Δ

Read as: structure M satisfies Gamma union Delta

Means here: The satisfaction statement read 'structure M satisfies Gamma union Delta' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 118

Expression 30

Γ_{n} \cup {D_{n}}

Γ_{n} \cup {D_{n}}

Read as: Gamma sub n union D sub n

Means here: The union read 'Gamma sub n union D sub n' combines the displayed premise sets or adjoins the displayed decision formula.

2 occurrence(s)

Expression 31

c \neq t

c \neq t

Read as: c is not equal to t

Means here: The equality or identity statement read 'c is not equal to t' fixes the exact objects identified by the surrounding definition or proof step.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 100

Expression 32

n

n

Read as: n

Means here: n is the exact natural-number or finite-stage index fixed by the surrounding construction.

17 occurrence(s)

Expression 33

R^{M /_{\approx}}

R^{M /_{\approx}}

Read as: the interpretation of R in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the interpretation of R in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 115

Expression 34

\in Γ_{n}

\in Γ_{n}

Read as: is in Gamma sub n

Means here: The membership statement read 'is in Gamma sub n' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 80

Expression 35

M (Γ^{*})

M (Γ^{*})

Read as: term model M of Gamma star

Means here: This names the term model constructed from Gamma star.

5 occurrence(s)

Expression 36

M

M

Read as: structure M

Means here: The expression read 'structure M' names the exact first-order structure fixed by the surrounding argument.

5 occurrence(s)

Expression 37

t \approx t^{'}

t \approx t^{'}

Read as: t is equivalent under the term-model relation approx to t prime

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

4 occurrence(s)

Expression 38

Γ^{*} ⊢ t = {t^{'}}^{'}

Γ^{*} ⊢ t = {t^{'}}^{'}

Read as: Gamma star syntactically derives t equals t double prime

Means here: The statement read 'Gamma star syntactically derives t equals t double prime' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 65

Expression 39

M ⊨ R (t)

M ⊨ R (t)

Read as: structure M satisfies R applied to t

Means here: The satisfaction statement read 'structure M satisfies R applied to t' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — identity.tex, line 125

Expression 40

Γ^{*} \supseteq Γ^{'}

Γ^{*} \supseteq Γ^{'}

Read as: Gamma star is a superset of Gamma prime

Means here: The inclusion read 'Gamma star is a superset of Gamma prime' states that the set on the left contains every member of the set on the right.

1 occurrence(s)

Occurrence 1 — completeness-thm.tex, line 29

Expression 41

\exists x A (x) \in Γ

\exists x A (x) \in Γ

Read as: there exists x, A of x is in Gamma

Means here: The membership statement read 'there exists x, A of x is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

5 occurrence(s)

Expression 42

f

f

Read as: f

Means here: f is the displayed function symbol or the compound term it forms from the listed closed terms.

4 occurrence(s)

Expression 43

Γ_{n}

Γ_{n}

Read as: Gamma sub n

Means here: Gamma sub n is stage n of the increasing Lindenbaum or finite-satisfiability construction.

11 occurrence(s)

Expression 44

\neg B \in Γ

\neg B \in Γ

Read as: not B is in Gamma

Means here: The membership statement read 'not B is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

2 occurrence(s)

Expression 45

\approx

\approx

Read as: is equivalent under the term-model relation approx to

Means here: Approx names the equivalence relation on closed terms defined by identity-sentence membership in Gamma star.

6 occurrence(s)

Expression 46

(A \to B) \in Γ

(A \to B) \in Γ

Read as: open parenthesis A implies B close parenthesis is in Gamma

Means here: The membership statement read 'open parenthesis A implies B close parenthesis is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness-direct.tex, line 41

Expression 47

{t_{1}}^{'}

{t_{1}}^{'}

Read as: t sub one prime

Means here: t sub one prime is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

1 occurrence(s)

Occurrence 1 — identity.tex, line 137

Expression 48

B (t) \in Γ^{*}

B (t) \in Γ^{*}

Read as: B of t is in Gamma star

Means here: The membership statement read 'B of t is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 255

Expression 49

Δ \cup Λ

Δ \cup Λ

Read as: Delta union Lambda

Means here: The union read 'Delta union Lambda' combines the displayed premise sets or adjoins the displayed decision formula.

2 occurrence(s)

Expression 50

d_{i}

d_{i}

Read as: object-language symbol d sub i

Means here: The expression read 'object-language symbol d sub i' is object-language notation, distinguished from the corresponding metalanguage number or operation.

2 occurrence(s)

Expression 51

M (Γ^{*}) ⊨ Γ

M (Γ^{*}) ⊨ Γ

Read as: term model M of Gamma star satisfies every sentence in Gamma

Means here: The satisfaction statement read 'term model M of Gamma star satisfies every sentence in Gamma' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 164

Expression 52

x

x

Read as: x

Means here: x is the displayed first-order variable, indexed when it belongs to the formula enumeration.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 42

Expression 53

a \in | M |

a \in | M |

Read as: a is in the domain of structure M

Means here: The membership statement read 'a is in the domain of structure M' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 108

Expression 54

c

c

Read as: c

Means here: c is the displayed constant symbol; in Henkin contexts it is chosen fresh as a witness constant.

8 occurrence(s)

Expression 55

\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})

\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})

Read as: there exists x sub n, A sub n open parenthesis x sub n close parenthesis implies A sub n open parenthesis c sub n close parenthesis

Means here: The complete first-order formula read 'there exists x sub n, A sub n open parenthesis x sub n close parenthesis implies A sub n open parenthesis c sub n close parenthesis' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 99

Expression 56

M ⊨ t = t^{'}

M ⊨ t = t^{'}

Read as: structure M satisfies t equals t prime

Means here: The satisfaction statement read 'structure M satisfies t equals t prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 115

Expression 57

B \in Γ

B \in Γ

Read as: B is in Gamma

Means here: The membership statement read 'B is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

9 occurrence(s)

Expression 58

(\exists x A (x) \to A (c)) \in Γ

(\exists x A (x) \to A (c)) \in Γ

Read as: open parenthesis there exists x, A of x implies A of c close parenthesis is in Gamma

Means here: The membership statement read 'open parenthesis there exists x, A of x implies A of c close parenthesis is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 175

Expression 59

{f^{n}}_{i}

{f^{n}}_{i}

Read as: object-language symbol f superscript n sub i

Means here: The expression read 'object-language symbol f superscript n sub i' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — outline.tex, line 110

Expression 60

| M |

| M |

Read as: the domain of structure M

Means here: The expression read 'the domain of structure M' names the underlying domain of the displayed structure.

10 occurrence(s)

Expression 61

\bar{k} = (1 + (1 + \dots + (1 + 1) \dots))

\bar{k} = (1 + (1 + \dots + (1 + 1) \dots))

Read as: the numeral for k equals open parenthesis object-language constant one plus open parenthesis object-language constant one plus and so on plus open parenthesis object-language constant one plus object-language constant one close parenthesis and so on close parenthesis close parenthesis

Means here: This expands the numeral for k as the corresponding repeated object-language sum of ones.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 143

Expression 62

\times

\times

Read as: times

Means here: times names the exact arithmetic operation or successor mark in the displayed first-order language.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 125

Expression 63

A_{1} (x_{1})

A_{1} (x_{1})

Read as: A sub one open parenthesis x sub one close parenthesis

Means here: A sub one open parenthesis x sub one close parenthesis is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 54

Expression 64

{c_{i}}^{M} = i

{c_{i}}^{M} = i

Read as: the interpretation of object-language symbol c sub i in structure M equals i

Means here: The interpretation statement read 'the interpretation of object-language symbol c sub i in structure M equals i' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 42

Expression 65

-

-

Read as: minus

Means here: minus names the exact arithmetic operation or successor mark in the displayed first-order language.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 126

Expression 66

\subseteq

\subseteq

Read as: is a subset of

Means here: The inclusion read 'is a subset of' states that every member of the left-hand set also belongs to the right-hand set.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 74

Expression 67

A_{n} (x_{n})

A_{n} (x_{n})

Read as: A sub n open parenthesis x sub n close parenthesis

Means here: A sub n open parenthesis x sub n close parenthesis is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

4 occurrence(s)

Expression 68

Γ_{n + 1} = Γ_{n} \cup {A_{n}}

Γ_{n + 1} = Γ_{n} \cup {A_{n}}

Read as: Gamma sub n plus one equals Gamma sub n union A sub n

Means here: The union read 'Gamma sub n plus one equals Gamma sub n union A sub n' combines the displayed premise sets or adjoins the displayed decision formula.

2 occurrence(s)

Expression 69

Δ^{'} \cup Λ^{'} \subseteq Δ \cup Λ

Δ^{'} \cup Λ^{'} \subseteq Δ \cup Λ

Read as: Delta prime union Lambda prime is a subset of Delta union Lambda

Means here: The inclusion read 'Delta prime union Lambda prime is a subset of Delta union Lambda' states that every member of the left-hand set also belongs to the right-hand set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 188

Expression 70

R (t_{1}, \dots, t_{n}) \in Γ^{*}

R (t_{1}, \dots, t_{n}) \in Γ^{*}

Read as: R applied to t sub one comma and so on comma t sub n is in Gamma star

Means here: The membership statement read 'R applied to t sub one comma and so on comma t sub n is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — identity.tex, line 108

Expression 71

i < 0

i < 0

Read as: i is less than zero

Means here: The order statement read 'i is less than zero' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 66

Expression 72

Γ_{n} ⊢ \neg D_{n}

Γ_{n} ⊢ \neg D_{n}

Read as: Gamma sub n syntactically derives not D sub n

Means here: The statement read 'Gamma sub n syntactically derives not D sub n' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 106

Expression 73

d_{1}

d_{1}

Read as: object-language symbol d sub one

Means here: The expression read 'object-language symbol d sub one' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 36

Expression 74

c^{M^{'}} = a

c^{M^{'}} = a

Read as: the interpretation of c in structure M prime equals a

Means here: The interpretation statement read 'the interpretation of c in structure M prime equals a' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 110

Expression 75

'

'

Read as: prime

Means here: prime names the exact arithmetic operation or successor mark in the displayed first-order language.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 161

Expression 76

Γ^{'} \subseteq Γ

Γ^{'} \subseteq Γ

Read as: Gamma prime is a subset of Gamma

Means here: The inclusion read 'Gamma prime is a subset of Gamma' states that every member of the left-hand set also belongs to the right-hand set.

2 occurrence(s)

Expression 77

(A \land B) \in Γ

(A \land B) \in Γ

Read as: open parenthesis A and B close parenthesis is in Gamma

Means here: The membership statement read 'open parenthesis A and B close parenthesis is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness-direct.tex, line 35

Expression 78

Trm (L) /_{\approx} = {{[t]}_{\approx} : t \in Trm (L)}

Trm (L) /_{\approx} = {{[t]}_{\approx} : t \in Trm (L)}

Read as: the quotient of the terms of language L by the term-model relation approx equals the set of the equivalence class of t under the term-model relation approx such that t is in the terms of language L

Means here: This defines the approx-equivalence class of t as all closed terms t prime related to t by approx.

1 occurrence(s)

Occurrence 1 — identity.tex, line 93

Expression 79

L^{'}

L^{'}

Read as: language L prime

Means here: The expression read 'language L prime' names the first-order language used by the surrounding construction.

3 occurrence(s)

Expression 80

M

M

Read as: structure M

Means here: The expression read 'structure M' names the exact first-order structure fixed by the surrounding argument.

18 occurrence(s)

Expression 81

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n}) Γ_{n} ⊢ \neg A_{n} (c_{n})

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n}) Γ_{n} ⊢ \neg A_{n} (c_{n})

Read as: Gamma sub n syntactically derives the existential formula there exists x sub n, A sub n of x sub n; and Gamma sub n syntactically derives not A sub n of c sub n

Means here: The statement read 'Gamma sub n syntactically derives the existential formula there exists x sub n, A sub n of x sub n; and Gamma sub n syntactically derives not A sub n of c sub n' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 109

Expression 82

Δ = {c \neq t : t \in Trm (L)} .

Δ = {c \neq t : t \in Trm (L)} .

Read as: Delta equals the set of terms t in language L such that constant c is not equal to t

Means here: The set-builder expression read 'Delta equals the set of terms t in language L such that constant c is not equal to t' defines exactly the auxiliary set described by its membership condition.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 102

Expression 83

Γ_{n} \cup {D_{n}}

Γ_{n} \cup {D_{n}}

Read as: Gamma sub n union D sub n

Means here: The union read 'Gamma sub n union D sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 146

Expression 84

c \times \bar{k} < 1

c \times \bar{k} < 1

Read as: c times the numeral for k is less than object-language constant one

Means here: The order statement read 'c times the numeral for k is less than object-language constant one' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 146

Expression 85

r

r

Read as: r

Means here: r is the displayed numerical value or bound used by the compactness example.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 130

Expression 86

{0 < c} \cup {c \times \bar{k} < 1 : k \in Z^{+}}

{0 < c} \cup {c \times \bar{k} < 1 : k \in Z^{+}}

Read as: the union of the singleton inequality object-language zero is less than c and the set of inequalities c times the numeral for k is less than object-language one, for positive integer k

Means here: The set-builder expression read 'the union of the singleton inequality object-language zero is less than c and the set of inequalities c times the numeral for k is less than object-language one, for positive integer k' defines exactly the auxiliary set described by its membership condition.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 139

Expression 87

⟨ k_{1}, \dots, k_{n} ⟩

⟨ k_{1}, \dots, k_{n} ⟩

Read as: the tuple k sub one comma and so on comma k sub n

Means here: the tuple k sub one comma and so on comma k sub n is the finite index tuple selecting the corresponding elements or constants.

1 occurrence(s)

Occurrence 1 — outline.tex, line 43

Expression 88

\neg A (c) \in Γ

\neg A (c) \in Γ

Read as: not A of c is in Gamma

Means here: The membership statement read 'not A of c is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — outline.tex, line 87

Expression 89

Q^{'}

Q^{'}

Read as: structure Q prime

Means here: The expression read 'structure Q prime' names the exact first-order structure fixed by the surrounding argument.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 147

Expression 90

\begin{matrix} {⟦ f (t_{1}, \dots, t_{n}) ⟧}^{M (Γ^{*})} & = f^{M (Γ^{*})} ({⟦ t_{1} ⟧}^{M (Γ^{*})}, \dots, {⟦ t_{n} ⟧}^{M (Γ^{*})}) \\ = f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) \\ = f (t_{1}, \dots, t_{n}), \end{matrix}

\begin{matrix} {⟦ f (t_{1}, \dots, t_{n}) ⟧}^{M (Γ^{*})} & = f^{M (Γ^{*})} ({⟦ t_{1} ⟧}^{M (Γ^{*})}, \dots, {⟦ t_{n} ⟧}^{M (Γ^{*})}) \\ = f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) \\ = f (t_{1}, \dots, t_{n}), \end{matrix}

Read as: row one: the value of f of t sub one through t sub n in term model M of Gamma star equals the interpretation of f applied to the values of those terms; next row: those values equal the terms themselves; next row: the result equals f of t sub one through t sub n

Means here: The term-value statement read 'row one: the value of f of t sub one through t sub n in term model M of Gamma star equals the interpretation of f applied to the values of those terms; next row: those values equal the terms themselves; next row: the result equals f of t sub one through t sub n' evaluates the displayed closed term in the named term or comparison model.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 88

Expression 91

Λ

Λ

Read as: Lambda

Means here: Lambda is the second auxiliary set of sentences used in the separation and compactness argument.

3 occurrence(s)

Expression 92

x_{i}

x_{i}

Read as: x sub i

Means here: x sub i is the displayed first-order variable, indexed when it belongs to the formula enumeration.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 55

Expression 93

a_{i} \equiv c_{k_{i}}

a_{i} \equiv c_{k_{i}}

Read as: a sub i is syntactically identical to object-language symbol c sub k sub i

Means here: The statement read 'a sub i is syntactically identical to object-language symbol c sub k sub i' asserts syntactic identity of the two displayed formula or symbol forms.

1 occurrence(s)

Occurrence 1 — outline.tex, line 45

Expression 94

Γ^{*} ⊢ t = t

Γ^{*} ⊢ t = t

Read as: Gamma star syntactically derives t equals t

Means here: The statement read 'Gamma star syntactically derives t equals t' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 62

Expression 95

{[t]}_{\approx} \notin R^{M /_{\approx}}

{[t]}_{\approx} \notin R^{M /_{\approx}}

Read as: the equivalence class of t under the term-model relation approx is not in the interpretation of R in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the equivalence class of t under the term-model relation approx is not in the interpretation of R in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 130

Expression 96

Q^{'} ⊨ Γ_{0} \cup Δ_{0}

Q^{'} ⊨ Γ_{0} \cup Δ_{0}

Read as: structure Q prime satisfies Gamma sub zero union Delta sub zero

Means here: The satisfaction statement read 'structure Q prime satisfies Gamma sub zero union Delta sub zero' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 148

Expression 97

Γ_{i} \subseteq Γ_{n}

Γ_{i} \subseteq Γ_{n}

Read as: Gamma sub i is a subset of Gamma sub n

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

3 occurrence(s)

Expression 98

N^{'}

N^{'}

Read as: structure N prime

Means here: The expression read 'structure N prime' names the exact first-order structure fixed by the surrounding argument.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 164

Expression 99

A (c)

A (c)

Read as: A of c

Means here: A of c is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

3 occurrence(s)

Expression 100

{⟦ t_{i} ⟧}^{M (Γ^{*})} = t_{i}

{⟦ t_{i} ⟧}^{M (Γ^{*})} = t_{i}

Read as: the value of t sub i in term model M of Gamma star equals t sub i

Means here: The term-value statement read 'the value of t sub i in term model M of Gamma star equals t sub i' evaluates the displayed closed term in the named term or comparison model.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 86

Expression 101

\neg A \in Γ^{*}

\neg A \in Γ^{*}

Read as: not A is in Gamma star

Means here: The membership statement read 'not A is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 50

Expression 102

M (Γ^{*}) ⊨ A

M (Γ^{*}) ⊨ A

Read as: term model M of Gamma star satisfies A

Means here: The satisfaction statement read 'term model M of Gamma star satisfies A' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

4 occurrence(s)

Expression 103

Γ^{'} \subseteq Γ_{n}

Γ^{'} \subseteq Γ_{n}

Read as: Gamma prime is a subset of Gamma sub n

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

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 80

Expression 104

Γ

Γ

Read as: Gamma

Means here: Gamma is the exact set of formulas or sentences whose consistency, satisfiability, consequence, or extension is under discussion.

100 occurrence(s)

Expression 105

⊢

⊢

Read as: syntactically derives

Means here: The turnstile denotes syntactic derivability in the selected first-order proof system.

2 occurrence(s)

Expression 106

\neg A_{n} \in Γ^{*}

\neg A_{n} \in Γ^{*}

Read as: not A sub n is in Gamma star

Means here: The membership statement read 'not A sub n is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 95

Expression 107

A \notin Γ^{*}

A \notin Γ^{*}

Read as: A is not in Gamma star

Means here: The nonmembership statement read 'A is not in Gamma star' says the complete displayed formula or object is absent from the named set.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 50

Expression 108

\begin{matrix} R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \in Γ^{*} iff \\ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) \in Γ^{*} . \end{matrix}

\begin{matrix} R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \in Γ^{*} iff \\ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) \in Γ^{*} . \end{matrix}

Read as: R of t sub one through t, then t sub i plus one through t sub n, belongs to Gamma star if and only if R with t prime in that position belongs to Gamma star

Means here: The membership statement read 'R of t sub one through t, then t sub i plus one through t sub n, belongs to Gamma star if and only if R with t prime in that position belongs to Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — identity.tex, line 50

Expression 109

M ⊨ \neg B

M ⊨ \neg B

Read as: structure M satisfies not B

Means here: The satisfaction statement read 'structure M satisfies not B' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 58

Expression 110

Γ_{n + 1} = Γ \cup {D_{0}, \dots, D_{n}}

Γ_{n + 1} = Γ \cup {D_{0}, \dots, D_{n}}

Read as: Gamma sub n plus one equals Gamma union D sub zero comma and so on comma D sub n

Means here: The union read 'Gamma sub n plus one equals Gamma union D sub zero comma and so on comma D sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 86

Expression 111

N

N

Read as: structure N

Means here: The expression read 'structure N' names the exact first-order structure fixed by the surrounding argument.

2 occurrence(s)

Expression 112

P

P

Read as: P

Means here: P is the displayed predicate symbol.

1 occurrence(s)

Occurrence 1 — outline.tex, line 40

Expression 113

\exists x A (x) \to A (c) \in Γ

\exists x A (x) \to A (c) \in Γ

Read as: there exists x, A of x implies A of c is in Gamma

Means here: The membership statement read 'there exists x, A of x implies A of c is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 45

Expression 114

(0 + 0) = 0

(0 + 0) = 0

Read as: open parenthesis object-language constant zero plus object-language constant zero close parenthesis equals object-language constant zero

Means here: The equality or identity statement read 'open parenthesis object-language constant zero plus object-language constant zero close parenthesis equals object-language constant zero' fixes the exact objects identified by the surrounding definition or proof step.

2 occurrence(s)

Expression 115

c_{i}

c_{i}

Read as: object-language symbol c sub i

Means here: The expression read 'object-language symbol c sub i' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — outline.tex, line 104

Expression 116

S

S

Read as: structure S

Means here: The expression read 'structure S' names the exact first-order structure fixed by the surrounding argument.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 151

Expression 117

A \land B \in Γ

A \land B \in Γ

Read as: A and B is in Gamma

Means here: The membership statement read 'A and B is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 67

Expression 118

0

0

Read as: zero

Means here: zero is the displayed numerical value or bound used by the compactness example.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 130

Expression 119

M^{'} ⊨ Γ^{'} \cup Δ^{'}

M^{'} ⊨ Γ^{'} \cup Δ^{'}

Read as: structure M prime satisfies Gamma prime union Delta prime

Means here: The satisfaction statement read 'structure M prime satisfies Gamma prime union Delta prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 114

Expression 120

Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n})

Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n})

Read as: Gamma star syntactically derives R applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n

Means here: The statement read 'Gamma star syntactically derives R applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 74

Expression 121

L

L

Read as: language L

Means here: The expression read 'language L' names the first-order language used by the surrounding construction.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 40

Expression 122

f (t_{1}, \dots, t_{n}) \approx f ({t_{1}}^{'}, \dots, {t_{n}}^{'})

f (t_{1}, \dots, t_{n}) \approx f ({t_{1}}^{'}, \dots, {t_{n}}^{'})

Read as: f applied to t sub one comma and so on comma t sub n is equivalent under the term-model relation approx to f applied to t sub one prime comma and so on comma t sub n prime

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 142

Expression 123

\forall x A (x) \in Γ

\forall x A (x) \in Γ

Read as: for every x, A of x is in Gamma

Means here: The membership statement read 'for every x, A of x is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

2 occurrence(s)

Expression 124

c_{n}

c_{n}

Read as: c sub n

Means here: c sub n is the displayed constant symbol; in Henkin contexts it is chosen fresh as a witness constant.

4 occurrence(s)

Expression 125

M (Γ^{*}) ⊨ \exists x A (x)

M (Γ^{*}) ⊨ \exists x A (x)

Read as: term model M of Gamma star satisfies there exists x, A of x

Means here: The satisfaction statement read 'term model M of Gamma star satisfies there exists x, A of x' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

2 occurrence(s)

Expression 126

D_{n - 1}

D_{n - 1}

Read as: D sub n minus one

Means here: D sub n minus one is the exact component or stage-decision formula used in the surrounding construction.

2 occurrence(s)

Expression 127

D_{n}

D_{n}

Read as: D sub n

Means here: D sub n is the exact component or stage-decision formula used in the surrounding construction.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 64

Expression 128

{⟦ t ⟧}^{M} = {⟦ t^{'} ⟧}^{M}

{⟦ t ⟧}^{M} = {⟦ t^{'} ⟧}^{M}

Read as: the value of t in structure M equals the value of t prime in structure M

Means here: The term-value statement read 'the value of t in structure M equals the value of t prime in structure M' evaluates the displayed closed term in the named term or comparison model.

1 occurrence(s)

Occurrence 1 — outline.tex, line 116

Expression 129

a_{i}

a_{i}

Read as: a sub i

Means here: The source metavariable read 'a sub i' has the exact formula, term, symbol, set, or index role stated by every bound source packet.

2 occurrence(s)

Expression 130

i < n + 1

i < n + 1

Read as: i is less than n plus one

Means here: The order statement read 'i is less than n plus one' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

2 occurrence(s)

Expression 131

ℝ

ℝ

Read as: the real numbers

Means here: The expression read 'the real numbers' names the displayed standard number system or numerical construction.

2 occurrence(s)

Expression 132

M (Γ^{*}) ⊨ C

M (Γ^{*}) ⊨ C

Read as: term model M of Gamma star satisfies C

Means here: The satisfaction statement read 'term model M of Gamma star satisfies C' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 221

Expression 133

t_{i - 1}

t_{i - 1}

Read as: t sub i minus one

Means here: t sub i minus one is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

4 occurrence(s)

Expression 134

c^{M /_{\approx}} = {[c]}_{\approx}

c^{M /_{\approx}} = {[c]}_{\approx}

Read as: the interpretation of c in quotient structure M modulo the term-model relation approx equals the equivalence class of c under the term-model relation approx

Means here: The quotient-model interpretation statement read 'the interpretation of c in quotient structure M modulo the term-model relation approx equals the equivalence class of c under the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 103

Expression 135

\forall x A (x)

\forall x A (x)

Read as: for every x, A of x

Means here: The complete first-order formula read 'for every x, A of x' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

3 occurrence(s)

Expression 136

P (a_{1}, \dots, a_{n})

P (a_{1}, \dots, a_{n})

Read as: P applied to a sub one comma and so on comma a sub n

Means here: The complete first-order formula read 'P applied to a sub one comma and so on comma a sub n' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

1 occurrence(s)

Occurrence 1 — outline.tex, line 37

Expression 137

M ⊨ P (a_{1}, \dots, a_{n})

M ⊨ P (a_{1}, \dots, a_{n})

Read as: structure M satisfies P applied to a sub one comma and so on comma a sub n

Means here: The satisfaction statement read 'structure M satisfies P applied to a sub one comma and so on comma a sub n' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 41

Expression 138

(0 \times 0)

(0 \times 0)

Read as: open parenthesis object-language constant zero times object-language constant zero close parenthesis

Means here: The expression read 'open parenthesis object-language constant zero times object-language constant zero close parenthesis' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — outline.tex, line 128

Expression 139

M (Γ^{*}) ⊨ B (t)

M (Γ^{*}) ⊨ B (t)

Read as: term model M of Gamma star satisfies B of t

Means here: The satisfaction statement read 'term model M of Gamma star satisfies B of t' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 253

Expression 140

A \to B \in Γ

A \to B \in Γ

Read as: A implies B is in Gamma

Means here: The membership statement read 'A implies B is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 73

Expression 141

=

=

Read as: equals

Means here: This is the identity predicate of the first-order language.

11 occurrence(s)

Expression 142

t = t^{'} \in Γ^{*}

t = t^{'} \in Γ^{*}

Read as: t equals t prime is in Gamma star

Means here: The membership statement read 't equals t prime is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — identity.tex, line 58

Expression 143

t^{'}

t^{'}

Read as: t prime

Means here: t prime is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

6 occurrence(s)

Expression 144

ℕ

ℕ

Read as: the natural numbers

Means here: The expression read 'the natural numbers' names the displayed standard number system or numerical construction.

1 occurrence(s)

Occurrence 1 — outline.tex, line 102

Expression 145

A_{0} (x_{0})

A_{0} (x_{0})

Read as: A sub zero open parenthesis x sub zero close parenthesis

Means here: A sub zero open parenthesis x sub zero close parenthesis is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

2 occurrence(s)

Expression 146

A \notin Γ

A \notin Γ

Read as: A is not in Gamma

Means here: The nonmembership statement read 'A is not in Gamma' says the complete displayed formula or object is absent from the named set.

5 occurrence(s)

Expression 147

D_{n}

D_{n}

Read as: D sub n

Means here: D sub n is the exact component or stage-decision formula used in the surrounding construction.

2 occurrence(s)

Expression 148

| M (Γ^{*}) |

| M (Γ^{*}) |

Read as: the domain of term model M of Gamma star

Means here: The expression read 'the domain of term model M of Gamma star' names the underlying domain of the displayed structure.

2 occurrence(s)

Expression 149

Γ_{n} ⊢ \neg A_{n} (c_{n})

Γ_{n} ⊢ \neg A_{n} (c_{n})

Read as: Gamma sub n syntactically derives not A sub n open parenthesis c sub n close parenthesis

Means here: The statement read 'Gamma sub n syntactically derives not A sub n open parenthesis c sub n close parenthesis' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 123

Expression 150

\bar{n}

\bar{n}

Read as: the numeral for n

Means here: The expression read 'the numeral for n' is the object-language numeral denoting the indicated natural number.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 160

Expression 151

⊥ \notin Γ^{*}

⊥ \notin Γ^{*}

Read as: falsum is not in Gamma star

Means here: The nonmembership statement read 'falsum is not in Gamma star' says the complete displayed formula or object is absent from the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 173

Expression 152

A (x)

A (x)

Read as: A of x

Means here: A of x is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

2 occurrence(s)

Expression 153

A

A

Read as: A

Means here: A is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

23 occurrence(s)

Expression 154

k

k

Read as: k

Means here: k is the exact natural-number or finite-stage index fixed by the surrounding construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 144

Expression 155

Γ_{i} \subseteq Γ_{n + 1}

Γ_{i} \subseteq Γ_{n + 1}

Read as: Gamma sub i is a subset of Gamma sub n plus one

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

2 occurrence(s)

Expression 156

r < 1 / k

r < 1 / k

Read as: r is less than one divided by k

Means here: The order statement read 'r is less than one divided by k' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 137

Expression 157

A_{\geq n}

A_{\geq n}

Read as: A sub is greater than or equal to n

Means here: The order statement read 'A sub is greater than or equal to n' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 173

Expression 158

Γ^{'} \cup Δ^{'}

Γ^{'} \cup Δ^{'}

Read as: Gamma prime union Delta prime

Means here: The union read 'Gamma prime union Delta prime' combines the displayed premise sets or adjoins the displayed decision formula.

2 occurrence(s)

Expression 159

K

K

Read as: K

Means here: K is the exact natural-number or finite-stage index fixed by the surrounding construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 145

Expression 160

0^{' \dots'}

0^{' \dots'}

Read as: object-language constant zero superscript prime and so on prime

Means here: The expression read 'object-language constant zero superscript prime and so on prime' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 160

Expression 161

\neg A (c)

\neg A (c)

Read as: not A of c

Means here: The complete first-order formula read 'not A of c' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

1 occurrence(s)

Occurrence 1 — outline.tex, line 89

Expression 162

Γ ⊢ A \lor B

Γ ⊢ A \lor B

Read as: Gamma syntactically derives A or B

Means here: The statement read 'Gamma syntactically derives A or B' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 162

Expression 163

{c_{i}}^{M} = c_{i}

{c_{i}}^{M} = c_{i}

Read as: the interpretation of object-language symbol c sub i in structure M equals object-language symbol c sub i

Means here: The interpretation statement read 'the interpretation of object-language symbol c sub i in structure M equals object-language symbol c sub i' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 106

Expression 164

f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) = f (t_{1}, \dots, t_{n})

f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) = f (t_{1}, \dots, t_{n})

Read as: the interpretation of f in term model M of Gamma star open parenthesis t sub one comma and so on comma t sub n close parenthesis equals f open parenthesis t sub one comma and so on comma t sub n close parenthesis

Means here: The interpretation statement read 'the interpretation of f in term model M of Gamma star open parenthesis t sub one comma and so on comma t sub n close parenthesis equals f open parenthesis t sub one comma and so on comma t sub n close parenthesis' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 51

Expression 165

Γ_{n} \cup {A_{n}}

Γ_{n} \cup {A_{n}}

Read as: Gamma sub n union A sub n

Means here: The union read 'Gamma sub n union A sub n' combines the displayed premise sets or adjoins the displayed decision formula.

3 occurrence(s)

Expression 166

Γ_{0} = Γ

Γ_{0} = Γ

Read as: Gamma sub zero equals Gamma

Means here: The equality or identity statement read 'Gamma sub zero equals Gamma' fixes the exact objects identified by the surrounding definition or proof step.

2 occurrence(s)

Expression 167

R

R

Read as: R

Means here: R is the displayed predicate symbol.

4 occurrence(s)

Expression 168

{[t]}_{\approx} \in R^{M /_{\approx}}

{[t]}_{\approx} \in R^{M /_{\approx}}

Read as: the equivalence class of t under the term-model relation approx is in the interpretation of R in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the equivalence class of t under the term-model relation approx is in the interpretation of R in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

2 occurrence(s)

Expression 169

Trm (L) /_{\approx}

Trm (L) /_{\approx}

Read as: the quotient of the terms of language L by the term-model relation approx

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 116

Expression 170

{⟦ t ⟧}^{M /_{\approx}} = {[t]}_{\approx}

{⟦ t ⟧}^{M /_{\approx}} = {[t]}_{\approx}

Read as: the value of t in quotient structure M modulo the term-model relation approx equals the equivalence class of t under the term-model relation approx

Means here: The expression read 'the value of t in quotient structure M modulo the term-model relation approx equals the equivalence class of t under the term-model relation approx' states equality, membership, or construction of the indicated approx-equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 164

Expression 171

c^{S}

c^{S}

Read as: the interpretation of c in structure S

Means here: The interpretation statement read 'the interpretation of c in structure S' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 152

Expression 172

\exists x B (x) \in Γ^{*}

\exists x B (x) \in Γ^{*}

Read as: there exists x, B of x is in Gamma star

Means here: The membership statement read 'there exists x, B of x is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 257

Expression 173

A_{0}

A_{0}

Read as: A sub zero

Means here: A sub zero is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 34

Expression 174

Γ^{'} = ⋃_{n} Γ_{n}

Γ^{'} = ⋃_{n} Γ_{n}

Read as: Gamma prime equals the union of sub n Gamma sub n

Means here: This defines the limit set as the union of all finite stages of the increasing construction.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 87

Expression 175

Γ^{'} \supseteq Γ

Γ^{'} \supseteq Γ

Read as: Gamma prime is a superset of Gamma

Means here: The inclusion read 'Gamma prime is a superset of Gamma' states that the set on the left contains every member of the set on the right.

2 occurrence(s)

Expression 176

A (x) \in Frm (L)

A (x) \in Frm (L)

Read as: A of x is in the formulas of language L

Means here: The membership statement read 'A of x is in the formulas of language L' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 41

Expression 177

M (Γ^{*}) ⊨ B

M (Γ^{*}) ⊨ B

Read as: term model M of Gamma star satisfies B

Means here: The satisfaction statement read 'term model M of Gamma star satisfies B' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 220

Expression 178

\neg A \in Γ

\neg A \in Γ

Read as: not A is in Gamma

Means here: The membership statement read 'not A is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

3 occurrence(s)

Expression 179

Γ_{n} \cup {\neg A_{n}}

Γ_{n} \cup {\neg A_{n}}

Read as: Gamma sub n union not A sub n

Means here: The union read 'Gamma sub n union not A sub n' combines the displayed premise sets or adjoins the displayed decision formula.

3 occurrence(s)

Expression 180

t_{1}, \dots, t_{n}

t_{1}, \dots, t_{n}

Read as: t sub one comma and so on comma t sub n

Means here: The source metavariable read 't sub one comma and so on comma t sub n' has the exact formula, term, symbol, set, or index role stated by every bound source packet.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 85

Expression 181

| M /_{\approx} | = Trm (L) /_{\approx}

| M /_{\approx} | = Trm (L) /_{\approx}

Read as: the domain of quotient structure M modulo the term-model relation approx equals the quotient of the terms of language L by the term-model relation approx

Means here: The domain of the quotient model is exactly the set of approx-equivalence classes of closed terms.

1 occurrence(s)

Occurrence 1 — identity.tex, line 102

Expression 182

Γ^{'}

Γ^{'}

Read as: Gamma prime

Means here: Gamma prime is the intermediate language expansion or premise set fixed by the surrounding proof.

8 occurrence(s)

Expression 183

\begin{matrix} Γ_{0} & = Γ \\ Γ_{n + 1} & = Γ_{n} \cup {D_{n}} \end{matrix}

\begin{matrix} Γ_{0} & = Γ \\ Γ_{n + 1} & = Γ_{n} \cup {D_{n}} \end{matrix}

Read as: Gamma sub zero then equals Gamma next row Gamma sub n plus one then equals Gamma sub n union D sub n

Means here: The union read 'Gamma sub zero then equals Gamma next row Gamma sub n plus one then equals Gamma sub n union D sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 82

Expression 184

Γ \cup {\neg A}

Γ \cup {\neg A}

Read as: Gamma union not A

Means here: The union read 'Gamma union not A' combines the displayed premise sets or adjoins the displayed decision formula.

3 occurrence(s)

Expression 185

k < K

k < K

Read as: k is less than K

Means here: The order statement read 'k is less than K' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 146

Expression 186

{f^{n}}_{i} (t_{1}, \dots, t_{n})

{f^{n}}_{i} (t_{1}, \dots, t_{n})

Read as: object-language symbol f superscript n sub i open parenthesis t sub one comma and so on comma t sub n close parenthesis

Means here: The expression read 'object-language symbol f superscript n sub i open parenthesis t sub one comma and so on comma t sub n close parenthesis' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — outline.tex, line 111

Expression 187

a \neq {⟦ t ⟧}^{M}

a \neq {⟦ t ⟧}^{M}

Read as: a is not equal to the value of t in structure M

Means here: The term-value statement read 'a is not equal to the value of t in structure M' evaluates the displayed closed term in the named term or comparison model.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 111

Expression 188

Γ_{0} \subseteq Γ

Γ_{0} \subseteq Γ

Read as: Gamma sub zero is a subset of Gamma

Means here: The inclusion read 'Gamma sub zero is a subset of Gamma' states that every member of the left-hand set also belongs to the right-hand set.

4 occurrence(s)

Expression 189

+

+

Read as: plus

Means here: plus names the exact arithmetic operation or successor mark in the displayed first-order language.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 125

Expression 190

Γ^{*} = ⋃_{n \geq 0} Γ_{n}

Γ^{*} = ⋃_{n \geq 0} Γ_{n}

Read as: Gamma star equals the union of all stages Gamma sub n for n at least zero

Means here: This defines the limit set as the union of all finite stages of the increasing construction.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 45

Expression 191

i < n

i < n

Read as: i is less than n

Means here: The order statement read 'i is less than n' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

2 occurrence(s)

Expression 192

Λ^{'} \subseteq Λ

Λ^{'} \subseteq Λ

Read as: Lambda prime is a subset of Lambda

Means here: The inclusion read 'Lambda prime is a subset of Lambda' states that every member of the left-hand set also belongs to the right-hand set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 189

Expression 193

| M | = ℕ

| M | = ℕ

Read as: the domain of structure M equals the natural numbers

Means here: This states that the domain of M is the set of natural numbers.

1 occurrence(s)

Occurrence 1 — outline.tex, line 42

Expression 194

Γ ⊨ A

Γ ⊨ A

Read as: Gamma semantically entails A

Means here: The statement read 'Gamma semantically entails A' says that every first-order structure and assignment satisfying all sentences on the left also satisfies the complete conclusion.

5 occurrence(s)

Expression 195

M (Γ^{*}) ⊨ A (t)

M (Γ^{*}) ⊨ A (t)

Read as: term model M of Gamma star satisfies A of t

Means here: The satisfaction statement read 'term model M of Gamma star satisfies A of t' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

3 occurrence(s)

Expression 196

Γ^{'} \subseteq Γ^{*}

Γ^{'} \subseteq Γ^{*}

Read as: Gamma prime is a subset of Gamma star

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

3 occurrence(s)

Expression 197

c \in L

c \in L

Read as: c is in language L

Means here: The membership statement read 'c is in language L' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 42

Expression 198

Γ^{*} ⊢ t^{'} = t

Γ^{*} ⊢ t^{'} = t

Read as: Gamma star syntactically derives t prime equals t

Means here: The statement read 'Gamma star syntactically derives t prime equals t' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 63

Expression 199

M ⊨ Γ

M ⊨ Γ

Read as: structure M satisfies Gamma

Means here: The satisfaction statement read 'structure M satisfies Gamma' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 112

Expression 200

Δ_{0}

Δ_{0}

Read as: Delta sub zero

Means here: Delta sub zero is the auxiliary set of sentences defined or selected by the surrounding completeness or compactness argument.

2 occurrence(s)

Expression 201

\bar{n} < x

\bar{n} < x

Read as: the numeral for n is less than x

Means here: The order statement read 'the numeral for n is less than x' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

2 occurrence(s)

Expression 202

B \in Γ^{*}

B \in Γ^{*}

Read as: B is in Gamma star

Means here: The membership statement read 'B is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

2 occurrence(s)

Expression 203

A \lor B

A \lor B

Read as: A or B

Means here: The complete first-order formula read 'A or B' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

2 occurrence(s)

Expression 204

A_{\geq n} \in Δ^{'}

A_{\geq n} \in Δ^{'}

Read as: A sub is greater than or equal to n is in Delta prime

Means here: The membership statement read 'A sub is greater than or equal to n is in Delta prime' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 190

Expression 205

M (Γ^{*})

M (Γ^{*})

Read as: term model M of Gamma star

Means here: This names the term model constructed from Gamma star.

8 occurrence(s)

Expression 206

P (a_{1}, \dots, a_{n}) \in Γ

P (a_{1}, \dots, a_{n}) \in Γ

Read as: P applied to a sub one comma and so on comma a sub n is in Gamma

Means here: The membership statement read 'P applied to a sub one comma and so on comma a sub n is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — outline.tex, line 43

Expression 207

L

L

Read as: language L

Means here: The expression read 'language L' names the first-order language used by the surrounding construction.

8 occurrence(s)

Expression 208

t \in {[t]}_{\approx}

t \in {[t]}_{\approx}

Read as: t is in the equivalence class of t under the term-model relation approx

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 117

Expression 209

k_{i}

k_{i}

Read as: k sub i

Means here: k sub i is the exact natural-number or finite-stage index fixed by the surrounding construction.

1 occurrence(s)

Occurrence 1 — outline.tex, line 44

Expression 210

M^{'} ⊨ Γ^{'}

M^{'} ⊨ Γ^{'}

Read as: structure M prime satisfies Gamma prime

Means here: The satisfaction statement read 'structure M prime satisfies Gamma prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 114

Expression 211

C \in Γ^{*}

C \in Γ^{*}

Read as: C is in Gamma star

Means here: The membership statement read 'C is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 222

Expression 212

Q

Q

Read as: structure Q

Means here: The expression read 'structure Q' names the exact first-order structure fixed by the surrounding argument.

2 occurrence(s)

Expression 213

Δ^{'} \subseteq Δ

Δ^{'} \subseteq Δ

Read as: Delta prime is a subset of Delta

Means here: The inclusion read 'Delta prime is a subset of Delta' states that every member of the left-hand set also belongs to the right-hand set.

2 occurrence(s)

Expression 214

Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})

Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})

Read as: Gamma star syntactically derives R applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n

Means here: The statement read 'Gamma star syntactically derives R applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 76

Expression 215

t \approx t^{'} iff t = t^{'} \in Γ^{*}

t \approx t^{'} iff t = t^{'} \in Γ^{*}

Read as: t is equivalent under the term-model relation approx to t prime if and only if t equals t prime is in Gamma star

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 30

Expression 216

A \in Γ

A \in Γ

Read as: A is in Gamma

Means here: The membership statement read 'A is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

16 occurrence(s)

Expression 217

Γ_{n + 1} = \begin{matrix} Γ_{n} \cup {A_{n}} & if Γ n \cup {A n} is consistent; \\ Γ_{n} \cup {\neg A_{n}} & otherwise. \end{matrix}

Γ_{n + 1} = \begin{matrix} Γ_{n} \cup {A_{n}} & if Γ n \cup {A n} is consistent; \\ Γ_{n} \cup {\neg A_{n}} & otherwise. \end{matrix}

Read as: Gamma sub n plus one equals Gamma sub n with A sub n adjoined when that set is consistent; otherwise it equals Gamma sub n with not A sub n adjoined

Means here: This is the successor clause of the Lindenbaum construction: adjoin A sub n if consistency is preserved, and otherwise adjoin its negation.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 37

Expression 218

M ⊭ B

M ⊭ B

Read as: structure M does not satisfy B

Means here: The non-satisfaction statement read 'structure M does not satisfy B' says the displayed formula is false in the named structure and assignment.

1 occurrence(s)

Occurrence 1 — outline.tex, line 57

Expression 219

(0 + 0)

(0 + 0)

Read as: open parenthesis object-language constant zero plus object-language constant zero close parenthesis

Means here: The expression read 'open parenthesis object-language constant zero plus object-language constant zero close parenthesis' is object-language notation, distinguished from the corresponding metalanguage number or operation.

2 occurrence(s)

Expression 220

0

0

Read as: object-language constant zero

Means here: The expression read 'object-language constant zero' is object-language notation, distinguished from the corresponding metalanguage number or operation.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 125

Expression 221

t_{1}

t_{1}

Read as: t sub one

Means here: t sub one is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

7 occurrence(s)

Expression 222

{[t]}_{\approx}

{[t]}_{\approx}

Read as: the equivalence class of t under the term-model relation approx

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

2 occurrence(s)

Expression 223

A \land B

A \land B

Read as: A and B

Means here: The complete first-order formula read 'A and B' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

3 occurrence(s)

Expression 224

M ⊨ Δ^{'} \cup Λ^{'}

M ⊨ Δ^{'} \cup Λ^{'}

Read as: structure M satisfies Delta prime union Lambda prime

Means here: The satisfaction statement read 'structure M satisfies Delta prime union Lambda prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 193

Expression 225

i = n

i = n

Read as: i equals n

Means here: The equality or identity statement read 'i equals n' fixes the exact objects identified by the surrounding definition or proof step.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 73

Expression 226

Γ_{n} \subseteq Γ_{n}

Γ_{n} \subseteq Γ_{n}

Read as: Gamma sub n is a subset of Gamma sub n

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

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 72

Expression 227

t_{n}

t_{n}

Read as: t sub n

Means here: t sub n is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

7 occurrence(s)

Expression 228

M /_{\approx}

M /_{\approx}

Read as: quotient structure M modulo the term-model relation approx

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

3 occurrence(s)

Expression 229

M = M (Γ^{*})

M = M (Γ^{*})

Read as: structure M equals term model M of Gamma star

Means here: This fixes M to be the term model constructed from Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 98

Expression 230

B \notin Γ

B \notin Γ

Read as: B is not in Gamma

Means here: The nonmembership statement read 'B is not in Gamma' says the complete displayed formula or object is absent from the named set.

3 occurrence(s)

Expression 231

A (c) \in Γ

A (c) \in Γ

Read as: A of c is in Gamma

Means here: The membership statement read 'A of c is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 178

Expression 232

\neg A

\neg A

Read as: not A

Means here: The complete first-order formula read 'not A' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

4 occurrence(s)

Expression 233

f^{M /_{\approx}}

f^{M /_{\approx}}

Read as: the interpretation of f in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the interpretation of f in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 114

Expression 234

D_{0}

D_{0}

Read as: D sub zero

Means here: D sub zero is the exact component or stage-decision formula used in the surrounding construction.

2 occurrence(s)

Expression 235

{[t^{'}]}_{\approx} \notin R^{M /_{\approx}}

{[t^{'}]}_{\approx} \notin R^{M /_{\approx}}

Read as: the equivalence class of t prime under the term-model relation approx is not in the interpretation of R in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the equivalence class of t prime under the term-model relation approx is not in the interpretation of R in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 127

Expression 236

D_{i}

D_{i}

Read as: D sub i

Means here: D sub i is the exact component or stage-decision formula used in the surrounding construction.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 80

Expression 237

(A \lor B) \in Γ^{*}

(A \lor B) \in Γ^{*}

Read as: open parenthesis A or B close parenthesis is in Gamma star

Means here: The membership statement read 'open parenthesis A or B close parenthesis is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — complete-consistent-sets.tex, line 50

Expression 238

1 / k

1 / k

Read as: one divided by k

Means here: one divided by k is the displayed numerical value or bound used by the compactness example.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 131

Expression 239

ZFC

ZFC

Read as: logical system ZFC

Means here: ZFC names the first-order theory used in the compactness application.

5 occurrence(s)

Expression 240

Γ ⊢ A

Γ ⊢ A

Read as: Gamma syntactically derives A

Means here: The statement read 'Gamma syntactically derives A' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

9 occurrence(s)

Expression 241

Γ ⊢ \exists x A (x)

Γ ⊢ \exists x A (x)

Read as: Gamma syntactically derives there exists x, A of x

Means here: The statement read 'Gamma syntactically derives there exists x, A of x' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 182

Expression 242

c^{Q^{'}} = 1 / K

c^{Q^{'}} = 1 / K

Read as: the interpretation of c in structure Q prime equals one divided by K

Means here: The interpretation statement read 'the interpretation of c in structure Q prime equals one divided by K' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 147

Expression 243

M^{'}

M^{'}

Read as: structure M prime

Means here: The expression read 'structure M prime' names the exact first-order structure fixed by the surrounding argument.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 109

Expression 244

Δ = {A_{\geq n} : n \geq 1}

Δ = {A_{\geq n} : n \geq 1}

Read as: Delta equals the set of sentences A sub at least n for every n at least one

Means here: The set-builder expression read 'Delta equals the set of sentences A sub at least n for every n at least one' defines exactly the auxiliary set described by its membership condition.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 176

Expression 245

Γ_{0}

Γ_{0}

Read as: Gamma sub zero

Means here: Gamma sub zero is the initial stage, or the finite premise subset named by the surrounding compactness argument.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 47

Expression 246

B

B

Read as: B

Means here: B is the exact component or stage-decision formula used in the surrounding construction.

5 occurrence(s)

Expression 247

(B \lor C) \in Γ^{*}

(B \lor C) \in Γ^{*}

Read as: open parenthesis B or C close parenthesis is in Gamma star

Means here: The membership statement read 'open parenthesis B or C close parenthesis is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 223

Expression 248

A_{i} (x_{i})

A_{i} (x_{i})

Read as: A sub i open parenthesis x sub i close parenthesis

Means here: A sub i open parenthesis x sub i close parenthesis is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 54

Expression 249

t_{i} \approx {t_{i}}^{'}

t_{i} \approx {t_{i}}^{'}

Read as: t sub i is equivalent under the term-model relation approx to t sub i prime

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 138

Expression 250

\begin{matrix} M /_{\approx} ⊨ t = t^{'} & iff {[t]}_{\approx} = {[t^{'}]}_{\approx} (by definition of M /_{\approx}) \\ iff t \approx t^{'} (by definition of {[t]}_{\approx}) \\ iff t = t^{'} \in Γ^{*} (by definition of \approx). \end{matrix}

\begin{matrix} M /_{\approx} ⊨ t = t^{'} & iff {[t]}_{\approx} = {[t^{'}]}_{\approx} (by definition of M /_{\approx}) \\ iff t \approx t^{'} (by definition of {[t]}_{\approx}) \\ iff t = t^{'} \in Γ^{*} (by definition of \approx). \end{matrix}

Read as: the quotient model satisfies t equals t prime if and only if their equivalence classes are equal; if and only if t is related to t prime by approx; if and only if t equals t prime belongs to Gamma star

Means here: This is the identity row of the quotient-model Truth Lemma: satisfaction of t equals t prime is equivalent successively to equality of their classes, the approx relation, and membership of the identity sentence in Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 185

Expression 251

P^{M}

P^{M}

Read as: the interpretation of P in structure M

Means here: The interpretation statement read 'the interpretation of P in structure M' fixes or applies the named constant, function, or predicate in the displayed structure.

1 occurrence(s)

Occurrence 1 — outline.tex, line 44

Expression 252

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n})

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n})

Read as: Gamma sub n syntactically derives there exists x sub n, A sub n open parenthesis x sub n close parenthesis

Means here: The statement read 'Gamma sub n syntactically derives there exists x sub n, A sub n open parenthesis x sub n close parenthesis' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 131

Expression 253

\exists x A (x)

\exists x A (x)

Read as: there exists x, A of x

Means here: The complete first-order formula read 'there exists x, A of x' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

2 occurrence(s)

Expression 254

Γ^{*} ⊢ t^{'} = {t^{'}}^{'}

Γ^{*} ⊢ t^{'} = {t^{'}}^{'}

Read as: Gamma star syntactically derives t prime equals t double prime

Means here: The statement read 'Gamma star syntactically derives t prime equals t double prime' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 64

Expression 255

i \leq n

i \leq n

Read as: i is less than or equal to n

Means here: The order statement read 'i is less than or equal to n' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 79

Expression 256

M ⊨ R (t_{1}, \dots, t_{n})

M ⊨ R (t_{1}, \dots, t_{n})

Read as: structure M satisfies R applied to t sub one comma and so on comma t sub n

Means here: The satisfaction statement read 'structure M satisfies R applied to t sub one comma and so on comma t sub n' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

2 occurrence(s)

Expression 257

f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \approx f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) .

f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \approx f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) .

Read as: f applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n is equivalent under the term-model relation approx to f applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n

Means here: This states compatibility with the term congruence approx, which is generated by identities belonging to Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 44

Expression 258

Γ^{*} ⊢ f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) = f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})

Γ^{*} ⊢ f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) = f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})

Γ^{*} ⊢ f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1},, \dots, t_{n}) = f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})

Read as: Gamma star syntactically derives f applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n equals f applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n

Means here: The statement read 'Gamma star syntactically derives f applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n equals f applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

1 occurrence(s)

Occurrence 1 — identity.tex, line 67

Expression 259

Δ^{'}

Δ^{'}

Read as: Delta prime

Means here: Delta prime is the auxiliary set of sentences defined or selected by the surrounding completeness or compactness argument.

2 occurrence(s)

Expression 260

R (t_{1}, \dots, t_{n}) \in Γ^{*}

R (t_{1}, \dots, t_{n}) \in Γ^{*}

Read as: R open parenthesis t sub one comma and so on comma t sub n close parenthesis is in Gamma star

Means here: The membership statement read 'R open parenthesis t sub one comma and so on comma t sub n close parenthesis is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 185

Expression 261

{⟦ t ⟧}^{M (Γ^{*})} = t

{⟦ t ⟧}^{M (Γ^{*})} = t

Read as: the value of t in term model M of Gamma star equals t

Means here: The term-value statement read 'the value of t in term model M of Gamma star equals t' evaluates the displayed closed term in the named term or comparison model.

3 occurrence(s)

Expression 262

<

<

Read as: is less than

Means here: The order statement read 'is less than' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 124

Expression 263

M (Γ^{*}) ⊨ A

M (Γ^{*}) ⊨ A

Read as: term model M of Gamma star satisfies the current induction formula

Means here: The satisfaction statement read 'term model M of Gamma star satisfies the current induction formula' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

3 occurrence(s)

Expression 264

s (x) = t

s (x) = t

Read as: s open parenthesis x close parenthesis equals t

Means here: The equality or identity statement read 's open parenthesis x close parenthesis equals t' fixes the exact objects identified by the surrounding definition or proof step.

2 occurrence(s)

Expression 265

M ⊨ A

M ⊨ A

Read as: structure M satisfies A

Means here: The satisfaction statement read 'structure M satisfies A' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

2 occurrence(s)

Expression 266

i

i

Read as: i

Means here: i is the exact natural-number or finite-stage index fixed by the surrounding construction.

2 occurrence(s)

Expression 267

Γ_{n}

Γ_{n}

Read as: Gamma sub n

Means here: Gamma sub n is stage n of the increasing Lindenbaum or finite-satisfiability construction.

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 96

Expression 268

A_{1}

A_{1}

Read as: A sub one

Means here: A sub one is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 34

Expression 269

\exists x A (x) \to A (c)

\exists x A (x) \to A (c)

Read as: there exists x, A of x implies A of c

Means here: The complete first-order formula read 'there exists x, A of x implies A of c' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

2 occurrence(s)

Expression 270

\neg B

\neg B

Read as: not B

Means here: The complete first-order formula read 'not B' preserves every quantifier, connective, term argument, and scope boundary printed in the source.

2 occurrence(s)

Expression 271

t

t

Read as: t

Means here: t is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

27 occurrence(s)

Expression 272

Γ_{0} ⊨ A

Γ_{0} ⊨ A

Read as: Gamma sub zero semantically entails A

Means here: The statement read 'Gamma sub zero semantically entails A' says that every first-order structure and assignment satisfying all sentences on the left also satisfies the complete conclusion.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 38

Expression 273

M = M (Γ^{*})

M = M (Γ^{*})

Read as: structure M equals term model M of Gamma star

Means here: This fixes M to be the term model constructed from Gamma star.

1 occurrence(s)

Occurrence 1 — identity.tex, line 163

Expression 274

A \equiv t = t^{'}

A \equiv t = t^{'}

Read as: A is syntactically identical to t equals t prime

Means here: The statement read 'A is syntactically identical to t equals t prime' asserts syntactic identity of the two displayed formula or symbol forms.

1 occurrence(s)

Occurrence 1 — identity.tex, line 183

Expression 275

A (t)

A (t)

Read as: A of t

Means here: A of t is the exact arbitrary, enumerated, or instantiated first-order formula fixed by this source context.

5 occurrence(s)

Expression 276

f (t_{1}, \dots, t_{n})

f (t_{1}, \dots, t_{n})

Read as: f open parenthesis t sub one comma and so on comma t sub n close parenthesis

Means here: f open parenthesis t sub one comma and so on comma t sub n close parenthesis is the displayed function symbol or the compound term it forms from the listed closed terms.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 50

Expression 277

B \notin Γ^{*}

B \notin Γ^{*}

Read as: B is not in Gamma star

Means here: The nonmembership statement read 'B is not in Gamma star' says the complete displayed formula or object is absent from the named set.

2 occurrence(s)

Expression 278

A \lor B \in Γ

A \lor B \in Γ

Read as: A or B is in Gamma

Means here: The membership statement read 'A or B is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

5 occurrence(s)

Expression 279

\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})

\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})

Read as: there exists x sub n, A sub n open parenthesis x sub n close parenthesis implies A sub n open parenthesis c sub n close parenthesis

1 occurrence(s)

Occurrence 1 — henkin-expansions.tex, line 65

Expression 280

{[t]}_{\approx} = {[t^{'}]}_{\approx}

{[t]}_{\approx} = {[t^{'}]}_{\approx}

Read as: the equivalence class of t under the term-model relation approx equals the equivalence class of t prime under the term-model relation approx

Means here: The expression read 'the equivalence class of t under the term-model relation approx equals the equivalence class of t prime under the term-model relation approx' states equality, membership, or construction of the indicated approx-equivalence classes.

2 occurrence(s)

Expression 281

M (Γ^{*}) ⊭ B

M (Γ^{*}) ⊭ B

Read as: term model M of Gamma star does not satisfy B

Means here: The non-satisfaction statement read 'term model M of Gamma star does not satisfy B' says the displayed formula is false in the named structure and assignment.

2 occurrence(s)

Expression 282

B \in Γ^{'}

B \in Γ^{'}

Read as: B is in Gamma prime

Means here: The membership statement read 'B is in Gamma prime' says the complete displayed formula, term, tuple, or object belongs to the named set.

2 occurrence(s)

Expression 283

{t_{n}}^{'}

{t_{n}}^{'}

Read as: t sub n prime

Means here: t sub n prime is a closed-term metavariable, with its subscript or prime distinguishing the exact term position.

1 occurrence(s)

Occurrence 1 — identity.tex, line 137

Expression 284

Γ_{i}

Γ_{i}

Read as: Gamma sub i

Means here: Gamma sub i is an earlier stage of the increasing construction.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 78

Expression 285

f^{M /_{\approx}} ({[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx}) = {[f (t_{1}, \dots, t_{n})]}_{\approx}

f^{M /_{\approx}} ({[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx}) = {[f (t_{1}, \dots, t_{n})]}_{\approx}

Read as: the interpretation of f in quotient structure M modulo the term-model relation approx open parenthesis the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx close parenthesis equals the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx

Means here: The quotient-model interpretation statement read 'the interpretation of f in quotient structure M modulo the term-model relation approx open parenthesis the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx close parenthesis equals the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 104

Expression 286

{[f (t_{1}, \dots, t_{n})]}_{\approx} = {[f ({t_{1}}^{'}, \dots, {t_{n}}^{'})]}_{\approx}

{[f (t_{1}, \dots, t_{n})]}_{\approx} = {[f ({t_{1}}^{'}, \dots, {t_{n}}^{'})]}_{\approx}

Read as: the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx equals the equivalence class of f applied to t sub one prime comma and so on comma t sub n prime under the term-model relation approx

Means here: The expression read 'the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx equals the equivalence class of f applied to t sub one prime comma and so on comma t sub n prime under the term-model relation approx' states equality, membership, or construction of the indicated approx-equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 140

Expression 287

L

L

Read as: language L

Means here: The expression read 'language L' names the first-order language used by the surrounding construction.

9 occurrence(s)

Expression 288

Δ

Δ

Read as: Delta

Means here: Delta is the auxiliary set of sentences defined or selected by the surrounding completeness or compactness argument.

10 occurrence(s)

Expression 289

⟨ {[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx} ⟩ \in R^{M /_{\approx}}

⟨ {[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx} ⟩ \in R^{M /_{\approx}}

Read as: the tuple the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx is in the interpretation of R in quotient structure M modulo the term-model relation approx

Means here: The quotient-model interpretation statement read 'the tuple the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx is in the interpretation of R in quotient structure M modulo the term-model relation approx' defines or tests the named constant, function, or predicate on equivalence classes.

1 occurrence(s)

Occurrence 1 — identity.tex, line 106

Expression 290

L^{'}

L^{'}

Read as: language L prime

Means here: The expression read 'language L prime' names the first-order language used by the surrounding construction.

5 occurrence(s)

Expression 291

M ⊨ R ({t_{1}}^{'}, \dots, {t_{n}}^{'})

M ⊨ R ({t_{1}}^{'}, \dots, {t_{n}}^{'})

Read as: structure M satisfies R applied to t sub one prime comma and so on comma t sub n prime

Means here: The satisfaction statement read 'structure M satisfies R applied to t sub one prime comma and so on comma t sub n prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — identity.tex, line 147

Expression 292

\geq n

\geq n

Read as: is greater than or equal to n

Means here: The order statement read 'is greater than or equal to n' supplies the exact stage, cardinal, numeral, or rational bound used in the construction.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 192

Expression 293

Γ \subseteq Γ^{*}

Γ \subseteq Γ^{*}

Read as: Gamma is a subset of Gamma star

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

1 occurrence(s)

Occurrence 1 — outline.tex, line 77

Expression 294

Frm (L)

Frm (L)

Read as: the formulas of language L

Means here: This is the set of all formulas of language L enumerated by the Lindenbaum construction.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 93

Expression 295

{⟦ c ⟧}^{M} \neq {⟦ t ⟧}^{M}

{⟦ c ⟧}^{M} \neq {⟦ t ⟧}^{M}

Read as: the value of c in structure M is not equal to the value of t in structure M

Means here: The term-value statement read 'the value of c in structure M is not equal to the value of t in structure M' evaluates the displayed closed term in the named term or comparison model.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 119

Expression 296

\forall x \forall y x = y

\forall x \forall y x = y

Read as: for every x, for every y, x equals y

Means here: The equality or identity statement read 'for every x, for every y, x equals y' fixes the exact objects identified by the surrounding definition or proof step.

1 occurrence(s)

Occurrence 1 — identity.tex, line 199

Expression 297

M ⊭ R (t)

M ⊭ R (t)

Read as: structure M does not satisfy R applied to t

Means here: The non-satisfaction statement read 'structure M does not satisfy R applied to t' says the displayed formula is false in the named structure and assignment.

1 occurrence(s)

Occurrence 1 — identity.tex, line 126

Expression 298

= Γ_{n} \cup {\neg A_{n}}

= Γ_{n} \cup {\neg A_{n}}

Read as: equals Gamma sub n union not A sub n

Means here: The union read 'equals Gamma sub n union not A sub n' combines the displayed premise sets or adjoins the displayed decision formula.

1 occurrence(s)

Occurrence 1 — lindenbaums-lemma.tex, line 69

Expression 299

M /_{\approx} ⊨ A

M /_{\approx} ⊨ A

Read as: quotient structure M modulo the term-model relation approx satisfies A

Means here: The satisfaction statement read 'quotient structure M modulo the term-model relation approx satisfies A' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

3 occurrence(s)

Expression 300

Γ^{*} ⊢ t = t^{'}

Γ^{*} ⊢ t = t^{'}

Read as: Gamma star syntactically derives t equals t prime

Means here: The statement read 'Gamma star syntactically derives t equals t prime' asserts that the complete formula to the right has a finite derivation from the displayed premises in the selected first-order proof system.

5 occurrence(s)

Expression 301

k \in | N |

k \in | N |

Read as: k is in the domain of structure N

Means here: The membership statement read 'k is in the domain of structure N' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 159

Expression 302

(A \lor B) \in Γ

(A \lor B) \in Γ

Read as: open parenthesis A or B close parenthesis is in Gamma

Means here: The membership statement read 'open parenthesis A or B close parenthesis is in Gamma' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — compactness-direct.tex, line 38

Expression 303

\neg B \in Γ^{*}

\neg B \in Γ^{*}

Read as: not B is in Gamma star

Means here: The membership statement read 'not B is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 200

Expression 304

M (Γ^{*}) ⊨ R (t_{1}, \dots, t_{n})

M (Γ^{*}) ⊨ R (t_{1}, \dots, t_{n})

Read as: term model M of Gamma star satisfies R of t sub one through t sub n

Means here: The satisfaction statement read 'term model M of Gamma star satisfies R of t sub one through t sub n' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — construction-of-model.tex, line 183

Expression 305

M^{'} ⊨ Δ^{'}

M^{'} ⊨ Δ^{'}

Read as: structure M prime satisfies Delta prime

Means here: The satisfaction statement read 'structure M prime satisfies Delta prime' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

1 occurrence(s)

Occurrence 1 — compactness.tex, line 112

Expression 306

Γ \cup Δ

Γ \cup Δ

Read as: Gamma union Delta

Means here: The union read 'Gamma union Delta' combines the displayed premise sets or adjoins the displayed decision formula.

8 occurrence(s)

Expression 307

A \in Γ^{*}

A \in Γ^{*}

Read as: A is in Gamma star

Means here: The membership statement read 'A is in Gamma star' says the complete displayed formula, term, tuple, or object belongs to the named set.

7 occurrence(s)

Expression 308

M (Γ^{*}), s ⊨ A (x)

M (Γ^{*}), s ⊨ A (x)

Read as: term model M of Gamma star satisfies A of x under assignment s

Means here: The satisfaction statement read 'term model M of Gamma star satisfies A of x under assignment s' asserts truth of the displayed formula or every sentence of the displayed set in the named structure.

3 occurrence(s)

Expression 309

1

1

Read as: object-language constant one

Means here: The expression read 'object-language constant one' is object-language notation, distinguished from the corresponding metalanguage number or operation.

2 occurrence(s)

52 formal objects

Definition of a complete set of sentences

A set Gamma is complete exactly when, for every sentence A, either A belongs to Gamma or the negation of A belongs to Gamma.

Expression one, in source order: Gamma.
Expression two, in source order: A.
Expression three, in source order: A is in Gamma.
Expression four, in source order: not A is in Gamma.

Source line 19

Proposition characterizing complete consistent sets

For complete consistent Gamma, derivability implies membership; a conjunction belongs exactly when both conjuncts belong; a disjunction belongs exactly when at least one disjunct belongs; and an implication belongs exactly when its antecedent is absent or its consequent belongs.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma syntactically derives A.
Expression three, in source order: A is in Gamma.
Expression four, in source order: A and B is in Gamma.
Expression five, in source order: A is in Gamma.
Expression six, in source order: B is in Gamma.
Expression seven, in source order: A or B is in Gamma.
Expression eight, in source order: A is in Gamma.
Expression nine, in source order: B is in Gamma.
Expression ten, in source order: A implies B is in Gamma.
Expression eleven, in source order: A is not in Gamma.
Expression twelve, in source order: B is in Gamma.

Source line 60

Exercise: complete the complete consistent set proof

The exercise asks the reader to complete the proof of the proposition characterizing membership in a complete consistent set. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the proposition characterizing complete consistent sets.

Source line 212

Proposition preserving consistency under language expansion

If Gamma is consistent in language L, then adding a denumerable family of new constants to obtain language L prime leaves Gamma consistent in the expanded language.

Expression one, in source order: Gamma.
Expression two, in source order: language L.
Expression three, in source order: language L prime.
Expression four, in source order: language L.
Expression five, in source order: object-language symbol d sub zero.
Expression six, in source order: object-language symbol d sub one.
Expression seven, in source order: Gamma.
Expression eight, in source order: language L prime.

Source line 32

Definition of a saturated set

A set Gamma is saturated when every one-free-variable formula has a constant witness whose existential implication belongs to Gamma.

Expression one, in source order: Gamma.
Expression two, in source order: language L.
Expression three, in source order: A of x is in the formulas of language L.
Expression four, in source order: x.
Expression five, in source order: c is in language L.
Expression six, in source order: there exists x, A of x implies A of c is in Gamma.

Source line 39

Definition of the Henkin witness sentences

The definition enumerates the one-free-variable formulas of the expanded language, chooses each fresh witness constant outside the formulas and earlier witness sentences, and defines the corresponding existential witness implication.

Expression one, in source order: language L prime.
Resolved reference one, in source order: Reference to the proposition preserving consistency under language expansion.
Expression two, in source order: A sub zero open parenthesis x sub zero close parenthesis.
Expression three, in source order: A sub one open parenthesis x sub one close parenthesis.
Expression four, in source order: A sub i open parenthesis x sub i close parenthesis.
Expression five, in source order: language L prime.
Expression six, in source order: x sub i.
Expression seven, in source order: D sub n.
Expression eight, in source order: n.
Expression nine, in source order: c sub zero.
Expression ten, in source order: object-language symbol d sub i.
Expression eleven, in source order: language L.
Expression twelve, in source order: A sub zero open parenthesis x sub zero close parenthesis.
Expression thirteen, in source order: D sub zero.
Expression fourteen, in source order: D sub n minus one.
Expression fifteen, in source order: c sub n.
Expression sixteen, in source order: object-language symbol d sub i.
Expression seventeen, in source order: D sub zero.
Expression eighteen, in source order: D sub n minus one.
Expression nineteen, in source order: A sub n open parenthesis x sub n close parenthesis.
Expression twenty, in source order: D sub n.
Expression twenty one, in source order: there exists x sub n, A sub n open parenthesis x sub n close parenthesis implies A sub n open parenthesis c sub n close parenthesis.

Source line 51

Henkin saturation extension lemma

Every consistent set Gamma extends to a saturated consistent set Gamma prime.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma prime.

Source line 70

Display defining the Henkin extension sequence

The two-row display starts with Gamma sub zero equal to Gamma and forms each successor by adjoining the current Henkin witness sentence.

Expression one, in source order: displayed formula: Gamma sub zero then equals Gamma next row Gamma sub n plus one then equals Gamma sub n union D sub n.

Source line 82

Proposition characterizing quantifiers in a saturated set

For complete consistent saturated Gamma, an existential sentence belongs exactly when one closed-term instance belongs, and a universal sentence belongs exactly when every closed-term instance belongs.

Expression one, in source order: Gamma.
Expression two, in source order: there exists x, A of x is in Gamma.
Expression three, in source order: A of t is in Gamma.
Expression four, in source order: t.
Expression five, in source order: for every x, A of x is in Gamma.
Expression six, in source order: A of t is in Gamma.
Expression seven, in source order: t.

Source line 160

Lindenbaum extension lemma

Every consistent set Gamma in language L extends to a complete consistent set Gamma star.

Expression one, in source order: Gamma.
Expression two, in source order: language L.
Expression three, in source order: Gamma star.

Source line 27

Definition of the term model

For complete consistent saturated Gamma star, the term model has all closed terms as its domain, interprets each constant as itself, interprets each function by term formation, and makes a predicate tuple true exactly when its atomic sentence belongs to Gamma star.

Expression one, in source order: Gamma star.
Expression two, in source order: language L.
Expression three, in source order: term model M of Gamma star.
Expression four, in source order: Gamma star.
Expression five, in source order: the domain of term model M of Gamma star.
Expression six, in source order: language L.
Expression seven, in source order: c.
Expression eight, in source order: c.
Expression nine, in source order: the interpretation of c in term model M of Gamma star equals c.
Expression ten, in source order: f.
Expression eleven, in source order: t sub one.
Expression twelve, in source order: t sub n.
Expression thirteen, in source order: f open parenthesis t sub one comma and so on comma t sub n close parenthesis.
Expression fourteen, in source order: displayed formula: the interpretation of f in term model M of Gamma star open parenthesis t sub one comma and so on comma t sub n close parenthesis equals f open parenthesis t sub one comma and so on comma t sub n close parenthesis.
Expression fifteen, in source order: R.
Expression sixteen, in source order: n.
Expression seventeen, in source order: displayed formula: the tuple t sub one comma and so on comma t sub n is in the interpretation of R in term model M of Gamma star if and only if R applied to t sub one comma and so on comma t sub n is in Gamma star.

Source line 37

Lemma evaluating closed terms in the term model

Every closed term t evaluates to itself in the term model of Gamma star.

Expression one, in source order: term model M of Gamma star.
Resolved reference one, in source order: Reference to the definition of the term model.
Expression two, in source order: the value of t in term model M of Gamma star equals t.

Source line 78

Display for the term-value induction step

The three-row display evaluates a compound term by applying the interpreted function to the values of its arguments, replaces those values by the terms themselves, and obtains the original compound term.

Expression one, in source order: displayed formula: row one: the value of f of t sub one through t sub n in term model M of Gamma star equals the interpretation of f applied to the values of those terms; next row: those values equal the terms themselves; next row: the result equals f of t sub one through t sub n.

Source line 88

Proposition characterizing quantifiers in the term model

In the term model, an existential sentence is true exactly when one closed-term instance is true, and a universal sentence is true exactly when every closed-term instance is true.

Expression one, in source order: term model M of Gamma star.
Resolved reference one, in source order: Reference to the definition of the term model.
Expression two, in source order: term model M of Gamma star satisfies there exists x, A of x.
Expression three, in source order: term model M of Gamma star satisfies A of t.
Expression four, in source order: t.
Expression five, in source order: term model M of Gamma star satisfies the universal formula, for every x, A of x.
Expression six, in source order: term model M of Gamma star satisfies A of t.
Expression seven, in source order: t.
Source correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged.

Source line 116

Exercise: complete the term model quantifier proof

The exercise asks the reader to complete the proof characterizing existential and universal truth in the term model. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the proposition characterizing quantifiers in the term model.

Source line 158

Truth Lemma for the term model without identity

For a sentence A that contains no identity symbol, the term model of Gamma star satisfies A exactly when A belongs to Gamma star.

Expression one, in source order: A.
Expression two, in source order: equals.
Expression three, in source order: term model M of Gamma star satisfies A.
Expression four, in source order: A is in Gamma star.

Source line 163

Exercise: complete the Truth Lemma proof

The exercise asks the reader to complete the proof of the Truth Lemma for the term model without identity. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the term-model Truth Lemma without identity.

Source line 265

Definition of the term-model congruence relation

For closed terms, t is related to t prime by the relation approx exactly when the identity sentence saying t equals t prime belongs to Gamma star.

Expression one, in source order: Gamma star.
Expression two, in source order: language L.
Expression three, in source order: is equivalent under the term-model relation approx to.
Expression four, in source order: language L.
Expression five, in source order: displayed formula: t is equivalent under the term-model relation approx to t prime if and only if t equals t prime is in Gamma star.

Source line 26

Proposition establishing the congruence properties of approx

The relation approx is reflexive, symmetric, and transitive; replacing related terms preserves function-term equivalence and preserves membership of predicate atoms in Gamma star.

Expression one, in source order: is equivalent under the term-model relation approx to.
Expression two, in source order: is equivalent under the term-model relation approx to.
Expression three, in source order: is equivalent under the term-model relation approx to.
Expression four, in source order: is equivalent under the term-model relation approx to.
Expression five, in source order: t is equivalent under the term-model relation approx to t prime.
Expression six, in source order: f.
Expression seven, in source order: t sub one.
Expression eight, in source order: t sub i minus one.
Expression nine, in source order: t sub i plus one.
Expression ten, in source order: t sub n.
Expression eleven, in source order: displayed formula: f applied to t sub one comma and so on comma t sub i minus one comma t comma t sub i plus one comma and so on comma t sub n is equivalent under the term-model relation approx to f applied to t sub one comma and so on comma t sub i minus one comma t prime comma t sub i plus one comma and so on comma t sub n.
Expression twelve, in source order: t is equivalent under the term-model relation approx to t prime.
Expression thirteen, in source order: R.
Expression fourteen, in source order: t sub one.
Expression fifteen, in source order: t sub i minus one.
Expression sixteen, in source order: t sub i plus one.
Expression seventeen, in source order: t sub n.
Expression eighteen, in source order: displayed formula: R of t sub one through t, then t sub i plus one through t sub n, belongs to Gamma star if and only if R with t prime in that position belongs to Gamma star.

Source line 35

Display of predicate congruence under approx

The two-line display says that a predicate atom with t in one argument position belongs to Gamma star exactly when the corresponding atom with the related term t prime belongs.

Expression one, in source order: displayed formula: R of t sub one through t, then t sub i plus one through t sub n, belongs to Gamma star if and only if R with t prime in that position belongs to Gamma star.

Source line 50

Exercise: complete the congruence proof

The exercise asks the reader to complete the proof that approx is an equivalence relation and a congruence for functions and predicates. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the congruence proposition for the relation approx.

Source line 82

Definition of equivalence classes and the quotient term set

The equivalence class of a closed term t contains exactly the closed terms related to t by approx, and the quotient term set consists of all such equivalence classes.

Expression one, in source order: Gamma star.
Expression two, in source order: language L.
Expression three, in source order: t.
Expression four, in source order: is equivalent under the term-model relation approx to.
Expression five, in source order: displayed formula: the equivalence class of t under the term-model relation approx equals the set of t prime such that t prime is in the terms of language L comma t is equivalent under the term-model relation approx to t prime.
Expression six, in source order: the quotient of the terms of language L by the term-model relation approx equals the set of the equivalence class of t under the term-model relation approx such that t is in the terms of language L.

Source line 86

Definition of the factored term model

The quotient structure has equivalence classes of closed terms as its domain, interprets constants and functions by their equivalence classes, and interprets predicates by truth in the original term model, equivalently by membership in Gamma star.

Expression one, in source order: structure M equals term model M of Gamma star.
Expression two, in source order: Gamma star.
Resolved reference one, in source order: Reference to the definition of the term model.
Expression three, in source order: quotient structure M modulo the term-model relation approx.
Expression four, in source order: the domain of quotient structure M modulo the term-model relation approx equals the quotient of the terms of language L by the term-model relation approx.
Expression five, in source order: the interpretation of c in quotient structure M modulo the term-model relation approx equals the equivalence class of c under the term-model relation approx.
Expression six, in source order: the interpretation of f in quotient structure M modulo the term-model relation approx open parenthesis the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx close parenthesis equals the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx.
Expression seven, in source order: the tuple the equivalence class of t sub one under the term-model relation approx comma and so on comma the equivalence class of t sub n under the term-model relation approx is in the interpretation of R in quotient structure M modulo the term-model relation approx.
Expression eight, in source order: structure M satisfies R applied to t sub one comma and so on comma t sub n.
Expression nine, in source order: R applied to t sub one comma and so on comma t sub n is in Gamma star.

Source line 96

Proposition that the quotient structure is well defined

If corresponding closed terms are related by approx, then their function values determine the same equivalence class and their predicate atoms have the same truth value in the term model.

Expression one, in source order: quotient structure M modulo the term-model relation approx.
Expression two, in source order: t sub one.
Expression three, in source order: t sub n.
Expression four, in source order: t sub one prime.
Expression five, in source order: t sub n prime.
Expression six, in source order: t sub i is equivalent under the term-model relation approx to t sub i prime.
Expression seven, in source order: the equivalence class of f applied to t sub one comma and so on comma t sub n under the term-model relation approx equals the equivalence class of f applied to t sub one prime comma and so on comma t sub n prime under the term-model relation approx.
Expression eight, in source order: displayed formula: f applied to t sub one comma and so on comma t sub n is equivalent under the term-model relation approx to f applied to t sub one prime comma and so on comma t sub n prime.
Expression nine, in source order: structure M satisfies R applied to t sub one comma and so on comma t sub n.
Expression ten, in source order: structure M satisfies R applied to t sub one prime comma and so on comma t sub n prime.
Expression eleven, in source order: displayed formula: R applied to t sub one comma and so on comma t sub n is in Gamma star if and only if R applied to t sub one prime comma and so on comma t sub n prime is in Gamma star.

Source line 135

Lemma evaluating terms in the quotient model

Every term t evaluates in the quotient structure to the equivalence class of t under approx.

Expression one, in source order: structure M equals term model M of Gamma star.
Expression two, in source order: the value of t in quotient structure M modulo the term-model relation approx equals the equivalence class of t under the term-model relation approx.

Source line 162

Exercise: complete the quotient term-value proof

The exercise asks the reader to complete the proof that each term evaluates to its equivalence class in the quotient model. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the quotient-model term-value lemma.

Source line 171

Truth Lemma for the quotient model with identity

For every sentence A, the quotient term model satisfies A exactly when A belongs to Gamma star.

Expression one, in source order: quotient structure M modulo the term-model relation approx satisfies A.
Expression two, in source order: A is in Gamma star.
Expression three, in source order: A.

Source line 175

Display of the identity case of the quotient Truth Lemma

The display follows three equivalent conditions: the quotient model satisfies t equals t prime, their equivalence classes are equal, t is related to t prime by approx, and the equality sentence belongs to Gamma star.

Expression one, in source order: displayed formula: the quotient model satisfies t equals t prime if and only if their equivalence classes are equal; if and only if t is related to t prime by approx; if and only if t equals t prime belongs to Gamma star.

Source line 185

First formulation of the Completeness Theorem

Every consistent set Gamma of first-order sentences is satisfiable.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma.

Source line 19

Semantic-to-syntactic formulation of completeness

For every set Gamma and sentence A, if Gamma semantically entails A, then Gamma syntactically derives A.

Expression one, in source order: Gamma.
Expression two, in source order: A.
Expression three, in source order: Gamma semantically entails A.
Expression four, in source order: Gamma syntactically derives A.

Source line 51

Exercise: derive the first completeness formulation

The exercise asks the reader to derive the consistency-implies-satisfiability theorem from the semantic-to-syntactic completeness corollary and thereby prove the formulations equivalent. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the semantic-to-syntactic completeness corollary.
Resolved reference two, in source order: Reference to the Completeness Theorem.

Source line 84

Exercise: audit the rules used by completeness

The exercise asks for a list or diagram tracing every explicit and tacit use of derivation rules in the results leading to completeness. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the Completeness Theorem.

Source line 100

Definition of finite satisfiability

A set Gamma is finitely satisfiable exactly when every finite subset Gamma sub zero of Gamma is satisfiable.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma sub zero is a subset of Gamma.

Source line 29

Compactness Theorem in two forms

For a set of sentences Gamma and a sentence A, semantic entailment has a finite witnessing subset; equivalently, Gamma is satisfiable exactly when every finite subset is satisfiable.

Expression one, in source order: Gamma.
Expression two, in source order: A.
Expression three, in source order: Gamma semantically entails A.
Expression four, in source order: Gamma sub zero is a subset of Gamma.
Expression five, in source order: Gamma sub zero semantically entails A.
Expression six, in source order: Gamma.
Source correction: The frozen source calls both Gamma and A sentences, although the theorem uses Gamma as a set of sentences. The reader supplies the missing type distinction; the source line is unchanged.

Source line 33

Exercise: prove the finite entailment form of compactness

The exercise asks the reader to prove the first clause of the Compactness Theorem, which gives a finite subset witnessing semantic entailment. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the Compactness Theorem in two forms.

Source line 79

Compactness example producing a non-covered model

Starting from an infinite model, the example adds a new constant and inequalities saying it differs from every old closed term; every finite subset is satisfiable, so compactness yields a model with an element not named by any old term.

Expression one, in source order: structure M.
Expression two, in source order: Gamma.
Expression three, in source order: t.
Expression four, in source order: the domain of structure M.
Expression five, in source order: the domain of structure M.
Expression six, in source order: Gamma.
Expression seven, in source order: Gamma.
Expression eight, in source order: structure M.
Expression nine, in source order: Gamma.
Expression ten, in source order: c.
Expression eleven, in source order: Gamma.
Expression twelve, in source order: Delta.
Expression thirteen, in source order: c is not equal to t.
Expression fourteen, in source order: t.
Expression fifteen, in source order: language L.
Expression sixteen, in source order: Gamma.
Expression seventeen, in source order: displayed formula: Delta equals the set of terms t in language L such that constant c is not equal to t.
Expression eighteen, in source order: Gamma union Delta.
Expression nineteen, in source order: Gamma prime union Delta prime.
Expression twenty, in source order: Gamma prime is a subset of Gamma.
Expression twenty one, in source order: Delta prime is a subset of Delta.
Expression twenty two, in source order: Delta prime.
Expression twenty three, in source order: a is in the domain of structure M.
Expression twenty four, in source order: the domain of structure M.
Expression twenty five, in source order: structure M prime.
Expression twenty six, in source order: structure M.
Expression twenty seven, in source order: the interpretation of c in structure M prime equals a.
Expression twenty eight, in source order: a is not equal to the value of t in structure M.
Expression twenty nine, in source order: t.
Expression thirty, in source order: Delta prime.
Expression thirty one, in source order: structure M prime satisfies Delta prime.
Expression thirty two, in source order: structure M satisfies Gamma.
Expression thirty three, in source order: Gamma prime is a subset of Gamma.
Expression thirty four, in source order: c.
Expression thirty five, in source order: Gamma.
Expression thirty six, in source order: structure M prime satisfies Gamma prime.
Expression thirty seven, in source order: structure M prime satisfies Gamma prime union Delta prime.
Expression thirty eight, in source order: Gamma prime union Delta prime.
Expression thirty nine, in source order: Gamma union Delta.
Expression forty, in source order: Gamma union Delta.
Expression forty one, in source order: Gamma union Delta.
Expression forty two, in source order: M that satisfies Gamma union Delta.
Expression forty three, in source order: structure M.
Expression forty four, in source order: Gamma.
Expression forty five, in source order: the value of c in structure M is not equal to the value of t in structure M.
Expression forty six, in source order: t.
Expression forty seven, in source order: language L.

Source line 91

Compactness example producing an infinitesimal

The example expands the ordered-field language by a constant c, requires c to be positive and smaller than every reciprocal numeral, verifies finite satisfiability in suitable rational expansions, and uses compactness to obtain a model containing an infinitesimal.

Expression one, in source order: language L.
Expression two, in source order: is less than.
Expression three, in source order: object-language constant zero.
Expression four, in source order: object-language constant one.
Expression five, in source order: plus.
Expression six, in source order: times.
Expression seven, in source order: minus.
Expression eight, in source order: Gamma.
Expression nine, in source order: structure Q.
Expression ten, in source order: the rational numbers.
Expression eleven, in source order: Gamma.
Expression twelve, in source order: language L.
Expression thirteen, in source order: the rational numbers.
Expression fourteen, in source order: the real numbers.
Expression fifteen, in source order: r.
Expression sixteen, in source order: zero.
Expression seventeen, in source order: one divided by k.
Expression eighteen, in source order: k is in the positive integers.
Expression nineteen, in source order: Gamma.
Expression twenty, in source order: r is less than one divided by k.
Expression twenty one, in source order: r times k is less than one.
Expression twenty two, in source order: c.
Expression twenty three, in source order: Delta.
Expression twenty four, in source order: displayed formula: the union of the singleton inequality object-language zero is less than c and the set of inequalities c times the numeral for k is less than object-language one, for positive integer k.
Expression twenty five, in source order: the numeral for k equals open parenthesis object-language constant one plus open parenthesis object-language constant one plus and so on plus open parenthesis object-language constant one plus object-language constant one close parenthesis and so on close parenthesis close parenthesis.
Expression twenty six, in source order: k.
Expression twenty seven, in source order: object-language constant one.
Expression twenty eight, in source order: Delta sub zero.
Expression twenty nine, in source order: Delta.
Expression thirty, in source order: K.
Expression thirty one, in source order: c times the numeral for k is less than object-language constant one.
Expression thirty two, in source order: Delta sub zero.
Expression thirty three, in source order: k is less than K.
Expression thirty four, in source order: structure Q.
Expression thirty five, in source order: structure Q prime.
Expression thirty six, in source order: the interpretation of c in structure Q prime equals one divided by K.
Expression thirty seven, in source order: structure Q prime satisfies Gamma sub zero union Delta sub zero.
Expression thirty eight, in source order: Gamma sub zero is a subset of Gamma.
Expression thirty nine, in source order: Gamma union Delta.
Expression forty, in source order: Gamma union Delta.
Expression forty one, in source order: structure S.
Expression forty two, in source order: Gamma union Delta.
Expression forty three, in source order: the interpretation of c in structure S.
Source correction: The frozen sentence combines 'for all' with 'have' and has no grammatical subject for the bound. The reader states that every displayed inequality in the finite subset has index k below K; the source is unchanged.

Source line 123

Exercise: obtain a nonstandard arithmetic element

The exercise asks the reader to use compactness to obtain a model of true arithmetic containing an element larger than every standard numeral. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Expression one, in source order: structure N.
Expression two, in source order: k is in the domain of structure N.
Expression three, in source order: the numeral for n is less than x.
Expression four, in source order: the numeral for n.
Expression five, in source order: object-language constant zero superscript prime and so on prime.
Expression six, in source order: n.
Expression seven, in source order: prime.
Expression eight, in source order: structure N.
Expression nine, in source order: structure N prime.
Expression ten, in source order: the numeral for n is less than x.

Source line 157

Compactness example separating infinitude from finitude

Sentences requiring at least n objects can force models to be infinite, while compactness shows that no first-order theory can have exactly all finite structures as its models.

Expression one, in source order: A sub is greater than or equal to n.
Expression two, in source order: n.
Expression three, in source order: the domain of structure M.
Expression four, in source order: n.
Expression five, in source order: displayed formula: Delta equals the set of sentences A sub at least n for every n at least one.
Expression six, in source order: Delta.
Expression seven, in source order: Delta.
Expression eight, in source order: Gamma union Delta.
Expression nine, in source order: Gamma.
Expression ten, in source order: Lambda.
Expression eleven, in source order: Delta union Lambda.
Expression twelve, in source order: Delta prime union Lambda prime is a subset of Delta union Lambda.
Expression thirteen, in source order: Delta prime is a subset of Delta.
Expression fourteen, in source order: Lambda prime is a subset of Lambda.
Expression fifteen, in source order: n.
Expression sixteen, in source order: A sub is greater than or equal to n is in Delta prime.
Expression seventeen, in source order: Lambda.
Expression eighteen, in source order: structure M.
Expression nineteen, in source order: is greater than or equal to n.
Expression twenty, in source order: structure M satisfies Delta prime union Lambda prime.
Expression twenty one, in source order: Delta union Lambda.
Expression twenty two, in source order: Lambda.

Source line 170

Proposition characterizing complete finitely satisfiable sets

For complete finitely satisfiable Gamma, conjunction, disjunction, and implication membership obey the expected truth-functional clauses.

Expression one, in source order: Gamma.
Expression two, in source order: open parenthesis A and B close parenthesis is in Gamma.
Expression three, in source order: A is in Gamma.
Expression four, in source order: B is in Gamma.
Expression five, in source order: open parenthesis A or B close parenthesis is in Gamma.
Expression six, in source order: A is in Gamma.
Expression seven, in source order: B is in Gamma.
Expression eight, in source order: open parenthesis A implies B close parenthesis is in Gamma.
Expression nine, in source order: A is not in Gamma.
Expression ten, in source order: B is in Gamma.

Source line 31

Exercise: prove the finite-satisfiability clauses directly

The exercise asks the reader to prove the proposition about complete finitely satisfiable sets without using syntactic derivability. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the proposition characterizing complete finitely satisfiable sets.
Expression one, in source order: syntactically derives.

Source line 47

Finite-satisfiability Henkin extension lemma

Every finitely satisfiable set Gamma extends to a saturated finitely satisfiable set Gamma prime.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma prime.

Source line 59

Exercise: prove the finite-satisfiability Henkin lemma

The exercise asks the reader to prove the saturation extension while showing directly that adjoining each witness sentence preserves finite satisfiability. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the finite-satisfiability Henkin extension lemma.
Expression one, in source order: Gamma sub n.
Expression two, in source order: Gamma sub n union D sub n.

Source line 66

Proposition characterizing quantified instances under finite satisfiability

For complete finitely satisfiable saturated Gamma, an existential belongs exactly when some closed-term instance belongs, and a universal belongs exactly when every closed-term instance belongs.

Expression one, in source order: Gamma.
Expression two, in source order: there exists x, A of x is in Gamma.
Expression three, in source order: A of t is in Gamma.
Expression four, in source order: t.
Expression five, in source order: for every x, A of x is in Gamma.
Expression six, in source order: A of t is in Gamma.
Expression seven, in source order: t.

Source line 74

Exercise: prove the finite-satisfiability quantifier clauses

The exercise asks the reader to prove the quantified-instance proposition for complete finitely satisfiable saturated sets. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the finite-satisfiability proposition for quantified instances.

Source line 86

Finite-satisfiability Lindenbaum extension lemma

Every finitely satisfiable set Gamma extends to a complete finitely satisfiable set Gamma star.

Expression one, in source order: Gamma.
Expression two, in source order: Gamma star.

Source line 91

Exercise: prove the finite-satisfiability Lindenbaum lemma

The exercise asks the reader to prove the extension lemma by showing that one of the two opposite successor extensions remains finitely satisfiable. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the finite-satisfiability Lindenbaum extension lemma.
Expression one, in source order: Gamma sub n.
Expression two, in source order: Gamma sub n union A sub n.
Expression three, in source order: Gamma sub n union not A sub n.

Source line 98

Direct Compactness Theorem

A set Gamma is satisfiable exactly when it is finitely satisfiable.

Expression one, in source order: Gamma.

Source line 115

Exercise: write the direct-proof Truth Lemma

The exercise asks the reader to write the complete version of the Truth Lemma needed by the direct proof of compactness. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

Resolved reference one, in source order: Reference to the term-model Truth Lemma without identity.
Resolved reference two, in source order: Reference to the direct Compactness Theorem.

Source line 146

Downward Lowenheim Skolem Theorem

Every consistent set Gamma has an enumerable model whose domain is finite or denumerable.

Expression one, in source order: Gamma.

Source line 20

Downward Lowenheim Skolem Theorem without identity

Every consistent set of sentences in first-order logic without identity has a denumerable model with an infinite enumerable domain.

Expression one, in source order: Gamma.

Source line 33

Example: Skolem's Paradox

If set theory is consistent, the Downward Lowenheim Skolem Theorem gives it enumerable models even though those models contain objects that the theory itself describes as nonenumerable.

Expression one, in source order: logical system ZFC.
Expression two, in source order: logical system ZFC.
Expression three, in source order: the real numbers.
Expression four, in source order: logical system ZFC.
Expression five, in source order: logical system ZFC.
Expression six, in source order: logical system ZFC.

Source line 48

114 resolved references

Reference to the proposition characterizing complete consistent sets — source line 139
Reference to the definition of the Henkin witness sentences — source line 142
Reference to the Henkin saturation extension lemma — source line 144
Reference to the proposition characterizing quantifiers in a saturated set — source line 149
Reference to Lindenbaum's extension lemma — source line 153
Reference to the definition of the term model — source line 159
Reference to the term-model Truth Lemma without identity — source line 163
Reference to the definition of the factored term model — source line 167
Reference to the quotient-model Truth Lemma with identity — source line 168
Reference to the derivability implies membership clause for complete consistent sets — source line 162
Reference to the proposition characterizing complete consistent sets — source line 213
Reference to the proposition preserving consistency under language expansion — source line 53
Reference to the proposition preserving consistency under language expansion — source line 79
Reference to the definition of the Henkin witness sentences — source line 81
Reference to the definition of the Henkin witness sentences — source line 103
Reference to the proposition characterizing complete consistent sets — source line 178
Reference to the derivability implies membership clause for complete consistent sets — source line 178
Reference to the proposition characterizing complete consistent sets — source line 184
Reference to the derivability implies membership clause for complete consistent sets — source line 184
Reference to the definition of the term model — source line 80
Reference to the definition of the term model — source line 118
Reference to the semantic proposition for quantified formulas — source line 130
Reference to the substitution and assignment extensionality proposition — source line 136
Reference to the proposition equating sentence truth and assignment satisfaction — source line 138
Reference to the proposition characterizing quantifiers in the term model — source line 159
Reference to the proposition characterizing complete consistent sets — source line 225
Reference to the disjunction clause for complete consistent sets — source line 225
Reference to the proposition characterizing quantifiers in the term model — source line 254
Reference to the proposition characterizing quantifiers in a saturated set — source line 256
Reference to the term-model Truth Lemma without identity — source line 266
Reference to the congruence proposition for the relation approx — source line 83
Reference to the definition of the term model — source line 99
Reference to the congruence proposition for the relation approx — source line 132
Reference to the congruence proposition for the relation approx — source line 156
Reference to the term-model value lemma — source line 168
Reference to the quotient-model term-value lemma — source line 172
Reference to the term-model Truth Lemma without identity — source line 182
Reference to the Henkin saturation extension lemma — source line 27
Reference to Lindenbaum's extension lemma — source line 28
Reference to the term-model Truth Lemma without identity — source line 39
Reference to the quotient-model Truth Lemma with identity — source line 45
Reference to the semantic-to-syntactic completeness corollary — source line 58
Reference to the Completeness Theorem — source line 59
Reference to the Completeness Theorem — source line 60
Reference to the proposition relating entailment to unsatisfiability — source line 67
Reference to the Completeness Theorem — source line 69
Reference to the semantic-to-syntactic completeness corollary — source line 85
Reference to the Completeness Theorem — source line 86
Reference to the Completeness Theorem — source line 107
Reference to the Completeness Theorem — source line 74
Reference to the Compactness Theorem in two forms — source line 80
Reference to the proposition characterizing complete finitely satisfiable sets — source line 48
Reference to the finite-satisfiability Henkin extension lemma — source line 67
Reference to the finite-satisfiability proposition for quantified instances — source line 87
Reference to the finite-satisfiability Lindenbaum extension lemma — source line 99
Reference to the finite-satisfiability Henkin extension lemma — source line 129
Reference to the finite-satisfiability Lindenbaum extension lemma — source line 130
Reference to the definition of the term model — source line 135
Reference to the proposition characterizing quantifiers in the term model — source line 136
Reference to the term-model Truth Lemma without identity — source line 139
Reference to the proposition characterizing complete consistent sets — source line 140
Reference to the proposition characterizing quantifiers in a saturated set — source line 141
Reference to the proposition characterizing complete finitely satisfiable sets — source line 142
Reference to the finite-satisfiability proposition for quantified instances — source line 142
Reference to the term-model Truth Lemma without identity — source line 148
Reference to the direct Compactness Theorem — source line 149
Reference to the Proof Theoretic Notions section for sequent calculus — source line 57
Reference to the Proof Theoretic Notions section for natural deduction — source line 57
Reference to the Proof Theoretic Notions section for axiomatic deduction — source line 57
Reference to the Proof Theoretic Notions section for tableaux — source line 57
Reference to the explicit inconsistency proposition for sequent calculus — source line 88
Reference to the explicit inconsistency proposition for natural deduction — source line 88
Reference to the explicit inconsistency proposition for axiomatic deduction — source line 88
Reference to the explicit inconsistency proposition for tableaux — source line 88
Reference to the proposition giving disjunction derivability facts for sequent calculus — source line 140
Reference to the proposition giving disjunction derivability facts for natural deduction — source line 140
Reference to the proposition giving disjunction derivability facts for axiomatic deduction — source line 140
Reference to the proposition giving disjunction derivability facts for tableaux — source line 140
Reference to the proposition giving disjunction derivability facts for sequent calculus — source line 154
Reference to the proposition giving disjunction derivability facts for natural deduction — source line 154
Reference to the proposition giving disjunction derivability facts for axiomatic deduction — source line 154
Reference to the proposition giving disjunction derivability facts for tableaux — source line 154
Reference to the Strong Generalization Theorem for axiomatic deduction — source line 121
Reference to the Strong Generalization Theorem for sequent calculus — source line 121
Reference to the Strong Generalization Theorem for natural deduction — source line 121
Reference to the Strong Generalization Theorem for tableaux — source line 121
Reference to the proposition giving implication derivability facts for axiomatic deduction — source line 177
Reference to the proposition giving implication derivability facts for sequent calculus — source line 177
Reference to the proposition giving implication derivability facts for natural deduction — source line 177
Reference to the proposition giving implication derivability facts for tableaux — source line 177
Reference to the proposition giving quantifier derivability facts for axiomatic deduction — source line 183
Reference to the proposition giving quantifier derivability facts for sequent calculus — source line 183
Reference to the proposition giving quantifier derivability facts for natural deduction — source line 183
Reference to the proposition giving quantifier derivability facts for tableaux — source line 183
Reference to the proposition about two inconsistent opposite extensions for axiomatic deduction — source line 55
Reference to the proposition about two inconsistent opposite extensions for sequent calculus — source line 55
Reference to the proposition about two inconsistent opposite extensions for natural deduction — source line 55
Reference to the proposition about two inconsistent opposite extensions for tableaux — source line 55
Reference to the proof theoretic compactness proposition for axiomatic deduction — source line 83
Reference to the proof theoretic compactness proposition for sequent calculus — source line 83
Reference to the proof theoretic compactness proposition for natural deduction — source line 83
Reference to the proof theoretic compactness proposition for tableaux — source line 83
Reference to the proposition relating derivability to inconsistency for axiomatic deduction — source line 72
Reference to the proposition relating derivability to inconsistency for sequent calculus — source line 72
Reference to the proposition relating derivability to inconsistency for natural deduction — source line 72
Reference to the proposition relating derivability to inconsistency for tableaux — source line 72
Reference to the soundness corollary that satisfiability implies consistency for axiomatic deduction — source line 55
Reference to the soundness corollary that satisfiability implies consistency for sequent calculus — source line 55
Reference to the soundness corollary that satisfiability implies consistency for natural deduction — source line 55
Reference to the soundness corollary that satisfiability implies consistency for tableaux — source line 55
Reference to the proof theoretic compactness proposition for axiomatic deduction — source line 66
Reference to the proof theoretic compactness proposition for sequent calculus — source line 66
Reference to the proof theoretic compactness proposition for natural deduction — source line 66
Reference to the proof theoretic compactness proposition for tableaux — source line 66