Semantics of First-Order Logic — Explore equations

Expression 1

M, s_{2} ⊨ \exists y R (x, y)

Conventional reading: structure M under assignment s sub two satisfies there exists y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s sub two satisfies there exists y, R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 345, column 24

Expression 2

a^{M} = 1

Conventional reading: the interpretation of a in structure M equals one

Meaning here: The expression reads the interpretation of a in structure M equals one. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 185, column 7

Expression 3

<^{M}

Conventional reading: the interpretation of less than in structure M

Meaning here: The expression reads the interpretation of less than in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 43, column 52

Expression 4

R (a, a) \to (R (b, x) \lor R (x, b))

Conventional reading: R of a comma a implies open scope R of b comma x or R of x comma b close scope

Meaning here: This conditional has atomic antecedent R of a comma a and a disjunctive consequent; the surrounding example identifies implication as its main connective.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 217, column 50

Expression 5

M, s_{2} [3 / y] ⊨ R (x, y)

Conventional reading: structure M under assignment s sub two updated to send variable y to object three satisfies R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s sub two updated to send variable y to object three satisfies R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 344, column 1

Expression 6

i = 1

Conventional reading: i equals one

Meaning here: The expression reads i equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

4 occurrences

Expression 7

0

Conventional reading: object language symbol zero

Meaning here: The expression reads object language symbol zero. The expression names a first-order language or one of its object-language symbols.

2 occurrences

Expression 8

s

Conventional reading: variable assignment s

Meaning here: The letter s names a variable assignment from all variables into the current structure's domain.

36 occurrences

Expression 9

A [t' / x]

Conventional reading: A with t prime substituted for variable x

Meaning here: The expression reads A with t prime substituted for variable x. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 124, column 21

Expression 10

M ⊩ B

Conventional reading: structure M makes true B

Meaning here: The expression reads structure M makes true B. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 313, column 9

Expression 11

M ⊨ Γ \cup {A}

Conventional reading: structure M satisfies Gamma union open brace A close brace

Meaning here: The expression reads structure M satisfies Gamma union open brace A close brace. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 118, column 39

Expression 12

c_{2}

Conventional reading: c sub two

Meaning here: Here c sub two is the second component of an ordered pair of domain elements.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 45, column 20

Expression 13

\times^{M}

Conventional reading: the interpretation of object language symbol times in structure M

Meaning here: The expression reads the interpretation of object language symbol times in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 49, column 48

Expression 14

x_{n}

Conventional reading: variable x sub n

Meaning here: This is the n-th variable in the finite list containing the variables relevant to a term or formula.

6 occurrences

Expression 15

| M |

Conventional reading: the domain of structure M

Meaning here: The expression reads the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

3 occurrences

Expression 16

⟨ 1, 3 ⟩ \in <^{M}

Conventional reading: the ordered tuple one comma three is an element of the interpretation of less than in structure M

Meaning here: The expression reads the ordered tuple one comma three is an element of the interpretation of less than in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 45, column 40

Expression 17

⊨ A

Conventional reading: A is valid

Meaning here: Sentence A is valid: it is true in every first-order structure, with no premises assumed.

2 occurrences

Expression 18

\forall x (R (a, x) \to \exists y R (x, y)) .

Conventional reading: for every x, open parenthesis R open parenthesis a comma x close parenthesis implies there exists y, R open parenthesis x comma y close parenthesis close parenthesis

Meaning here: The expression reads for every x, open parenthesis R open parenthesis a comma x close parenthesis implies there exists y, R open parenthesis x comma y close parenthesis close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 325, column 1

Expression 19

M, s [2 / x] ⊨ \exists y R (x, y)

Conventional reading: structure M under assignment s updated to send variable x to object two satisfies there exists y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object two satisfies there exists y, R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 338, column 17

Expression 20

M, s [m / x] ⊭ R (b, x) \land R (x, b)

Conventional reading: structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis b comma x close parenthesis and R open parenthesis x comma b close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis b comma x close parenthesis and R open parenthesis x comma b close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 258, column 48

Expression 21

\forall x A (x, f (x))

Conventional reading: for every x, A open parenthesis x comma f open parenthesis x close parenthesis close parenthesis

Meaning here: The expression reads for every x, A open parenthesis x comma f open parenthesis x close parenthesis close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 349, column 1

Expression 22

M ⊨ A (t)

Conventional reading: structure M satisfies A open parenthesis t close parenthesis

Meaning here: The expression reads structure M satisfies A open parenthesis t close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 136, column 41

Expression 23

⟨ 2, 3 ⟩ \in R^{M}

Conventional reading: the ordered tuple two comma three is an element of the interpretation of R in structure M

Meaning here: The expression reads the ordered tuple two comma three is an element of the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 344, column 44

Expression 24

A (x, y)

Conventional reading: formula A with free variables x and y

Meaning here: This notation presents formula A with x and y as its displayed free-variable arguments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 343, column 46

Expression 25

M, s [4 / x] ⊭ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object four does not satisfy R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object four does not satisfy R open parenthesis a comma x close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 329, column 1

Expression 26

a_{1}

Conventional reading: domain element a sub one

Meaning here: This is the first selected domain element paired with the fresh constant c sub one in the substitution exercise.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 333, column 1

Expression 27

s \sim_{x} s [{Val}_{s}^{M} (t') / x]

Conventional reading: assignment s is an x variant of assignment s updated to send variable x to object the value of t prime in structure M under assignment s

Meaning here: The expression reads assignment s is an x variant of assignment s updated to send variable x to object the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 80, column 3

Expression 28

m = 1

Conventional reading: m equals one

Meaning here: The expression reads m equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

5 occurrences

Expression 29

s [m / x] (y) = \begin{matrix} m & if y \equiv x \\ s (y) & otherwise . \end{matrix}

Conventional reading: the assignment s updated at x with m sends y to m if y is syntactically identical to x and sends y to s of y otherwise

Meaning here: This two-case definition changes assignment s only at variable x, sending x to domain element m and preserving every other value.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 91, column 3

Expression 30

L_{Z}

Conventional reading: language L sub Z

Meaning here: The expression reads language L sub Z. The expression names a first-order language or one of its object-language symbols.

3 occurrences

Expression 31

{Val}^{M} (t) = f^{M} ({Val}^{M} (t_{1}), \dots, {Val}^{M} (t_{n})) .

Conventional reading: the value of t in structure M equals the interpretation of f in structure M open parenthesis the value of t sub one in structure M comma through comma the value of t sub n in structure M close parenthesis

Meaning here: The expression reads the value of t in structure M equals the interpretation of f in structure M open parenthesis the value of t sub one in structure M comma through comma the value of t sub n in structure M close parenthesis. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 24, column 3

Expression 32

M, s_{1} ⊨ C

Conventional reading: structure M under assignment s sub one satisfies C

Meaning here: The expression reads structure M under assignment s sub one satisfies C. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 138, column 29

Expression 33

M ⊨ Γ'

Conventional reading: structure M satisfies Gamma prime

Meaning here: The expression reads structure M satisfies Gamma prime. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 34

M, s_{2} ⊨ B

Conventional reading: structure M under assignment s sub two satisfies B

Meaning here: The expression reads structure M under assignment s sub two satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 35

⟨ {Val}^{M} (b), {Val}^{M} (f (a, b)) ⟩ = ⟨ 2, 3 ⟩ \in R^{M}

Conventional reading: the ordered tuple the value of b in structure M comma the value of f open parenthesis a comma b close parenthesis in structure M equals the ordered tuple two comma three is an element of the interpretation of R in structure M

Meaning here: The expression reads the ordered tuple the value of b in structure M comma the value of f open parenthesis a comma b close parenthesis in structure M equals the ordered tuple two comma three is an element of the interpretation of R in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 211, column 38

Expression 36

Γ' ⊨ A

Conventional reading: Gamma prime semantically entails A

Meaning here: The expression reads Gamma prime semantically entails A. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

2 occurrences

Expression 37

s_{1}' = s_{1} [m / x]

Conventional reading: s sub one prime equals assignment s sub one updated to send variable x to object m

Meaning here: The expression reads s sub one prime equals assignment s sub one updated to send variable x to object m. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 162, column 11

Expression 38

s (x) = 1

Conventional reading: s open parenthesis x close parenthesis equals one

Meaning here: The expression reads s open parenthesis x close parenthesis equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

2 occurrences

Expression 39

M_{2}

Conventional reading: structure M sub two

Meaning here: The expression reads structure M sub two. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 53, column 49

Expression 40

M, s_{2} ⊨ t_{1} = t_{2}

Conventional reading: structure M under assignment s sub two satisfies t sub one equals t sub two

Meaning here: The expression reads structure M under assignment s sub two satisfies t sub one equals t sub two. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 104, column 8

Expression 41

n

Conventional reading: metavariable n

Meaning here: The exact occurrence authority distinguishes n as an arity, an index bound, a natural number, or a domain witness in its local packet.

7 occurrences

Expression 42

m = 2

Conventional reading: m equals two

Meaning here: The expression reads m equals two. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 331, column 5

Expression 43

Γ ⊨ A \to B

Conventional reading: Gamma semantically entails A implies B

Meaning here: The expression reads Gamma semantically entails A implies B. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

3 occurrences

Expression 44

{Val}^{M} (c) = c^{M}

Conventional reading: the value of c in structure M equals the interpretation of c in structure M

Meaning here: The expression reads the value of c in structure M equals the interpretation of c in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 22, column 49

Expression 45

⟨ 1, 3 ⟩ \notin R^{M}

Conventional reading: the ordered pair one comma three is not an element of the interpretation of R in structure M

Meaning here: The expression reads the ordered pair one comma three is not an element of the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 213, column 35

Expression 46

{Val}_{s_{1}}^{M} (t_{1}) = {Val}_{s_{1}}^{M} (t_{2})

Conventional reading: the value of t sub one in structure M under assignment s sub one equals the value of t sub two in structure M under assignment s sub one

Meaning here: The expression reads the value of t sub one in structure M under assignment s sub one equals the value of t sub two in structure M under assignment s sub one. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 95, column 10

Expression 47

'^{N} (n) = n + 1

Conventional reading: the interpretation of object language symbol prime in structure N open parenthesis n close parenthesis equals n plus one

Meaning here: The expression reads the interpretation of object language symbol prime in structure N open parenthesis n close parenthesis equals n plus one. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 57, column 7

Expression 48

{Val}_{s}^{M} (t) = f^{M} ({Val}_{s}^{M} (t_{1}), \dots, {Val}_{s}^{M} (t_{n})) .

Conventional reading: the value of t in structure M under assignment s equals the interpretation of f in structure M applied to the values of t sub one through t sub n under assignment s

Meaning here: In the compound-term case, t is the term formed by applying f to t sub one through t sub n, and its value is obtained by applying the interpretation of f to their values.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 67, column 1

Expression 49

t = f (t_{1}, \dots, t_{k})

Conventional reading: t equals f of t sub one comma and so on comma t sub k

Meaning here: The expression reads t equals f of t sub one comma and so on comma t sub k. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 42, column 37

Expression 50

s (x) = {Val}^{M} (t)

Conventional reading: s open parenthesis x close parenthesis equals the value of t in structure M

Meaning here: The expression reads s open parenthesis x close parenthesis equals the value of t in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 137, column 34

Expression 51

'^{M} : | M | \to | M |

Conventional reading: the interpretation of successor in structure M is a function from the domain of M to the domain of M

Meaning here: This is the exact unary function type of the interpreted successor symbol in the arithmetic structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 48, column 3

Expression 52

\begin{matrix} M, s ⊨ R (a, a) \to (R (b, x) \lor R (x, b)) iff \\ M, s ⊭ R (a, a) or M, s ⊨ R (b, x) \lor R (x, b) Since M, s ⊨ R (a, a) (because ⟨ 1, 1 ⟩ \in R^{M}) we can't yet determine the answer and must first figure out if M, s ⊨ R (b, x) \lor R (x, b) : & M, s ⊨ R (b, x) \lor R (x, b) iff \\ M, s ⊨ R (b, x) or M, s ⊨ R (x, b) And this is the case, since M, s ⊨ R (x, b) (because ⟨ 1, 2 ⟩ \in R^{M}). \end{matrix}

Conventional reading: structure M satisfies the conditional with antecedent R of a comma a and consequent open scope R of b comma x or R of x comma b close scope under assignment s if and only if the antecedent is not satisfied or the consequent is satisfied; the antecedent is satisfied because ordered pair one comma one belongs to the interpretation of R; the consequent is satisfied because R of x comma b is satisfied and ordered pair one comma two belongs to the interpretation of R

Meaning here: This worked calculation applies the satisfaction clauses for implication and disjunction, then verifies the consequent from the interpreted relation, so the conditional is satisfied under assignment s.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 219, column 1

Expression 53

M

Conventional reading: structure M

Meaning here: The expression reads structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

38 occurrences

Expression 54

R (t_{1}, \dots, t_{k})

Conventional reading: atomic formula R of t sub one through t sub k

Meaning here: This is an atomic formula formed by applying the k-place predicate R to the ordered list of terms from t sub one through t sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 68, column 1

Expression 55

N

Conventional reading: structure N

Meaning here: The expression reads structure N. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

2 occurrences

Expression 56

M ⊩ A

Conventional reading: structure M makes true A

Meaning here: The expression reads structure M makes true A. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

5 occurrences

Expression 57

s_{1} (x_{i}) = s_{2} (x_{i})

Conventional reading: s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis

Meaning here: The expression reads s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 195, column 5

Expression 58

f

Conventional reading: function symbol f

Meaning here: The letter f names the function symbol whose arity and interpretation are fixed by the surrounding structure or induction case.

4 occurrences

Expression 59

| M_{1} | = | M_{2} |

Conventional reading: the domain of structure M sub one equals the domain of structure M sub two

Meaning here: The expression reads the domain of structure M sub one equals the domain of structure M sub two. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

2 occurrences

Expression 60

c^{M} \in | M |

Conventional reading: the interpretation of c in structure M is an element of the domain of structure M

Meaning here: The expression reads the interpretation of c in structure M is an element of the domain of structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 34, column 28

Expression 61

Γ \cup {A} ⊨ B

Conventional reading: Gamma union open brace A close brace semantically entails B

Meaning here: The expression reads Gamma union open brace A close brace semantically entails B. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 107, column 1

Expression 62

M ⊩ A

Conventional reading: structure M makes true A

Meaning here: The expression reads structure M makes true A. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 284, column 1

Expression 63

{Val}_{s}^{M} (t) = c^{M} .

Conventional reading: the value of t in structure M under assignment s equals the interpretation of constant c in structure M

Meaning here: The enclosing induction case binds t to the constant term c, so the value of t is the interpretation of c in M.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 64, column 22

Expression 64

M, s ⊨ C

Conventional reading: structure M under assignment s satisfies C

Meaning here: The expression reads structure M under assignment s satisfies C. This is a first-order satisfaction claim in the displayed structure and assignment context.

3 occurrences

Expression 65

R^{M_{1}} = R^{M_{2}}

Conventional reading: the interpretation of R in structure M sub one equals the interpretation of R in structure M sub two

Meaning here: The expression reads the interpretation of R in structure M sub one equals the interpretation of R in structure M sub two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 33, column 40

Expression 66

\times^{N} (n, m) = n \cdot m

Conventional reading: the interpretation of object language symbol times in structure N open parenthesis n comma m close parenthesis equals n times m

Meaning here: The expression reads the interpretation of object language symbol times in structure N open parenthesis n comma m close parenthesis equals n times m. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 59, column 7

Expression 67

M ⊨ A \to B

Conventional reading: structure M satisfies A implies B

Meaning here: The expression reads structure M satisfies A implies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 68

c_{1}

Conventional reading: c sub one

Meaning here: The exact occurrence authority distinguishes the first domain component from the first fresh constant symbol.

2 occurrences

Expression 69

m = 3

Conventional reading: m equals three

Meaning here: The expression reads m equals three. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 348, column 41

Expression 70

M, s ⊨ A

Conventional reading: structure M under assignment s satisfies A

Meaning here: The expression reads structure M under assignment s satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

8 occurrences

Expression 71

M, s ⊨ A [t' / x]

Conventional reading: structure M under assignment s satisfies A with t prime substituted for variable x

Meaning here: The expression reads structure M under assignment s satisfies A with t prime substituted for variable x. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 107, column 18

Expression 72

x

Conventional reading: variable x

Meaning here: The letter x is the displayed variable, except in the two quoted relation examples where it informally ranges over objects.

23 occurrences

Expression 73

a \in | M |

Conventional reading: a is an element of the domain of structure M

Meaning here: The expression reads a is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 322, column 9

Expression 74

c

Conventional reading: constant symbol c

Meaning here: The letter c names a first-order constant symbol, including the fresh-constant substitution cases.

7 occurrences

Expression 75

s_{1} (x_{i}) = s_{2} (x_{i})

Conventional reading: s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis

Meaning here: The expression reads s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

4 occurrences

Expression 76

M ⊩ C

Conventional reading: structure M makes true C

Meaning here: The expression reads structure M makes true C. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 313, column 36

Expression 77

| M |

Conventional reading: the domain of structure M

Meaning here: The expression reads the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

2 occurrences

Expression 78

M ⊨ B (m)

Conventional reading: structure M satisfies B open parenthesis m close parenthesis

Meaning here: The expression reads structure M satisfies B open parenthesis m close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 79

\times

Conventional reading: multiplication function symbol

Meaning here: This is the binary multiplication symbol in the arithmetic language.

2 occurrences

Expression 80

{one}^{M} = 1

Conventional reading: the interpretation of object language symbol one in structure M equals one

Meaning here: The expression reads the interpretation of object language symbol one in structure M equals one. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 42, column 1

Expression 81

M ⊨ B

Conventional reading: structure M satisfies B

Meaning here: The expression reads structure M satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

3 occurrences

Expression 82

M ⊨ Γ \cup {A}

Conventional reading: structure M satisfies Gamma union open brace A close brace

Meaning here: The expression reads structure M satisfies Gamma union open brace A close brace. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 83

x + y \leq 3

Conventional reading: x plus y is less than or equal to three

Meaning here: This inequality is the first case condition in the piecewise interpretation of the function symbol f.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 187, column 38

Expression 84

⟨ 1, 1 ⟩ \in R^{M}

Conventional reading: the ordered tuple one comma one is an element of the interpretation of R in structure M

Meaning here: The expression reads the ordered tuple one comma one is an element of the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 335, column 39

Expression 85

R (t_{1}, t_{2})

Conventional reading: atomic formula R of t sub one comma t sub two

Meaning here: This is the atomic formula obtained by applying binary predicate R to the first and second terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 208, column 23

Expression 86

b

Conventional reading: constant symbol b

Meaning here: The letter b names the second constant symbol in the worked first-order structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 180, column 47

Expression 87

f^{M} : {| M |}^{n} \to | M |

Conventional reading: the interpretation of f in structure M is a function from n tuples of elements of the domain of M to the domain of M

Meaning here: This is the exact type of the interpretation of an n place function symbol.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 39, column 57

Expression 88

{Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (x) = {Val}_{s}^{M} (t')

Conventional reading: the value of x in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s equals the value of t prime in structure M under assignment s

Meaning here: The expression reads the value of x in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s equals the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 83, column 3

Expression 89

\exists x (A (x) \lor \neg A (x))

Conventional reading: there exists x, open parenthesis A open parenthesis x close parenthesis or not A open parenthesis x close parenthesis close parenthesis

Meaning here: The expression reads there exists x, open parenthesis A open parenthesis x close parenthesis or not A open parenthesis x close parenthesis close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 98, column 17

Expression 90

M, s_{2} ⊭ A

Conventional reading: structure M under assignment s sub two does not satisfy A

Meaning here: The expression reads structure M under assignment s sub two does not satisfy A. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 80, column 5

Expression 91

M [a / c]

Conventional reading: the c expanded structure M in which constant c denotes a

Meaning here: This notation names the structure like M except that constant c is reinterpreted as domain element a; it is not a variable assignment or division.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 282, column 8

Expression 92

M

Conventional reading: structure M

Meaning here: The expression reads structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

14 occurrences

Expression 93

M, s_{2} ⊨ C

Conventional reading: structure M under assignment s sub two satisfies C

Meaning here: The expression reads structure M under assignment s sub two satisfies C. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 139, column 29

Expression 94

M, s [1 / x] ⊨ \exists y R (x, y)

Conventional reading: structure M under assignment s updated to send variable x to object one satisfies there exists y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object one satisfies there exists y, R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 331, column 18

Expression 95

s [3 / x]

Conventional reading: assignment s updated to send variable x to object three

Meaning here: The expression reads assignment s updated to send variable x to object three. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 254, column 4

Expression 96

M, s_{1} ⊨ A

Conventional reading: structure M under assignment s sub one satisfies A

Meaning here: The expression reads structure M under assignment s sub one satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 97

Γ \subseteq Γ'

Conventional reading: Gamma is a subset of Gamma prime

Meaning here: The expression reads Gamma is a subset of Gamma prime. This membership or inclusion claim is evaluated using the displayed domain, relation, or set.

2 occurrences

Expression 98

M, s [m / x] ⊭ R (x, a)

Conventional reading: structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis x comma a close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis x comma a close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 269, column 3

Expression 99

s_{2} (y) = 1

Conventional reading: s sub two open parenthesis y close parenthesis equals one

Meaning here: The expression reads s sub two open parenthesis y close parenthesis equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 342, column 5

Expression 100

M, s ⊭ \forall x (R (a, x) \to R (x, a))

Conventional reading: structure M under assignment s does not satisfy for every x, open parenthesis R open parenthesis a comma x close parenthesis implies R open parenthesis x comma a close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s does not satisfy for every x, open parenthesis R open parenthesis a comma x close parenthesis implies R open parenthesis x comma a close parenthesis close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 271, column 3

Expression 101

Γ ⊨ ⊥

Conventional reading: Gamma semantically entails contradiction

Meaning here: The expression reads Gamma semantically entails contradiction. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 84, column 17

Expression 102

M, s' ⊨ A

Conventional reading: structure M under assignment s prime satisfies A

Meaning here: The expression reads structure M under assignment s prime satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 103

{Val}_{s_{1}}^{M} (t) = {Val}_{s_{2}}^{M} (t)

Conventional reading: the value of t in structure M under assignment s sub one equals the value of t in structure M under assignment s sub two

Meaning here: The expression reads the value of t in structure M under assignment s sub one equals the value of t in structure M under assignment s sub two. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 31, column 53

Expression 104

4

Conventional reading: number four

Meaning here: Four is a displayed member of the finite domain and an assignment value in the worked model.

3 occurrences

Expression 105

M, s_{1} ⊭ A

Conventional reading: structure M under assignment s sub one does not satisfy A

Meaning here: The expression reads structure M under assignment s sub one does not satisfy A. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 79, column 30

Expression 106

M ⊭ A

Conventional reading: structure M does not satisfy A

Meaning here: The expression reads structure M does not satisfy A. This is a negative satisfaction claim in the displayed structure and assignment context.

3 occurrences

Expression 107

\begin{matrix} {Val}_{s_{2}}^{M} (t_{1}) & = {Val}_{s_{1}}^{M} (t_{1}) & (by cited result) \\ = {Val}_{s_{1}}^{M} (t_{2}) & (since M, s_{1} ⊨ t_{1} = t_{2}) \\ = {Val}_{s_{2}}^{M} (t_{2}) & (by cited result), \end{matrix}

Conventional reading: the value of t sub one under assignment s sub two equals its value under s sub one by value independence; that equals the value of t sub two under s sub one because structure M satisfies their identity there; and that equals the value of t sub two under s sub two by value independence

Meaning here: This equality chain transports equality of two term values from assignment s sub one to assignment s sub two using the term-value independence proposition on both sides.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 96, column 5

Expression 108

v

Conventional reading: variable v

Meaning here: The letter v denotes an arbitrary variable when defining agreement between assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 410, column 42

Expression 109

M, s [m / x] ⊨ B

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies B

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 110

3

Conventional reading: number three

Meaning here: Three is the displayed domain element and upper value used in the worked interpretation.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 268, column 43

Expression 111

s_{2} = s [2 / x]

Conventional reading: s sub two equals assignment s updated to send variable x to object two

Meaning here: The expression reads s sub two equals assignment s updated to send variable x to object two. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 341, column 4

Expression 112

\times

Conventional reading: object language symbol times

Meaning here: The expression reads object language symbol times. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 70, column 30

Expression 113

| M | = {1, 2, 3, 4}

Conventional reading: the domain of structure M equals open brace one comma two comma three comma four close brace

Meaning here: The expression reads the domain of structure M equals open brace one comma two comma three comma four close brace. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 184, column 7

Expression 114

f^{M} (1) = 2, f^{M} (2) = 3, f^{M} (3) = 2

Conventional reading: the interpretation of f in structure M open parenthesis one close parenthesis equals two comma the interpretation of f in structure M open parenthesis two close parenthesis equals three comma the interpretation of f in structure M open parenthesis three close parenthesis equals two

Meaning here: The expression reads the interpretation of f in structure M open parenthesis one close parenthesis equals two comma the interpretation of f in structure M open parenthesis two close parenthesis equals three comma the interpretation of f in structure M open parenthesis three close parenthesis equals two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 407, column 7

Expression 115

⊤

Conventional reading: truth constant

Meaning here: This is the logical truth constant, which is satisfied in every structure under every assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 56, column 24

Expression 116

n \geq m

Conventional reading: n is greater than or equal to m

Meaning here: This relation on natural numbers is offered as a possible interpretation of the set-theory membership predicate.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 80, column 6

Expression 117

s_{2}

Conventional reading: variable assignment s sub two

Meaning here: The letter s sub two names the second assignment in the current argument; its exact relationship to other assignments is supplied by the local occurrence.

2 occurrences

Expression 118

B (m)

Conventional reading: formula B with argument m

Meaning here: This is the instance of formula B obtained by placing domain element m in the displayed argument position.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 159, column 56

Expression 119

M [a_{1} / c_{1}, \dots, a_{n} / c_{n}] ⊩ A [c_{1} / x_{1}] \dots [c_{n} / x_{n}]

Conventional reading: the expanded structure M in which constants c sub one through c sub n denote a sub one through a sub n makes true A with each c sub i substituted for x sub i

Meaning here: The structure expands M by interpreting each fresh constant c sub i as a sub i, and the displayed truth claim uses the corresponding simultaneous sequence of substitutions.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 335, column 32

Expression 120

M ⊩ A

Conventional reading: structure M makes true A

Meaning here: The expression reads structure M makes true A. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

2 occurrences

Expression 121

Γ

Conventional reading: Gamma

Meaning here: Gamma denotes the current set of first-order sentences used as premises or as a satisfiability target.

12 occurrences

Expression 122

s_{1}' (x) = s_{2}' (x) = m

Conventional reading: s sub one prime open parenthesis x close parenthesis equals s sub two prime open parenthesis x close parenthesis equals m

Meaning here: The expression reads s sub one prime open parenthesis x close parenthesis equals s sub two prime open parenthesis x close parenthesis equals m. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 166, column 41

Expression 123

one

Conventional reading: object language symbol one

Meaning here: The expression reads object language symbol one. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 38, column 1

Expression 124

s (x_{i}) = a_{i}

Conventional reading: s open parenthesis x sub i close parenthesis equals a sub i

Meaning here: The expression reads s open parenthesis x sub i close parenthesis equals a sub i. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 333, column 40

Expression 125

t = c

Conventional reading: t equals c

Meaning here: The expression reads t equals c. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 37, column 64

Expression 126

M, s [1 / x] ⊨ R (b, x) \lor R (x, b)

Conventional reading: structure M under assignment s updated to send variable x to object one satisfies R open parenthesis b comma x close parenthesis or R open parenthesis x comma b close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object one satisfies R open parenthesis b comma x close parenthesis or R open parenthesis x comma b close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 253, column 9

Expression 127

'

Conventional reading: object language symbol prime

Meaning here: The expression reads object language symbol prime. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 70, column 5

Expression 128

<^{M} \subseteq {| M |}^{2}

Conventional reading: the interpretation of object language symbol less than in structure M is a subset of the domain of structure M superscript two

Meaning here: The expression reads the interpretation of object language symbol less than in structure M is a subset of the domain of structure M superscript two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 51, column 12

Expression 129

M_{1} ⊨ A

Conventional reading: structure M sub one satisfies A

Meaning here: The expression reads structure M sub one satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 54, column 37

Expression 130

n \in ℕ

Conventional reading: n is an element of the natural numbers

Meaning here: The expression reads n is an element of the natural numbers. This membership or inclusion claim is evaluated using the displayed domain, relation, or set.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 57, column 52

Expression 131

t_{2}

Conventional reading: term t sub two

Meaning here: This is the second term in an atomic identity or predicate application.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 69, column 61

Expression 132

\begin{matrix} {Val}^{M} (\times (two, + (three, zero))) = \\ \begin{matrix} = \times^{M} ({Val}^{M} (two), {Val}^{M} (+ (three, zero))) \\ = \times^{M} ({Val}^{M} (two), +^{M} ({Val}^{M} (three), {Val}^{M} (zero))) \\ = \times^{M} ({two}^{M}, +^{M} ({three}^{M}, {zero}^{M})) \\ = \times^{M} (2, +^{M} (3, 0)) \\ = \times^{M} (2, 3) \\ = 6 \end{matrix} \end{matrix}

Conventional reading: the value in structure M of the product of object-language two and the sum of object-language three and object-language zero is expanded by the recursive term-value definition; the constants denote two three and zero; the inner sum denotes three; and the outer product denotes six

Meaning here: This display evaluates the closed arithmetic term from the inside out and concludes that its value in structure M is six.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 53, column 1

Expression 133

s'

Conventional reading: variable assignment s prime

Meaning here: The letter s prime names a second variable assignment, often an x variant of s.

5 occurrences

Expression 134

{Val}_{s}^{M} (t_{1}) = {Val}_{s}^{M} (t_{2})

Conventional reading: the value of t sub one in structure M under assignment s equals the value of t sub two in structure M under assignment s

Meaning here: The expression reads the value of t sub one in structure M under assignment s equals the value of t sub two in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 119, column 3

Expression 135

ℤ

Conventional reading: the set of integers

Meaning here: This symbol denotes the integers in the explanatory comparison between structures and intended domains.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 68, column 57

Expression 136

R^{M} = {⟨ 1, 1 ⟩, ⟨ 1, 2 ⟩, ⟨ 2, 3 ⟩, ⟨ 2, 4 ⟩}

Conventional reading: the interpretation of R in structure M equals open brace the ordered tuple one comma one comma the ordered tuple one comma two comma the ordered tuple two comma three comma the ordered tuple two comma four close brace

Meaning here: The expression reads the interpretation of R in structure M equals open brace the ordered tuple one comma one comma the ordered tuple one comma two comma the ordered tuple two comma three comma the ordered tuple two comma four close brace. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 188, column 7

Expression 137

⟨ {Val}_{s_{1}}^{M} (t_{1}), \dots, {Val}_{s_{1}}^{M} (t_{k}) ⟩ \in R^{M} .

Conventional reading: open angle bracket the value of t sub one in structure M under assignment s sub one comma through comma the value of t sub k in structure M under assignment s sub one close angle bracket is an element of the interpretation of R in structure M

Meaning here: The expression reads open angle bracket the value of t sub one in structure M under assignment s sub one comma through comma the value of t sub k in structure M under assignment s sub one close angle bracket is an element of the interpretation of R in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 85, column 5

Expression 138

m

Conventional reading: domain element m

Meaning here: The letter m denotes the domain element used to update an assignment or instantiate a quantified formula.

2 occurrences

Expression 139

M ⊩ B

Conventional reading: structure M makes true B

Meaning here: The expression reads structure M makes true B. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 305, column 18

Expression 140

M, s_{2}' ⊨ B

Conventional reading: structure M under assignment s sub two prime satisfies B

Meaning here: The expression reads structure M under assignment s sub two prime satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 169, column 7

Expression 141

{Val}_{s}^{M} (c) = c^{M} = {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (c)

Conventional reading: the value of c in structure M under assignment s equals the interpretation of c in structure M equals the value of c in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s

Meaning here: The expression reads the value of c in structure M under assignment s equals the interpretation of c in structure M equals the value of c in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 74, column 11

Expression 142

B [m / x]

Conventional reading: B with m substituted for variable x

Meaning here: The expression reads B with m substituted for variable x. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 160, column 24

Expression 143

M, s ⊭ R (x, f (a, b))

Conventional reading: structure M under assignment s does not satisfy R open parenthesis x comma f open parenthesis a comma b close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s does not satisfy R open parenthesis x comma f open parenthesis a comma b close parenthesis close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 213, column 1

Expression 144

+^{N} (n, m) = n + m

Conventional reading: the interpretation of object language symbol plus in structure N open parenthesis n comma m close parenthesis equals n plus m

Meaning here: The expression reads the interpretation of object language symbol plus in structure N open parenthesis n comma m close parenthesis equals n plus m. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 58, column 7

Expression 145

c_{n}

Conventional reading: fresh constant c sub n

Meaning here: This is the n-th fresh constant introduced for the free-variable replacement exercise.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 332, column 15

Expression 146

0^{N} = 0

Conventional reading: the interpretation of object language symbol zero in structure N equals zero

Meaning here: The expression reads the interpretation of object language symbol zero in structure N equals zero. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 56, column 7

Expression 147

M, s [2 / x] ⊭ R (a, x) \to R (x, a)

Conventional reading: structure M under assignment s updated to send variable x to object two does not satisfy R open parenthesis a comma x close parenthesis implies R open parenthesis x comma a close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object two does not satisfy R open parenthesis a comma x close parenthesis implies R open parenthesis x comma a close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 274, column 9

Expression 148

s : Var \to | M |

Conventional reading: s is a function from the set of variables to the domain of M

Meaning here: This is the exact type signature of a variable assignment for structure M.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 44, column 7

Expression 149

{Val}_{s}^{M} (t)

Conventional reading: the value of t in structure M under assignment s

Meaning here: The expression reads the value of t in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 61, column 39

Expression 150

M_{2}

Conventional reading: structure M sub two

Meaning here: The expression reads structure M sub two. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 30, column 51

Expression 151

M ⊭ Γ

Conventional reading: structure M does not satisfy Gamma

Meaning here: The expression reads structure M does not satisfy Gamma. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 77, column 1

Expression 152

\exists x x = a

Conventional reading: there exists x, x equals a

Meaning here: The expression reads there exists x, x equals a. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 105, column 33

Expression 153

s' \sim_{x} s

Conventional reading: assignment s prime is an x variant of assignment s

Meaning here: The expression reads assignment s prime is an x variant of assignment s. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 78, column 40

Expression 154

\begin{matrix} {Val}_{s}^{M} (f (a, b)) & = f^{M} ({Val}_{s}^{M} (a), {Val}_{s}^{M} (b)) . Since a and b are !! constant s, {Val}_{s}^{M} (a) = a^{M} = 1 and {Val}_{s}^{M} (b) = b^{M} = 2 . So {Val}_{s}^{M} (f (a, b)) & = f^{M} (1, 2) = 1 + 2 = 3 . To compute the value of f (f (a, b), a) we have to consider {Val}_{s}^{M} (f (f (a, b), a)) & = f^{M} ({Val}_{s}^{M} (f (a, b)), {Val}_{s}^{M} (a)) = f^{M} (3, 1) = 3, since 3 + 1 > 3 . Since s (x) = 1 and {Val}_{s}^{M} (x) = s (x), we also have {Val}_{s}^{M} (f (f (a, b), x)) & = f^{M} ({Val}_{s}^{M} (f (a, b)), {Val}_{s}^{M} (x)) = f^{M} (3, 1) = 3, \end{matrix}

Conventional reading: the value of f of a comma b under assignment s is the interpretation of f applied to the values of a and b and therefore is three; the value of f of f of a comma b comma a is three; because x also has value one under s the value of f of f of a comma b comma x is likewise three

Meaning here: This worked display recursively evaluates three function terms in the finite structure, using the interpretations of a, b, f, and assignment s.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 194, column 1

Expression 155

⟨ c_{1}, c_{2} ⟩ \in {| M |}^{2}

Conventional reading: the ordered tuple c sub one comma c sub two is an element of the domain of structure M superscript two

Meaning here: The expression reads the ordered tuple c sub one comma c sub two is an element of the domain of structure M superscript two. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 44, column 22

Expression 156

M, s [2 / x] ⊭ R (x, a)

Conventional reading: structure M under assignment s updated to send variable x to object two does not satisfy R open parenthesis x comma a close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object two does not satisfy R open parenthesis x comma a close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 275, column 43

Expression 157

c^{M [a / c]} = a

Conventional reading: the interpretation of c in the c expanded structure M equals a

Meaning here: The c expanded structure is like M except that it interprets constant c as domain element a.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 283, column 31

Expression 158

s_{2}'

Conventional reading: variable assignment s sub two prime

Meaning here: This is the x variant of s sub two used in the induction argument for satisfaction independence.

3 occurrences

Expression 159

M ⊨ Γ \cup {\neg A}

Conventional reading: structure M satisfies Gamma union open brace not A close brace

Meaning here: The expression reads structure M satisfies Gamma union open brace not A close brace. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 68, column 59

Expression 160

\forall x A (x)

Conventional reading: for every x, A open parenthesis x close parenthesis

Meaning here: The expression reads for every x, A open parenthesis x close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 261, column 15

Expression 161

n \in | M |

Conventional reading: n is an element of the domain of structure M

Meaning here: The expression reads n is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

3 occurrences

Expression 162

M ⊨ Γ \cup {\neg A}

Conventional reading: structure M satisfies Gamma union open brace not A close brace

Meaning here: The expression reads structure M satisfies Gamma union open brace not A close brace. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 70, column 33

Expression 163

s [{Val}_{s}^{M} (t') / x]

Conventional reading: assignment s updated to send variable x to object the value of t prime in structure M under assignment s

Meaning here: The expression reads assignment s updated to send variable x to object the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 84, column 17

Expression 164

=

Conventional reading: identity predicate

Meaning here: This is the logical identity predicate of first-order logic.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 36, column 47

Expression 165

<^{N} = {⟨ n, m ⟩ : n \in ℕ, m \in ℕ, n < m}

Conventional reading: the interpretation of object language symbol less than in structure N equals the set of the ordered tuple n comma m such that n is an element of the natural numbers comma m is an element of the natural numbers comma n less than m

Meaning here: The expression reads the interpretation of object language symbol less than in structure N equals the set of the ordered tuple n comma m such that n is an element of the natural numbers comma m is an element of the natural numbers comma n less than m. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 60, column 7

Expression 166

s_{2} (y) = s (y) = 1

Conventional reading: s sub two open parenthesis y close parenthesis equals s open parenthesis y close parenthesis equals one

Meaning here: The expression reads s sub two open parenthesis y close parenthesis equals s open parenthesis y close parenthesis equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 241, column 28

Expression 167

M_{1}, s ⊨ A

Conventional reading: structure M sub one under assignment s satisfies A

Meaning here: The expression reads structure M sub one under assignment s satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 36, column 3

Expression 168

t'

Conventional reading: substitution term t prime

Meaning here: The term t prime is the term substituted for variable x in the extensionality propositions.

4 occurrences

Expression 169

s_{1}

Conventional reading: variable assignment s sub one

Meaning here: The letter s sub one names the first assignment in the current argument; its exact relationship to other assignments is supplied by the local occurrence.

2 occurrences

Expression 170

M ⊨ \forall x A (x)

Conventional reading: structure M satisfies for every x, A open parenthesis x close parenthesis

Meaning here: The expression reads structure M satisfies for every x, A open parenthesis x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 265, column 22

Expression 171

M' ⊨ \forall x A (x, f (x))

Conventional reading: structure M prime satisfies for every x, A open parenthesis x comma f open parenthesis x close parenthesis close parenthesis

Meaning here: The expression reads structure M prime satisfies for every x, A open parenthesis x comma f open parenthesis x close parenthesis close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 346, column 15

Expression 172

M_{1}

Conventional reading: structure M sub one

Meaning here: The expression reads structure M sub one. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 30, column 33

Expression 173

ℕ

Conventional reading: the natural numbers

Meaning here: This symbol denotes the natural-number domain of the standard arithmetic structure.

2 occurrences

Expression 174

M, s_{2} [m / x] ⊨ B

Conventional reading: structure M under assignment s sub two updated to send variable x to object m satisfies B

Meaning here: The expression reads structure M under assignment s sub two updated to send variable x to object m satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 171, column 7

Expression 175

M, s ⊭ \exists x (R (b, x) \land R (x, b))

Conventional reading: structure M under assignment s does not satisfy there exists x, open parenthesis R open parenthesis b comma x close parenthesis and R open parenthesis x comma b close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s does not satisfy there exists x, open parenthesis R open parenthesis b comma x close parenthesis and R open parenthesis x comma b close parenthesis close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 255, column 3

Expression 176

s (y) = 1

Conventional reading: s open parenthesis y close parenthesis equals one

Meaning here: The expression reads s open parenthesis y close parenthesis equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 335, column 23

Expression 177

Γ \cup {A} ⊨ ⊥

Conventional reading: Gamma union open brace A close brace semantically entails contradiction

Meaning here: The expression reads Gamma union open brace A close brace semantically entails contradiction. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 85, column 17

Expression 178

M, s ⊭ B

Conventional reading: structure M under assignment s does not satisfy B

Meaning here: The expression reads structure M under assignment s does not satisfy B. This is a negative satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 179

\times (two, + (three, zero))

Conventional reading: times open parenthesis object language symbol two comma plus open parenthesis object language symbol three comma object language symbol zero close parenthesis close parenthesis

Meaning here: The expression reads times open parenthesis object language symbol two comma plus open parenthesis object language symbol three comma object language symbol zero close parenthesis close parenthesis. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 50, column 32

Expression 180

M [a / c] ⊩ B [c / x]

Conventional reading: the c expanded structure M in which c denotes a makes true B with c substituted for x

Meaning here: The truth claim is evaluated in the structure obtained by reinterpreting fresh constant c as a, not under a variable assignment and not by division.

2 occurrences

Expression 181

f^{M_{1}} = f^{M_{2}}

Conventional reading: the interpretation of f in structure M sub one equals the interpretation of f in structure M sub two

Meaning here: The expression reads the interpretation of f in structure M sub one equals the interpretation of f in structure M sub two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 34, column 7

Expression 182

{zero}^{M} = 0

Conventional reading: the interpretation of object language symbol zero in structure M equals zero

Meaning here: The expression reads the interpretation of object language symbol zero in structure M equals zero. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 41, column 21

Expression 183

{Val}_{s_{1}}^{M} (t) = c^{M} = {Val}_{s_{2}}^{M} (t)

Conventional reading: the value of t in structure M under assignment s sub one equals the interpretation of c in structure M equals the value of t in structure M under assignment s sub two

Meaning here: The expression reads the value of t in structure M under assignment s sub one equals the interpretation of c in structure M equals the value of t in structure M under assignment s sub two. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 38, column 12

Expression 184

A (x)

Conventional reading: formula A with free variable x

Meaning here: This notation presents formula A with x as its sole displayed free variable.

2 occurrences

Expression 185

M, s [m / x] ⊭ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m does not satisfy R open parenthesis a comma x close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 348, column 1

Expression 186

| M | = {0, 1, 2, \dots}

Conventional reading: the domain of structure M equals open brace zero comma one comma two comma through close brace

Meaning here: The expression reads the domain of structure M equals open brace zero comma one comma two comma through close brace. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 40, column 41

Expression 187

A

Conventional reading: formula A

Meaning here: A denotes the formula or, where explicitly stated, the sentence under semantic evaluation.

49 occurrences

Expression 188

k

Conventional reading: arity k

Meaning here: The letter k is the finite arity and the last index in the displayed term list.

2 occurrences

Expression 189

+^{M} (2, 3)

Conventional reading: the interpretation of plus in structure M open parenthesis two comma three close parenthesis

Meaning here: The expression reads the interpretation of plus in structure M open parenthesis two comma three close parenthesis. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 48, column 10

Expression 190

M ⊩ B

Conventional reading: structure M makes true B

Meaning here: The expression reads structure M makes true B. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 301, column 9

Expression 191

t_{k}

Conventional reading: term t sub k

Meaning here: This is the final term in the k-term argument list.

2 occurrences

Expression 192

zero

Conventional reading: object language symbol zero

Meaning here: The expression reads object language symbol zero. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 37, column 51

Expression 193

M_{1}

Conventional reading: structure M sub one

Meaning here: The expression reads structure M sub one. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 53, column 33

Expression 194

M, s ⊭ A

Conventional reading: structure M under assignment s does not satisfy A

Meaning here: The expression reads structure M under assignment s does not satisfy A. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 109, column 25

Expression 195

M, s [m / x] ⊨ \exists y R (x, y)

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies there exists y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies there exists y, R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 349, column 1

Expression 196

R

Conventional reading: predicate symbol R

Meaning here: The letter R names the predicate whose arity and interpretation are fixed by the surrounding structure or atomic case.

4 occurrences

Expression 197

a \in | M |

Conventional reading: a is an element of the domain of structure M

Meaning here: The expression reads a is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

2 occurrences

Expression 198

M, s [m / x] ⊨ A (x)

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies A open parenthesis x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies A open parenthesis x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 199

M, s_{1} ⊨ A

Conventional reading: structure M under assignment s sub one satisfies A

Meaning here: The expression reads structure M under assignment s sub one satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

5 occurrences

Expression 200

M, s ⊨ R (b, f (a, b))

Conventional reading: structure M under assignment s satisfies R open parenthesis b comma f open parenthesis a comma b close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s satisfies R open parenthesis b comma f open parenthesis a comma b close parenthesis close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 211, column 6

Expression 201

t \equiv c

Conventional reading: term t is syntactically identical to constant c

Meaning here: This is the constant base case in the induction on terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 73, column 34

Expression 202

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

Conventional reading: function term f of t sub one through t sub n

Meaning here: This compound term applies the n-place function symbol f to the ordered list of its n argument terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 23, column 29

Expression 203

1 \in | M |

Conventional reading: one is an element of the domain of structure M

Meaning here: The expression reads one is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 190, column 38

Expression 204

M, s [1 / x] ⊨ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object one satisfies R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object one satisfies R open parenthesis a comma x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 267, column 36

Expression 205

M, s [m / x] ⊨ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies R open parenthesis a comma x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 357, column 9

Expression 206

M, s [3 / x] ⊭ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object three does not satisfy R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object three does not satisfy R open parenthesis a comma x close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 328, column 7

Expression 207

M'

Conventional reading: structure M prime

Meaning here: The expression reads structure M prime. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

3 occurrences

Expression 208

a_{n} \in | M |

Conventional reading: a sub n is an element of the domain of structure M

Meaning here: The expression reads a sub n is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 333, column 15

Expression 209

t \equiv x

Conventional reading: term t is syntactically identical to variable x

Meaning here: This is the substituted-variable base case in the induction on terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 82, column 10

Expression 210

M ⊩ C

Conventional reading: structure M makes true C

Meaning here: The expression reads structure M makes true C. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

2 occurrences

Expression 211

{d_{1}}^{M} = {d_{2}}^{M}

Conventional reading: the interpretation of d sub one in structure M equals the interpretation of d sub two in structure M

Meaning here: The expression reads the interpretation of d sub one in structure M equals the interpretation of d sub two in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 297, column 3

Expression 212

\exists x B (x)

Conventional reading: there exists x, B open parenthesis x close parenthesis

Meaning here: The expression reads there exists x, B open parenthesis x close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

2 occurrences

Expression 213

| M | = {1, 2, 3, 4}

Conventional reading: the domain of structure M equals open brace one comma two comma three comma four close brace

Meaning here: The expression reads the domain of structure M equals open brace one comma two comma three comma four close brace. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 243, column 31

Expression 214

s_{1}' (x_{i}) = s_{2}' (x_{i})

Conventional reading: s sub one prime open parenthesis x sub i close parenthesis equals s sub two prime open parenthesis x sub i close parenthesis

Meaning here: The expression reads s sub one prime open parenthesis x sub i close parenthesis equals s sub two prime open parenthesis x sub i close parenthesis. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 164, column 30

Expression 215

M_{2}, s ⊨ A

Conventional reading: structure M sub two under assignment s satisfies A

Meaning here: The expression reads structure M sub two under assignment s satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 36, column 26

Expression 216

R^{M} \subseteq {| M |}^{n}

Conventional reading: the interpretation of R in structure M is a subset of the domain of structure M superscript n

Meaning here: The expression reads the interpretation of R in structure M is a subset of the domain of structure M superscript n. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 37, column 12

Expression 217

| HF | = \emptyset \cup ℘ (\emptyset) \cup ℘ (℘ (\emptyset)) \cup ℘ (℘ (℘ (\emptyset))) \cup \dots

Conventional reading: the domain of structure HF equals the empty set union the power set of the empty set union the power set of the power set of the empty set union the power set of the power set of the power set of the empty set union and so on

Meaning here: The expression reads the domain of structure HF equals the empty set union the power set of the empty set union the power set of the power set of the empty set union the power set of the power set of the power set of the empty set union and so on. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 87, column 7

Expression 218

{Val}^{M} (t)

Conventional reading: the value of t in structure M

Meaning here: The expression reads the value of t in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 19, column 51

Expression 219

Γ \cup {\neg A}

Conventional reading: Gamma union the singleton containing not A

Meaning here: This is the premise set Gamma extended by the negation of A in the unsatisfiability characterization of entailment.

2 occurrences

Expression 220

n = 4

Conventional reading: n equals four

Meaning here: The expression reads n equals four. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 359, column 20

Expression 221

Γ \cup {A} ⊨ B

Conventional reading: Gamma union open brace A close brace semantically entails B

Meaning here: The expression reads Gamma union open brace A close brace semantically entails B. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

2 occurrences

Expression 222

\forall x A (x) ⊨ A (t)

Conventional reading: for every x, A open parenthesis x close parenthesis semantically entails A open parenthesis t close parenthesis

Meaning here: The expression reads for every x, A open parenthesis x close parenthesis semantically entails A open parenthesis t close parenthesis. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 129, column 22

Expression 223

s [m / x]

Conventional reading: assignment s updated to send variable x to object m

Meaning here: The expression reads assignment s updated to send variable x to object m. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

5 occurrences

Expression 224

{Val}_{s}^{M} (t [t' / x]) = {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (t)

Conventional reading: the value of t with t prime substituted for variable x in structure M under assignment s equals the value of t in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s

Meaning here: The expression reads the value of t with t prime substituted for variable x in structure M under assignment s equals the value of t in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 66, column 27

Expression 225

⟨ {Val}_{s}^{M} (t_{1}), \dots, {Val}_{s}^{M} (t_{n}) ⟩ \in R^{M}

Conventional reading: open angle bracket the value of t sub one in structure M under assignment s comma and so on comma the value of t sub n in structure M under assignment s close angle bracket is an element of the interpretation of R in structure M

Meaning here: The expression reads open angle bracket the value of t sub one in structure M under assignment s comma and so on comma the value of t sub n in structure M under assignment s close angle bracket is an element of the interpretation of R in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 115, column 7

Expression 226

s [1 / x] [n / y] = s [1 / y] = s

Conventional reading: the assignment obtained by updating s to send x to one and then y to n equals the assignment obtained by updating s to send y to one, and both equal s

Meaning here: Both bracket operations are assignment updates; the outer update sends y to n and is not syntactic substitution.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 334, column 18

Expression 227

Γ \cup {\neg A}

Conventional reading: Gamma union the singleton containing not A

Meaning here: This is the premise set Gamma extended by the negation of A in the semantic proof.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 63, column 26

Expression 228

M, s_{1} ⊨ B

Conventional reading: structure M under assignment s sub one satisfies B

Meaning here: The expression reads structure M under assignment s sub one satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 229

t \equiv y

Conventional reading: term t is syntactically identical to variable y

Meaning here: This is the non-substituted-variable base case, where y differs from x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 77, column 49

Expression 230

⟨ {Val}_{s}^{M} (t_{1}), {Val}_{s}^{M} (t_{2}) ⟩

Conventional reading: the ordered tuple the value of t sub one in structure M under assignment s comma the value of t sub two in structure M under assignment s

Meaning here: The expression reads the ordered tuple the value of t sub one in structure M under assignment s comma the value of t sub two in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 209, column 32

Expression 231

y

Conventional reading: variable y

Meaning here: The letter y is the displayed variable, or the second informal object placeholder in a quoted binary relation.

3 occurrences

Expression 232

L = {a, b, f, R}

Conventional reading: language L equals open brace a comma b comma f comma R close brace

Meaning here: The expression reads language L equals open brace a comma b comma f comma R close brace. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 180, column 5

Expression 233

M, s [m / x] [n / y] ⊭ R (x, y)

Conventional reading: structure M under the assignment obtained by updating s to send x to m and then y to n does not satisfy R of x comma y

Meaning here: The satisfaction claim uses two successive assignment updates, first at x and then at y; neither update is syntactic substitution.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 360, column 1

Expression 234

+

Conventional reading: addition function symbol

Meaning here: This is the binary addition symbol in the arithmetic language.

2 occurrences

Expression 235

two

Conventional reading: object language symbol two

Meaning here: The expression reads object language symbol two. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 38, column 14

Expression 236

M, s [m / x] ⊨ A

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies A

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 132, column 3

Expression 237

M, s ⊭ A

Conventional reading: structure M under assignment s does not satisfy A

Meaning here: The expression reads structure M under assignment s does not satisfy A. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 106, column 1

Expression 238

M, s [2 / x] ⊨ R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object two satisfies R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object two satisfies R open parenthesis a comma x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 275, column 3

Expression 239

M ⊩ B

Conventional reading: structure M makes true B

Meaning here: The expression reads structure M makes true B. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 309, column 5

Expression 240

Γ ⊨ A

Conventional reading: Gamma semantically entails A

Meaning here: The expression reads Gamma semantically entails A. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

11 occurrences

Expression 241

M, s [m / x] ⊨ R (x, a) \to R (a, x)

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies R open parenthesis x comma a close parenthesis implies R open parenthesis a comma x close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies R open parenthesis x comma a close parenthesis implies R open parenthesis a comma x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 266, column 9

Expression 242

M, s ⊨ \forall x (R (x, a) \to R (a, x)),

Conventional reading: structure M under assignment s satisfies for every x, open parenthesis R open parenthesis x comma a close parenthesis implies R open parenthesis a comma x close parenthesis close parenthesis comma

Meaning here: The expression reads structure M under assignment s satisfies for every x, open parenthesis R open parenthesis x comma a close parenthesis implies R open parenthesis a comma x close parenthesis close parenthesis comma. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 263, column 3

Expression 243

\in

Conventional reading: object language symbol is an element of

Meaning here: The expression reads object language symbol is an element of. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 84, column 4

Expression 244

M, s [m / x] ⊨ R (a, x) \land \forall y R (x, y)

Conventional reading: structure M under assignment s updated to send variable x to object m satisfies R open parenthesis a comma x close parenthesis and for every y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m satisfies R open parenthesis a comma x close parenthesis and for every y, R open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 362, column 53

Expression 245

M ⊨ Γ

Conventional reading: structure M satisfies Gamma

Meaning here: The expression reads structure M satisfies Gamma. This is a first-order satisfaction claim in the displayed structure and assignment context.

11 occurrences

Expression 246

c^{M} = 3

Conventional reading: the interpretation of c in structure M equals three

Meaning here: The expression reads the interpretation of c in structure M equals three. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 406, column 7

Expression 247

M, s [1 / x] [n / y] ⊨ R (x, y)

Conventional reading: structure M under the assignment obtained by updating s to send x to one and then y to n satisfies R of x comma y

Meaning here: The satisfaction claim uses two successive assignment updates, first at x and then at y.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 333, column 1

Expression 248

{Val}_{s}^{M} (y) = {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (y)

Conventional reading: the value of y in structure M under assignment s equals the value of y in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s

Meaning here: The expression reads the value of y in structure M under assignment s equals the value of y in structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 78, column 31

Expression 249

A^{M} = {⟨ 1, 2 ⟩, ⟨ 2, 3 ⟩, ⟨ 3, 3 ⟩}

Conventional reading: the interpretation of A in structure M equals open brace the ordered tuple one comma two comma the ordered tuple two comma three comma the ordered tuple three comma three close brace

Meaning here: The expression reads the interpretation of A in structure M equals open brace the ordered tuple one comma two comma the ordered tuple two comma three comma the ordered tuple three comma three close brace. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 408, column 7

Expression 250

m = {Val}_{s}^{M} (t')

Conventional reading: m equals the value of t prime in structure M under assignment s

Meaning here: The expression reads m equals the value of t prime in structure M under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 128, column 33

Expression 251

c^{M_{1}} = c^{M_{2}}

Conventional reading: the interpretation of c in structure M sub one equals the interpretation of c in structure M sub two

Meaning here: The expression reads the interpretation of c in structure M sub one equals the interpretation of c in structure M sub two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 33, column 3

Expression 252

\begin{matrix} {Val}_{s_{1}}^{M} (t) & = {Val}_{s_{1}}^{M} (f (t_{1}, \dots, t_{k})) \\ = f^{M} ({Val}_{s_{1}}^{M} (t_{1}), \dots, {Val}_{s_{1}}^{M} (t_{k})) . For j = 1, \dots, k, the !! variable s of t j are among x 1, \dots, x n . By the induction hypothesis, {Val}_{s_{1}}^{M} (t_{j}) = {Val}_{s_{2}}^{M} (t_{j}) . So, {Val}_{s_{1}}^{M} (t) & = {Val}_{s_{1}}^{M} (f (t_{1}, \dots, t_{k})) \\ = f^{M} ({Val}_{s_{1}}^{M} (t_{1}), \dots, {Val}_{s_{1}}^{M} (t_{k})) \\ = f^{M} ({Val}_{s_{2}}^{M} (t_{1}), \dots, {Val}_{s_{2}}^{M} (t_{k})) \\ = {Val}_{s_{2}}^{M} (f (t_{1}, \dots, t_{k})) = {Val}_{s_{2}}^{M} (t) . \end{matrix}

Conventional reading: the value of compound term t under assignment s sub one is the interpretation of f applied to the values of its argument terms; each argument has the same value under s sub one and s sub two by the induction hypothesis; replacing every argument value therefore gives the value of t under s sub two

Meaning here: This is the compound-term induction step proving that assignments agreeing on all variables of a term give that term the same value.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 44, column 1

Expression 253

L

Conventional reading: language L

Meaning here: The expression reads language L. The expression names a first-order language or one of its object-language symbols.

4 occurrences

Expression 254

M, s ⊨ A (t)

Conventional reading: structure M under assignment s satisfies A open parenthesis t close parenthesis

Meaning here: The expression reads structure M under assignment s satisfies A open parenthesis t close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 138, column 9

Expression 255

+^{M}

Conventional reading: the interpretation of plus in structure M

Meaning here: The expression reads the interpretation of plus in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 47, column 26

Expression 256

M, s ⊨ A

Conventional reading: structure M under assignment s satisfies A

Meaning here: The expression reads structure M under assignment s satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

8 occurrences

Expression 257

{Val}_{s}^{M} (t) = s (x) .

Conventional reading: the value of t in structure M under assignment s equals s of x

Meaning here: The enclosing induction case binds t to variable x, so the value of t is the element assigned to x by s.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 65, column 22

Expression 258

Γ ⊨ A [c / x]

Conventional reading: Gamma semantically entails A with c substituted for variable x

Meaning here: The expression reads Gamma semantically entails A with c substituted for variable x. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 87, column 41

Expression 259

s_{1} = s

Conventional reading: s sub one equals s

Meaning here: The expression reads s sub one equals s. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 244, column 18

Expression 260

{Val}_{s_{1}}^{M} (t_{i}) = {Val}_{s_{2}}^{M} (t_{i})

Conventional reading: the value of t sub i in structure M under assignment s sub one equals the value of t sub i in structure M under assignment s sub two

Meaning here: The expression reads the value of t sub i in structure M under assignment s sub one equals the value of t sub i in structure M under assignment s sub two. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 89, column 30

Expression 261

A \in Γ

Conventional reading: A is an element of Gamma

Meaning here: The expression reads A is an element of Gamma. This membership or inclusion claim is evaluated using the displayed domain, relation, or set.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 243, column 46

Expression 262

s [2 / x] [3 / y] = s_{2} [3 / y]

Conventional reading: the assignment obtained by updating s to send x to two and then y to three equals assignment s sub two updated to send y to three

Meaning here: Both sides denote the same nested assignment update; the outer brackets send y to three.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 343, column 10

Expression 263

t_{1}

Conventional reading: term t sub one

Meaning here: This is the first term in the displayed finite argument list.

3 occurrences

Expression 264

M, s ⊨ B

Conventional reading: structure M under assignment s satisfies B

Meaning here: The expression reads structure M under assignment s satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 265

s_{2}' = s_{2} [m / x]

Conventional reading: s sub two prime equals assignment s sub two updated to send variable x to object m

Meaning here: The expression reads s sub two prime equals assignment s sub two updated to send variable x to object m. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

2 occurrences

Expression 266

M, s_{1} ⊭ B

Conventional reading: structure M under assignment s sub one does not satisfy B

Meaning here: The expression reads structure M under assignment s sub one does not satisfy B. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 123, column 7

Expression 267

M, s ⊨ \exists x (A (f (z), c) \to \forall y (A (y, x) \lor A (f (y), x)))

Conventional reading: structure M under assignment s satisfies there exists x, open parenthesis A open parenthesis f open parenthesis z close parenthesis comma c close parenthesis implies for every y, open parenthesis A open parenthesis y comma x close parenthesis or A open parenthesis f open parenthesis y close parenthesis comma x close parenthesis close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s satisfies there exists x, open parenthesis A open parenthesis f open parenthesis z close parenthesis comma c close parenthesis implies for every y, open parenthesis A open parenthesis y comma x close parenthesis or A open parenthesis f open parenthesis y close parenthesis comma x close parenthesis close parenthesis close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 411, column 1

Expression 268

M, s ⊨ A (x)

Conventional reading: structure M under assignment s satisfies A open parenthesis x close parenthesis

Meaning here: The expression reads structure M under assignment s satisfies A open parenthesis x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

3 occurrences

Expression 269

s_{2} (x) = 2

Conventional reading: s sub two open parenthesis x close parenthesis equals two

Meaning here: The expression reads s sub two open parenthesis x close parenthesis equals two. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

2 occurrences

Expression 270

{Val}_{s}^{M_{1}} (t) = {Val}_{s}^{M_{2}} (t)

Conventional reading: the value of t in structure M sub one under assignment s equals the value of t in structure M sub two under assignment s

Meaning here: The expression reads the value of t in structure M sub one under assignment s equals the value of t in structure M sub two under assignment s. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 41, column 3

Expression 271

M, s [{Val}_{s}^{M} (t') / x] ⊨ A

Conventional reading: structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s satisfies A

Meaning here: The expression reads structure M under assignment s updated to send variable x to object the value of t prime in structure M under assignment s satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 108, column 1

Expression 272

+

Conventional reading: object language symbol plus

Meaning here: The expression reads object language symbol plus. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 70, column 20

Expression 273

t [t' / x] = c

Conventional reading: t with t prime substituted for variable x equals c

Meaning here: The expression reads t with t prime substituted for variable x equals c. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 73, column 52

Expression 274

s (v) = 1

Conventional reading: s open parenthesis v close parenthesis equals one

Meaning here: The expression reads s open parenthesis v close parenthesis equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 410, column 9

Expression 275

four

Conventional reading: object language symbol four

Meaning here: The expression reads object language symbol four. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 49, column 55

Expression 276

M ⊨ \exists x A (x)

Conventional reading: structure M satisfies there exists x, A open parenthesis x close parenthesis

Meaning here: The expression reads structure M satisfies there exists x, A open parenthesis x close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 277

M ⊩ A

Conventional reading: structure M makes true A

Meaning here: The expression reads structure M makes true A. Here the double turnstile defines truth of a sentence in a structure without variable assignments.

2 occurrences

Expression 278

a

Conventional reading: constant symbol a

Meaning here: The letter a names the first constant symbol in the worked first-order language.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 180, column 39

Expression 279

Γ ⊨ \neg A

Conventional reading: Gamma semantically entails not A

Meaning here: The expression reads Gamma semantically entails not A. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 85, column 56

Expression 280

t [t' / x]

Conventional reading: t with t prime substituted for variable x

Meaning here: The expression reads t with t prime substituted for variable x. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 123, column 52

Expression 281

M_{2} ⊨ A

Conventional reading: structure M sub two satisfies A

Meaning here: The expression reads structure M sub two satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 54, column 57

Expression 282

t_{1} = t_{2}

Conventional reading: term t sub one equals term t sub two

Meaning here: This is the atomic identity formula formed from the first and second terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 69, column 25

Expression 283

t [t' / x] = t'

Conventional reading: t with t prime substituted for variable x equals t prime

Meaning here: The expression reads t with t prime substituted for variable x equals t prime. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 82, column 29

Expression 284

⊥

Conventional reading: falsity constant

Meaning here: This is the logical falsity constant, which is not satisfied in any structure under any assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 67, column 18

Expression 285

{| M |}^{2} \to | M |

Conventional reading: functions from the square of the domain of M to the domain of M

Meaning here: This is the exact binary function type shared by the interpreted addition and multiplication symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 50, column 23

Expression 286

+^{M}

Conventional reading: the interpretation of object language symbol plus in structure M

Meaning here: The expression reads the interpretation of object language symbol plus in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 49, column 23

Expression 287

M, s_{1} [m / x] ⊨ B

Conventional reading: structure M under assignment s sub one updated to send variable x to object m satisfies B

Meaning here: The expression reads structure M under assignment s sub one updated to send variable x to object m satisfies B. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 161, column 37

Expression 288

{two}^{M} = 2

Conventional reading: the interpretation of object language symbol two in structure M equals two

Meaning here: The expression reads the interpretation of object language symbol two in structure M equals two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 42, column 30

Expression 289

\to

Conventional reading: conditional connective

Meaning here: This is the main implication connective of the displayed conditional formula.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 218, column 26

Expression 290

B

Conventional reading: formula B

Meaning here: B denotes the immediate subformula or sentence used in a satisfaction, induction, or entailment step.

11 occurrences

Expression 291

HF

Conventional reading: structure HF

Meaning here: The expression reads structure HF. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 85, column 22

Expression 292

0^{M}

Conventional reading: the interpretation of object language symbol zero in structure M

Meaning here: The expression reads the interpretation of object language symbol zero in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 46, column 35

Expression 293

Γ \cup {A}

Conventional reading: Gamma union the singleton containing A

Meaning here: This is the premise set Gamma extended by sentence A for the semantic deduction theorem.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 113, column 64

Expression 294

Γ ⊨ \forall x A

Conventional reading: Gamma semantically entails for every x, A

Meaning here: The expression reads Gamma semantically entails for every x, A. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 87, column 3

Expression 295

m \in | M |

Conventional reading: m is an element of the domain of structure M

Meaning here: The expression reads m is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

7 occurrences

Expression 296

s [2 / x] [n / y]

Conventional reading: the assignment obtained by updating s to send x to two and then y to n

Meaning here: The outer brackets update the already updated assignment to send y to n; they do not perform syntactic substitution.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 340, column 1

Expression 297

2

Conventional reading: number two

Meaning here: Two is a displayed domain element, assignment value, or case value in the worked model.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 349, column 62

Expression 298

\exists x A (x)

Conventional reading: there exists x, A open parenthesis x close parenthesis

Meaning here: The expression reads there exists x, A open parenthesis x close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

3 occurrences

Expression 299

R^{M}

Conventional reading: the interpretation of R in structure M

Meaning here: The expression reads the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 210, column 43

Expression 300

| N | = ℕ

Conventional reading: the domain of structure N equals the natural numbers

Meaning here: The expression reads the domain of structure N equals the natural numbers. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 55, column 7

Expression 301

L_{A}

Conventional reading: language L sub A

Meaning here: The expression reads language L sub A. The expression names a first-order language or one of its object-language symbols.

4 occurrences

Expression 302

m = 2

Conventional reading: m equals two

Meaning here: The expression reads m equals two. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

3 occurrences

Expression 303

M, s ⊨ \forall x (R (a, x) \to \exists y R (x, y)) .

Conventional reading: structure M under assignment s satisfies for every x, open parenthesis R open parenthesis a comma x close parenthesis implies there exists y, R open parenthesis x comma y close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s satisfies for every x, open parenthesis R open parenthesis a comma x close parenthesis implies there exists y, R open parenthesis x comma y close parenthesis close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 350, column 1

Expression 304

t [t' / x] = y

Conventional reading: t with t prime substituted for variable x equals y

Meaning here: The expression reads t with t prime substituted for variable x equals y. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 78, column 3

Expression 305

⟨ 2, 2 ⟩ \notin <^{M}

Conventional reading: the ordered tuple two comma two is not an element of the interpretation of less than in structure M

Meaning here: The expression reads the ordered tuple two comma two is not an element of the interpretation of less than in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 46, column 20

Expression 306

x_{1}

Conventional reading: variable x sub one

Meaning here: This is the first variable in the finite list containing all relevant variables.

6 occurrences

Expression 307

b^{M} = 2

Conventional reading: the interpretation of b in structure M equals two

Meaning here: The expression reads the interpretation of b in structure M equals two. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 186, column 7

Expression 308

<

Conventional reading: less-than predicate symbol

Meaning here: This is the binary less-than predicate of the arithmetic language.

2 occurrences

Expression 309

Γ = {⊤}

Conventional reading: Gamma equals open brace verum close brace

Meaning here: The expression reads Gamma equals open brace verum close brace. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 55, column 66

Expression 310

{Val}_{s_{1}}^{M} (t) = s_{1} (x_{i}) = s_{2} (x_{i}) = {Val}_{s_{2}}^{M} (t)

Conventional reading: the value of t in structure M under assignment s sub one equals s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis equals the value of t in structure M under assignment s sub two

Meaning here: The expression reads the value of t in structure M under assignment s sub one equals s sub one open parenthesis x sub i close parenthesis equals s sub two open parenthesis x sub i close parenthesis equals the value of t in structure M under assignment s sub two. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 40, column 8

Expression 311

\in^{HF} = {⟨ x, y ⟩ : x, y \in | HF |, x \in y}

Conventional reading: the interpretation of membership in structure HF equals the set of ordered pairs x comma y such that x and y are elements of the domain of HF and x is an element of y

Meaning here: The interpreted binary relation contains exactly the ordered pairs of hereditarily finite sets whose first component is a member of the second.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 89, column 7

Expression 312

M ⊨ A

Conventional reading: structure M satisfies A

Meaning here: The expression reads structure M satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

16 occurrences

Expression 313

M, s_{2} ⊨ A

Conventional reading: structure M under assignment s sub two satisfies A

Meaning here: The expression reads structure M under assignment s sub two satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

2 occurrences

Expression 314

R (x, y)

Conventional reading: atomic formula R of x comma y

Meaning here: This atomic formula applies binary predicate R to variables x and y.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 341, column 52

Expression 315

M ⊨ \neg A

Conventional reading: structure M satisfies not A

Meaning here: The expression reads structure M satisfies not A. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 71, column 1

Expression 316

M, s_{2} ⊭ B

Conventional reading: structure M under assignment s sub two does not satisfy B

Meaning here: The expression reads structure M under assignment s sub two does not satisfy B. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 124, column 7

Expression 317

⟨ {Val}_{s_{2}}^{M} (t_{1}), \dots, {Val}_{s_{2}}^{M} (t_{k}) ⟩ \in R^{M}

Conventional reading: the tuple of the value of t sub one through t sub k in structure M under assignment s sub two is an element of the interpretation of R in structure M

Meaning here: The expression reads the tuple of the value of t sub one through t sub k in structure M under assignment s sub two is an element of the interpretation of R in structure M. This evaluates the displayed term in the stated structure and, when present, relative to the stated variable assignment.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 91, column 5

Expression 318

t

Conventional reading: term t

Meaning here: The letter t denotes the term whose value, variables, or substitution behavior is under discussion.

18 occurrences

Expression 319

two \times (three + zero)

Conventional reading: object language symbol two times open parenthesis object language symbol three plus object language symbol zero close parenthesis

Meaning here: The expression reads object language symbol two times open parenthesis object language symbol three plus object language symbol zero close parenthesis. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 51, column 52

Expression 320

\begin{matrix} s_{1} & = s [1 / x], & s_{2} & = s [2 / x], \\ s_{3} & = s [3 / x], & s_{4} & = s [4 / x] . \end{matrix}

Conventional reading: s sub one equals assignment s updated to send variable x to object one comma s sub two equals assignment s updated to send variable x to object two comma then s sub three equals assignment s updated to send variable x to object three comma s sub four equals assignment s updated to send variable x to object four

Meaning here: The expression reads s sub one equals assignment s updated to send variable x to object one comma s sub two equals assignment s updated to send variable x to object two comma then s sub three equals assignment s updated to send variable x to object three comma s sub four equals assignment s updated to send variable x to object four. The expression concerns an updated variable assignment or a capture-avoiding syntactic substitution, as its displayed first argument determines.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 235, column 1

Expression 321

n, m \in ℕ

Conventional reading: n and m are elements of the natural numbers

Meaning here: Both n and m range over the natural numbers; the comma does not form an ordered pair or a single member.

3 occurrences

Expression 322

M, s_{2} ⊨ A

Conventional reading: structure M under assignment s sub two satisfies A

Meaning here: The expression reads structure M under assignment s sub two satisfies A. This is a first-order satisfaction claim in the displayed structure and assignment context.

4 occurrences

Expression 323

A (t)

Conventional reading: formula A with term t substituted as argument

Meaning here: This is the term instance of one-free-variable formula A.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 138, column 35

Expression 324

f^{M} (x, y) = x + y

Conventional reading: the interpretation of f in structure M open parenthesis x comma y close parenthesis equals x plus y

Meaning here: The expression reads the interpretation of f in structure M open parenthesis x comma y close parenthesis equals x plus y. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 187, column 7

Expression 325

\forall x B (x)

Conventional reading: for every x, B open parenthesis x close parenthesis

Meaning here: The expression reads for every x, B open parenthesis x close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 155, column 31

Expression 326

⟨ 2, 1 ⟩ \notin R^{M}

Conventional reading: the ordered tuple two comma one is not an element of the interpretation of R in structure M

Meaning here: The expression reads the ordered tuple two comma one is not an element of the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 342, column 23

Expression 327

\forall x \exists y A (x, y)

Conventional reading: for every x, there exists y, A open parenthesis x comma y close parenthesis

Meaning here: The expression reads for every x, there exists y, A open parenthesis x comma y close parenthesis. This is a quantified first-order formula with the displayed variable bound in its scope.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 350, column 1

Expression 328

L = {c, f, A}

Conventional reading: language L equals open brace c comma f comma A close brace

Meaning here: The expression reads language L equals open brace c comma f comma A close brace. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 401, column 5

Expression 329

5

Conventional reading: number five

Meaning here: Five is the value obtained in the arithmetic interpretation example.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/covered-structures.tex, line 48, column 39

Expression 330

= 3

Conventional reading: equals three in the otherwise case

Meaning here: This source fragment continues the left hand side giving the interpreted value of f at x and y; the occurrence reader repeats that subject.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 187, column 54

Expression 331

L

Conventional reading: language L

Meaning here: The expression reads language L. The expression names a first-order language or one of its object-language symbols.

7 occurrences

Expression 332

<

Conventional reading: object language symbol less than

Meaning here: The expression reads object language symbol less than. The expression names a first-order language or one of its object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/structures.tex, line 70, column 45

Expression 333

M, s ⊨ \exists x (R (b, x) \lor R (x, b)),

Conventional reading: structure M under assignment s satisfies there exists x, open parenthesis R open parenthesis b comma x close parenthesis or R open parenthesis x comma b close parenthesis close parenthesis comma

Meaning here: The expression reads structure M under assignment s satisfies there exists x, open parenthesis R open parenthesis b comma x close parenthesis or R open parenthesis x comma b close parenthesis close parenthesis comma. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 250, column 3

Expression 334

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

Conventional reading: term t is syntactically identical to function term f of t sub one through t sub n

Meaning here: This is the compound-function case in the induction on terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 86, column 10

Expression 335

A (t) ⊨ \exists x A (x)

Conventional reading: A open parenthesis t close parenthesis semantically entails there exists x, A open parenthesis x close parenthesis

Meaning here: The expression reads A open parenthesis t close parenthesis semantically entails there exists x, A open parenthesis x close parenthesis. This is a semantic-consequence claim: every interpretation satisfying the premises also satisfies the conclusion.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/semantic-notions.tex, line 128, column 21

Expression 336

\begin{matrix} {Val}_{s}^{M} (t [t' / x]) = \\ \begin{matrix} = {Val}_{s}^{M} (f (t_{1} [t' / x], \dots, t_{n} [t' / x])) \\ by definition of t [t' / x] \\ = f^{M} ({Val}_{s}^{M} (t_{1} [t' / x]), \dots, {Val}_{s}^{M} (t_{n} [t' / x])) \\ by definition of {Val}_{s}^{M} (f (\dots)) \\ = f^{M} ({Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (t_{1}), \dots, {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (t_{n})) \\ by induction hypothesis \\ = {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (t) by definition of {Val}_{s [{Val}_{s}^{M} (t') / x]}^{M} (f (\dots)) \end{matrix} \end{matrix}

Conventional reading: the value after substituting term t prime for x in compound term t is expanded into the values of the substituted argument terms; the induction hypothesis moves each substitution into the assignment by updating s at x with the value of t prime; the resulting function value is the value of t under that updated assignment

Meaning here: This display proves the compound-function case of the substitution lemma for term values.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/extensionality.tex, line 87, column 1

Expression 337

A (a)

Conventional reading: formula A with constant a as argument

Meaning here: This is the constant instance used in the existential-generalization discussion.

2 occurrences

Expression 338

M, s [m / x] ⊭ \forall y R (x, y)

Conventional reading: structure M under assignment s updated to send variable x to object m does not satisfy for every y, R open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M under assignment s updated to send variable x to object m does not satisfy for every y, R open parenthesis x comma y close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 361, column 1

Expression 339

M, s ⊭ \exists x (R (a, x) \land \forall y R (x, y)) .

Conventional reading: structure M under assignment s does not satisfy there exists x, open parenthesis R open parenthesis a comma x close parenthesis and for every y, R open parenthesis x comma y close parenthesis close parenthesis

Meaning here: The expression reads structure M under assignment s does not satisfy there exists x, open parenthesis R open parenthesis a comma x close parenthesis and for every y, R open parenthesis x comma y close parenthesis close parenthesis. This is a negative satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 354, column 1

Expression 340

⟨ {d_{1}}^{M}, \dots, {d_{n}}^{M} ⟩ \in R^{M}

Conventional reading: open angle bracket the interpretation of d sub one in structure M comma and so on comma the interpretation of d sub n in structure M close angle bracket is an element of the interpretation of R in structure M

Meaning here: The expression reads open angle bracket the interpretation of d sub one in structure M comma and so on comma the interpretation of d sub n in structure M close angle bracket is an element of the interpretation of R in structure M. The superscripted notation denotes the interpretation assigned to an object-language symbol by the structure.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 293, column 7

Expression 341

B (x)

Conventional reading: formula B with free variable x

Meaning here: This is the quantified formula's scope with x displayed free before assignment update.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 174, column 56

Expression 342

| M | = {1, 2, 3}

Conventional reading: the domain of structure M equals open brace one comma two comma three close brace

Meaning here: The expression reads the domain of structure M equals open brace one comma two comma three close brace. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 405, column 7

Expression 343

n = 1

Conventional reading: n equals one

Meaning here: The expression reads n equals one. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

2 occurrences

Expression 344

M ⊨ \forall x \exists y A (x, y)

Conventional reading: structure M satisfies for every x, there exists y, A open parenthesis x comma y close parenthesis

Meaning here: The expression reads structure M satisfies for every x, there exists y, A open parenthesis x comma y close parenthesis. This is a first-order satisfaction claim in the displayed structure and assignment context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 345, column 1

Expression 345

s_{1}'

Conventional reading: variable assignment s sub one prime

Meaning here: This is the x variant of s sub one used in the satisfaction-independence induction.

3 occurrences

Expression 346

t = x_{i}

Conventional reading: t equals x sub i

Meaning here: The expression reads t equals x sub i. The equality identifies the two displayed values, assignments, interpretations, or expressions in the surrounding semantic argument.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/assignments.tex, line 39, column 1

Expression 347

m \in | M |

Conventional reading: m is an element of the domain of structure M

Meaning here: The expression reads m is an element of the domain of structure M. The fraktur letter names a first-order structure, and its domain is the nonempty collection over which its variables range.

8 occurrences

Expression 348

(A \land B)

Conventional reading: open scope formula A and formula B close scope

Meaning here: This conjunction illustrates how satisfaction is defined recursively from the satisfaction of its two immediate subformulas.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/intro-semantics.tex, line 29, column 53

Reading preferences

Equation and object guide

348 expression records

Expression 1

Expression 2

Expression 3

Expression 4

Expression 5

Expression 6

Expression 7

Expression 8

Expression 9

Expression 10

Expression 11

Expression 12

Expression 13

Expression 14

Expression 15

Expression 16

Expression 17

Expression 18

Expression 19

Expression 20

Expression 21

Expression 22

Expression 23

Expression 24

Expression 25

Expression 26

Expression 27

Expression 28

Expression 29

Expression 30

Expression 31

Expression 32

Expression 33

Expression 34

Expression 35

Expression 36

Expression 37

Expression 38

Expression 39

Expression 40

Expression 41

Expression 42

Expression 43

Expression 44

Expression 45

Expression 46

Expression 47

Expression 48

Expression 49

Expression 50

Expression 51

Expression 52

Expression 53

Expression 54

Expression 55

Expression 56

Expression 57

Expression 58

Expression 59

Expression 60

Expression 61

Expression 62

Expression 63

Expression 64

Expression 65

Expression 66

Expression 67

Expression 68

Expression 69

Expression 70

Expression 71

Expression 72

Expression 73

Expression 74

Expression 75

Expression 76

Expression 77