Second-order logic

Syntax and Semantics

Equation form expr-01a02ff4402bc478

s[M/X](z)∈M\Subst{s}{M}{X}(z) \in M

Read as: the value of lower case z under s modified to assign the relation M to capital X belongs to M

Means: the value of lower case z under s modified to assign the relation M to capital X belongs to M

1 occurrence in this chapter

Equation form expr-022f089b8754c90a

uin\Obj u_i^n

Read as: the function variable u with index i and arity n

Means: the function variable u with index i and arity n

1 occurrence in this chapter

Equation form expr-02d2a72f2c936ead

ran(f)≠M\ran{f} \neq M

Read as: the range of f is not the entire set M

Means: the range of f is not the entire set M

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: s

15 occurrences in this chapter

Equation form expr-04ff73f0195023b4

s(X)=R*s(X) = R^*

Read as: s of capital X equals R star

Means: s of capital X equals R star

1 occurrence in this chapter

Equation form expr-055d5ee422435b80

R*R^*

Read as: R star

Means: R star

2 occurrences in this chapter

Equation form expr-06b343a286afe3b7

s(Vin)⊆|M|ns(\Obj{V_i^n}) \subseteq \Domain{M}^n

Read as: the value assigned by s to the relation variable capital V with index i and arity n is a subset of the set of n tuples from the domain of structure M

Means: the value assigned by s to the relation variable capital V with index i and arity n is a subset of the set of n tuples from the domain of structure M

1 occurrence in this chapter

Equation form expr-078f4908c90bb026

R(a,c1)R(a,c_1)

Read as: R relates a to c subscript one

Means: R relates a to c subscript one

1 occurrence in this chapter

Equation form expr-08f271887ce94707

MM

Read as: capital M

Means: capital M

7 occurrences in this chapter

Equation form expr-0953c73d5f914111

∀X(X(x)→X(y))\lforall[X][(X(x) \lif X(y))]

Read as: for every unary relation capital X, if capital X holds of lower case x then capital X holds of lower case y

Means: for every unary relation capital X, if capital X holds of lower case x then capital X holds of lower case y

1 occurrence in this chapter

Equation form expr-09929e9000f85104

|M|\Domain M

Read as: the domain of structure M

Means: the domain of structure M

1 occurrence in this chapter

Equation form expr-0ab83730c263f0b7

⊨A\Entails !A

Read as: A is logically valid

Means: A is logically valid

1 occurrence in this chapter

Equation form expr-0bfe935e70c321c7

uu

Read as: u

Means: u

6 occurrences in this chapter

Equation form expr-0ce267ec3077d9f0

V1n\Obj V_1^n

Read as: the relation variable capital V with index one and arity n

Means: the relation variable capital V with index one and arity n

1 occurrence in this chapter

Equation form expr-0dd678d817d436c0

y∈|M|y \in \Domain{M}

Read as: lower case y in the domain of structure M

Means: lower case y in the domain of structure M

1 occurrence in this chapter

Equation form expr-10d4d1a76249eef1

s(x)=as(x) = a

Read as: s assigns a to lower case x

Means: s assigns a to lower case x

1 occurrence in this chapter

Equation form expr-127d3b98c666fc2e

x∈Mx \in M

Read as: lower case x belongs to M

Means: lower case x belongs to M

3 occurrences in this chapter

Equation form expr-13df79da978c63c8

M={m,f(m),f(f(m)),…}M = \{m, f(m), f(f(m)), \dots\}

Read as: M is the set consisting of m, f of m, f of f of m, and all further finite iterates

Means: M is the set consisting of m, f of m, f of f of m, and all further finite iterates

1 occurrence in this chapter

Equation form expr-142725828815e92f

f:M→Mf\colon M \to M

Read as: f from M to M

Means: f from M to M

2 occurrences in this chapter

Equation form expr-153ffebc8cbe7d63

s(X)={1,2,3}=|M|s(X) = \{1, 2, 3\} = \Domain{M}

Read as: s of capital X equals the set one, two, three, which is the entire domain of structure M

Means: s of capital X equals the set one, two, three, which is the entire domain of structure M

1 occurrence in this chapter

Equation form expr-159fe7a0a658fce3

∃V01∀v0(V01(v0)∨¬V01(v0))\lexists[\Obj{V^1_0}][\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj{v_0}) \lor \lnot \Obj{V^1_0}(\Obj{v_0}))]]

Read as: there exists a unary relation variable capital V subscript zero such that for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

Means: there exists a unary relation variable capital V subscript zero such that for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

1 occurrence in this chapter

Equation form expr-170d993bcd0dc9c4

M,s[M/X]⊨∀x(X(x)→X(u(x)))\Sat{M}{\lforall[x][(X(x) \lif X(u(x)))]}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: for every object lower case x, if capital X holds of x then capital X holds of u of x

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: for every object lower case x, if capital X holds of x then capital X holds of u of x

1 occurrence in this chapter

Equation form expr-176c9ef2d11bfa7d

s(X)=∅s(X) = \emptyset

Read as: s assigns the empty relation to capital X

Means: s assigns the empty relation to capital X

1 occurrence in this chapter

Equation form expr-17a2d7fbe5d823e6

M⊨Count\Sat{M}{\fn{Count}}

Read as: structure M satisfies the following: Count

Means: structure M satisfies the following: Count

3 occurrences in this chapter

Equation form expr-18f5384d58bcb1bb

YY

Read as: capital Y

Means: capital Y

4 occurrences in this chapter

Equation form expr-199649af431f6dc9

N⊆|M|N \subseteq \Domain{M}

Read as: N contained in the domain of structure M

Means: N contained in the domain of structure M

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

11 occurrences in this chapter

Equation form expr-1d633050c0896880

2∈s2[2/z](X)2 \in \Subst{s_2}{2}{z}(X)

Read as: two belongs to the value of capital X under s subscript two modified to assign two to lower case z

Means: two belongs to the value of capital X under s subscript two modified to assign two to lower case z

1 occurrence in this chapter

Equation form expr-2160509ff364e743

M\Struct M

Read as: the structure M

Means: the structure M

8 occurrences in this chapter

Equation form expr-21aef9213924a898

s(X)={1,2}s(X) = \{1, 2\}

Read as: s assigns the set one, two to capital X

Means: s assigns the set one, two to capital X

1 occurrence in this chapter

Equation form expr-21b3256df2f9f181

∀x∀y(f(x)=f(y)→x=y)∧∃y∀xy≠f(x).\lforall[x][\lforall[y][(\eq[f(x)][f(y)] \to \eq[x][y])]] \land \lexists[y][\lforall[x][\eq/[y][f(x)]]].

Read as: for all objects lower case x and lower case y, if f of x equals f of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from f of x

Means: for all objects lower case x and lower case y, if f of x equals f of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from f of x

1 occurrence in this chapter

Equation form expr-223c4d2008755108

a=ba = b

Read as: a equals b

Means: a equals b

1 occurrence in this chapter

Equation form expr-2243e3b7b9aad203

∃uA\lexists[u][!A]

Read as: the expression, quote, there exists a function u such that A, end quote

Means: the expression, quote, there exists a function u such that A, end quote

1 occurrence in this chapter

Equation form expr-24bc1e59a325f7d4

Id|M|\Id{\Domain{M}}

Read as: the identity relation on the domain of structure M

Means: the identity relation on the domain of structure M

3 occurrences in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

5 occurrences in this chapter

Equation form expr-254051ed849e0a84

ckc_k

Read as: c subscript k

Means: c subscript k

1 occurrence in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: negation

Means: negation

1 occurrence in this chapter

Equation form expr-2a0391fcf00437fa

s(X)=|M|s(X) = \Domain{M}

Read as: s of capital X equals the entire domain of structure M

Means: s of capital X equals the entire domain of structure M

2 occurrences in this chapter

Equation form expr-2a0f7d095343e035

N≠∅N \neq \emptyset

Read as: nonempty N

Means: nonempty N

1 occurrence in this chapter

Equation form expr-2a7cb0e79915cabe

m0,m1,m2,…m_0, m_1, m_2, \dots

Read as: m subscript zero, m subscript one, m subscript two, and so on

Means: m subscript zero, m subscript one, m subscript two, and so on

1 occurrence in this chapter

Equation form expr-2a82573bef434983

∃XA\lexists[X][!A]

Read as: the expression, quote, there exists a relation capital X such that A, end quote

Means: the expression, quote, there exists a relation capital X such that A, end quote

1 occurrence in this chapter

Equation form expr-2a86a1412e8efc6e

A→∀X∀yX(y)!A \lif \lforall[X][\lforall[y][X(y)]]

Read as: if A, then for every unary relation capital X and every object lower case y, capital X holds of y

Means: if A, then for every unary relation capital X and every object lower case y, capital X holds of y

1 occurrence in this chapter

Equation form expr-2ceb4df5993cba2b

c1c_1

Read as: c subscript one

Means: c subscript one

1 occurrence in this chapter

Equation form expr-2d2b51f442bf96d9

M,s⊨A\Sat{M}{!A}[s]

Read as: the statement that structure M under assignment s satisfies A

Means: the statement that structure M under assignment s satisfies A

3 occurrences in this chapter

Equation form expr-2d47c518b9cd45da

x=y\eq[x][y]

Read as: lower case x equals lower case y

Means: lower case x equals lower case y

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: lower case x

Means: lower case x

6 occurrences in this chapter

Equation form expr-2d7214c5774812ff

s(z)=m0s(z) = m_0

Read as: s assigns m subscript zero to lower case z

Means: s assigns m subscript zero to lower case z

1 occurrence in this chapter

Equation form expr-2e34c44555fc963b

s(u)=fs(u) = f

Read as: s assigns the function f to u

Means: s assigns the function f to u

2 occurrences in this chapter

Equation form expr-2fd3757235cab8cb

N=|M|∖s(X)N = \Domain{M} \setminus s(X)

Read as: N equals the domain of structure M with the members of s of capital X removed

Means: N equals the domain of structure M with the members of s of capital X removed

1 occurrence in this chapter

Equation form expr-302bf971932aa0ea

BR(X)≡∀x∀y(R(x,y)→X(x,y))∧∀x∀y∀z((X(x,y)∧X(y,z))→X(x,z)).!B_R(X) \ident \lforall[x][\lforall[y][(R(x,y) \lif X(x, y))]] \land {}\\ \lforall[x][\lforall[y][\lforall[z][((X(x,y) \land X(y,z)) \lif X(x, z))]]].

Read as: B subscript R of capital X abbreviates the conjunction of two conditions. First, for all objects lower case x and lower case y, if R relates x to y then capital X relates x to y. Second, for all objects lower case x, lower case y, and lower case z, if capital X relates x to y and capital X relates y to z, then capital X relates x to z

Means: B subscript R of capital X abbreviates the conjunction of two conditions. First, for all objects lower case x and lower case y, if R relates x to y then capital X relates x to y. Second, for all objects lower case x, lower case y, and lower case z, if capital X relates x to y and capital X relates y to z, then capital X relates x to z

1 occurrence in this chapter

Equation form expr-316fcce072aa19f6

M,s⊨∀X((X(z)∧∀x(X(x)→X(u(x))))→∀xX(x))\Sat{M}{\lforall[X][((X(z) \land \lforall[x][(X(x) \lif X(u(x)))]) \lif \lforall[x][X(x)])]}[s]

Read as: structure M under assignment s satisfies the following: for every unary relation capital X: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

Means: structure M under assignment s satisfies the following: for every unary relation capital X: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

2 occurrences in this chapter

Equation form expr-32e8c27e056d2ad2

R(ck,b)R(c_k,b)

Read as: R relates c subscript k to b

Means: R relates c subscript k to b

1 occurrence in this chapter

Equation form expr-335b5e6f91a8441f

m0m_0

Read as: m subscript zero

Means: m subscript zero

1 occurrence in this chapter

Equation form expr-33a9c96304bcc292

|M|\Domain{M}

Read as: the domain of structure M

Means: the domain of structure M

21 occurrences in this chapter

Equation form expr-37215724c929cadf

∀X∀yX(y)\lforall[X][\lforall[y][X(y)]]

Read as: for every unary relation capital X and every object lower case y, capital X holds of y

Means: for every unary relation capital X and every object lower case y, capital X holds of y

1 occurrence in this chapter

Equation form expr-3e23e8160039594a

bb

Read as: b

Means: b

4 occurrences in this chapter

Equation form expr-401683b397b9764b

M,s[M/X]⊨X(z)\Sat{M}{X(z)}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: capital X holds of lower case z

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: capital X holds of lower case z

1 occurrence in this chapter

Equation form expr-41e12352e4691c3b

uin\Obj{u_i^n}

Read as: the function variable u with index i and arity n

Means: the function variable u with index i and arity n

1 occurrence in this chapter

Equation form expr-428459f7dd087b9a

f(z)f(z)

Read as: f of lower case z

Means: f of lower case z

2 occurrences in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: the structure M

Means: the structure M

11 occurrences in this chapter

Equation form expr-45e200a89a29ed8f

R*(X)≡BR(X)∧∀Y(BR(Y)→∀x∀y(X(x,y)→Y(x,y))).R^*(X) \ident !B_R(X) \land \lforall[Y][(!B_R(Y) \lif \lforall[x][\lforall[y][(X(x, y) \lif Y(x,y))]])].

Read as: R star of capital X abbreviates: B subscript R of capital X, and for every binary relation capital Y, if B subscript R of capital Y then for all objects lower case x and lower case y, if capital X relates x to y then capital Y relates x to y

Means: R star of capital X abbreviates: B subscript R of capital X, and for every binary relation capital Y, if B subscript R of capital Y then for all objects lower case x and lower case y, if capital X relates x to y then capital Y relates x to y

1 occurrence in this chapter

Equation form expr-46adfe66b9be53aa

M,s[M/X]⊨∀xX(x)\Sat{M}{\lforall[x][X(x)]}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: for every object lower case x, capital X holds of x

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: for every object lower case x, capital X holds of x

2 occurrences in this chapter

Equation form expr-484bca22f27a32a8

⟨ValsM(t1),…,ValsM(tn)⟩∈s(Xn)\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in s(X^n)

Read as: the ordered n tuple of the values of t subscript one through t subscript n in structure M under assignment s belongs to the n place relation assigned to capital X superscript n by s

Means: the ordered n tuple of the values of t subscript one through t subscript n in structure M under assignment s belongs to the n place relation assigned to capital X superscript n by s

1 occurrence in this chapter

Equation form expr-4a145705f6d198a8

|M|∖s(X)\Domain{M} \setminus s(X)

Read as: the domain of structure M with the members of s of capital X removed

Means: the domain of structure M with the members of s of capital X removed

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: capital X

Means: capital X

12 occurrences in this chapter

Equation form expr-4c94485e0c21ae6c

vv

Read as: v

Means: v

1 occurrence in this chapter

Equation form expr-4cb0bda4bc901613

R(a,b)R(a, b)

Read as: R relates a to b

Means: R relates a to b

1 occurrence in this chapter

Equation form expr-4daae228e5fbd9bd

z=m0z = m_0

Read as: lower case z equals m subscript zero

Means: lower case z equals m subscript zero

1 occurrence in this chapter

Equation form expr-5116f52e35d3ac37

s(X)≠|M|s(X) \neq \Domain{M}

Read as: s of capital X is not the entire domain of structure M

Means: s of capital X is not the entire domain of structure M

1 occurrence in this chapter

Equation form expr-54f0b300c9515311

m1m_1

Read as: m subscript one

Means: m subscript one

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

3 occurrences in this chapter

Equation form expr-587f0149651dc20d

M,s⊨∀z(X(z)↔¬Y(z))\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s]

Read as: structure M under assignment s satisfies the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

Means: structure M under assignment s satisfies the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-594e519ae499312b

zz

Read as: lower case z

Means: lower case z

5 occurrences in this chapter

Equation form expr-5967618e124d3970

b∉{a}b \notin \{a\}

Read as: b does not belong to the singleton set a

Means: b does not belong to the singleton set a

1 occurrence in this chapter

Equation form expr-59a9b7a26234be44

u1n\Obj u_1^n

Read as: the function variable u with index one and arity n

Means: the function variable u with index one and arity n

1 occurrence in this chapter

Equation form expr-5a60f3596955aa14

{⟨a,a⟩:a∈|M|}\Setabs{\tuple{a,a}}{a \in \Domain{M}}

Read as: the set of ordered pairs a, a, for a belonging to the domain of structure M

Means: the set of ordered pairs a, a, for a belonging to the domain of structure M

1 occurrence in this chapter

Equation form expr-5a787461a7b6ae66

u2n\Obj u_2^n

Read as: the function variable u with index two and arity n

Means: the function variable u with index two and arity n

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

2 occurrences in this chapter

Equation form expr-5e769b89788d547a

s′s'

Read as: s prime

Means: s prime

2 occurrences in this chapter

Equation form expr-60d56f28e122ddd5

Count\fn{Count}

Read as: Count

Means: Count

1 occurrence in this chapter

Equation form expr-67c26ce60dd4e0e3

vi\Obj v_i

Read as: the object variable v subscript i

Means: the object variable v subscript i

1 occurrence in this chapter

Equation form expr-6b31fda238a75ac5

s1(X)={1,2}s_1(X) = \{1, 2\}

Read as: s subscript one assigns the set one, two to capital X

Means: s subscript one assigns the set one, two to capital X

1 occurrence in this chapter

Equation form expr-6b6f3586b256ed30

ValsM(t)\Value{t}{M}[s]

Read as: the value of term t in structure M under assignment s

Means: the value of term t in structure M under assignment s

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: one

3 occurrences in this chapter

Equation form expr-6c615579d76b85c6

AR(x,y)!A_R(x, y)

Read as: A subscript R of lower case x and lower case y

Means: A subscript R of lower case x and lower case y

1 occurrence in this chapter

Equation form expr-6d96ffa2cbee7291

s′∼xs\varAssign{s'}{s}{x}

Read as: s prime is a lower case x variant of s

Means: s prime is a lower case x variant of s

1 occurrence in this chapter

Equation form expr-6e7032ee25458893

Fin≡¬Inf\fn{Fin} \ident \lnot \fn{Inf}

Read as: Fin abbreviates not Inf

Means: Fin abbreviates not Inf

1 occurrence in this chapter

Equation form expr-6ebe59bada62146c

ran(f)≠|M|\ran{f} \neq \Domain{M}

Read as: the range of f is not the entire domain of structure M

Means: the range of f is not the entire domain of structure M

2 occurrences in this chapter

Equation form expr-6f118eb66f56af74

f(x)∈Mf(x) \in M

Read as: f of lower case x belongs to M

Means: f of lower case x belongs to M

2 occurrences in this chapter

Equation form expr-741595b2e35370d6

R⊆XR \subseteq X

Read as: R is included in capital X

Means: R is included in capital X

1 occurrence in this chapter

Equation form expr-74f4567a6896230a

=\eq

Read as: the equality symbol

Means: the equality symbol

4 occurrences in this chapter

Equation form expr-759ef1429512ef8e

M,s⊨∃Y(∃yY(y)∧∀z(X(z)↔¬Y(z)))\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]

Read as: structure M under assignment s satisfies the following: there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

Means: structure M under assignment s satisfies the following: there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

2 occurrences in this chapter

Equation form expr-7b07cc095dee3123

M⊨Fin\Sat{M}{\fn{Fin}}

Read as: structure M satisfies the following: Fin

Means: structure M satisfies the following: Fin

1 occurrence in this chapter

Equation form expr-7b3a20cfa0386f58

s[f/y]={fif y≡us(y)otherwise.\Subst{s}{f}{y} = \begin{cases} f & \text{if } y \ident u\\ s(y) & \text{otherwise}. \end{cases}

Read as: the source writes assignment s modified to assign f to lower case y, equals the following cases: f if lower case y is the very same variable as u; and s of lower case y otherwise

Means: the source writes assignment s modified to assign f to lower case y, equals the following cases: f if lower case y is the very same variable as u; and s of lower case y otherwise

1 occurrence in this chapter

Equation form expr-7ba2329a6f451ded

s[m/y]={mif y≡xs(y)otherwise,\Subst{s}{m}{y} = \begin{cases} m & \text{if } y \ident x\\ s(y) & \text{otherwise}, \end{cases}

Read as: the source writes assignment s modified to assign m to lower case y, equals the following cases: m if lower case y is the very same variable as lower case x; and s of lower case y otherwise

Means: the source writes assignment s modified to assign m to lower case y, equals the following cases: m if lower case y is the very same variable as lower case x; and s of lower case y otherwise

1 occurrence in this chapter

Equation form expr-7ceec4d9e7c595b6

Trm2(L)\TrmSOL[L]

Read as: the set of second order terms of language L

Means: the set of second order terms of language L

1 occurrence in this chapter

Equation form expr-7e9c62e858c77db9

R(a,b)R(a,b)

Read as: R relates a to b

Means: R relates a to b

1 occurrence in this chapter

Equation form expr-7ea2dbbec70d4200

2∈s2[2/z](Y)2 \in \Subst{s_2}{2}{z}(Y)

Read as: two belongs to the value of capital Y under s subscript two modified to assign two to lower case z

Means: two belongs to the value of capital Y under s subscript two modified to assign two to lower case z

1 occurrence in this chapter

Equation form expr-7f8e1ef8d24f26a0

m=s(z)m = s(z)

Read as: m equals s of lower case z

Means: m equals s of lower case z

1 occurrence in this chapter

Equation form expr-814ccba120f87c1c

f(f(z))f(f(z))

Read as: f of f of lower case z

Means: f of f of lower case z

2 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

9 occurrences in this chapter

Equation form expr-838849c1bcc6fcb6

Frm2(L)\FrmSOL[L]

Read as: the set of second order formulas of language L

Means: the set of second order formulas of language L

1 occurrence in this chapter

Equation form expr-84bb4fdbf81ba8f9

a∈{a}a \in \{a\}

Read as: a belongs to the singleton set a

Means: a belongs to the singleton set a

1 occurrence in this chapter

Equation form expr-84cda14b18319013

m2=f(f(m0))∈Mm_2 = f(f(m_0)) \in M

Read as: m subscript two equals f of f of m subscript zero, and belongs to M

Means: m subscript two equals f of f of m subscript zero, and belongs to M

1 occurrence in this chapter

Equation form expr-89c797143648720a

(s[M/X](u))(x)∈M(\Subst{s}{M}{X}(u))(x) \in M

Read as: the function assigned to u by s modified to assign M to capital X, evaluated at lower case x, has its value in M

Means: the function assigned to u by s modified to assign M to capital X, evaluated at lower case x, has its value in M

1 occurrence in this chapter

Equation form expr-8ac4e321ed9bbf1b

M∋m=s[M/X](z)M \ni m = \Subst{s}{M}{X}(z)

Read as: M contains m, which equals the value of lower case z under s modified to assign M to capital X

Means: M contains m, which equals the value of lower case z under s modified to assign M to capital X

1 occurrence in this chapter

Equation form expr-8afca4ea845b52d4

f:|M|→|M|f\colon \Domain{M} \to \Domain{M}

Read as: function f from the domain of structure M to itself

Means: function f from the domain of structure M to itself

1 occurrence in this chapter

Equation form expr-8b13b8764c5cca04

M=∅M = \emptyset

Read as: the set M is empty

Means: the set M is empty

1 occurrence in this chapter

Equation form expr-8b19ee8f92e456bf

R⊆|M|2R \subseteq \Domain{M}^2

Read as: R on the Cartesian square of the domain of structure M

Means: R on the Cartesian square of the domain of structure M

1 occurrence in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

10 occurrences in this chapter

Equation form expr-8cb43f7fa2f788da

∀XA\lforall[X][!A]

Read as: the expression, quote, for every relation capital X, A, end quote

Means: the expression, quote, for every relation capital X, A, end quote

1 occurrence in this chapter

Equation form expr-8cf761cb3a925e79

V2n\Obj V_2^n

Read as: the relation variable capital V with index two and arity n

Means: the relation variable capital V with index two and arity n

1 occurrence in this chapter

Equation form expr-8e6faa0d85c79ab4

z∈Mz \in M

Read as: lower case z in M

Means: lower case z in M

1 occurrence in this chapter

Equation form expr-90eaac1ca119a254

M=|M|M = \Domain{M}

Read as: the set M equals the whole domain of structure M

Means: the set M equals the whole domain of structure M

2 occurrences in this chapter

Equation form expr-916433cfa1250348

s(Y)=|M|∖s(X)s(Y) = \Domain{M} \setminus s(X)

Read as: s of capital Y equals the domain of structure M with the members of s of capital X removed

Means: s of capital Y equals the domain of structure M with the members of s of capital X removed

1 occurrence in this chapter

Equation form expr-91eb48531e661c7f

M⊆|M|M \subseteq \Domain{M}

Read as: a subset M of the domain of structure M

Means: a subset M of the domain of structure M

3 occurrences in this chapter

Equation form expr-930f5c4baa5c7864

∀\lforall

Read as: the universal quantifier

Means: the universal quantifier

4 occurrences in this chapter

Equation form expr-934afa459ba95844

V0n\Obj V_0^n

Read as: the relation variable capital V with index zero and arity n

Means: the relation variable capital V with index zero and arity n

1 occurrence in this chapter

Equation form expr-93694b6126480f7f

u(t1,…,tn)\Atom{u}{t_1, \ldots, t_n}

Read as: u applied to the terms t subscript one through t subscript n

Means: u applied to the terms t subscript one through t subscript n

1 occurrence in this chapter

Equation form expr-93d6d7d57d9ce594

∀X(X(x)↔X(y))\lforall[X][(X(x) \liff X(y))]

Read as: for every unary relation capital X, capital X holds of lower case x if and only if capital X holds of lower case y

Means: for every unary relation capital X, capital X holds of lower case x if and only if capital X holds of lower case y

1 occurrence in this chapter

Equation form expr-98370bf0ff093461

∀z(P(z)↔¬R(z))\lforall[z][(\Atom{P}{z} \liff \lnot \Atom{R}{z})]

Read as: for every object lower case z, P holds of z if and only if R does not hold of z

Means: for every object lower case z, P holds of z if and only if R does not hold of z

1 occurrence in this chapter

Equation form expr-9ac9f96a8283a0a1

s[m/x]\Subst{s}{m}{x}

Read as: assignment s modified to assign m to lower case x

Means: assignment s modified to assign m to lower case x

1 occurrence in this chapter

Equation form expr-9af6e0d05697f98c

M,s[M/X]⊨(X(z)∧∀x(X(x)→X(u(x))))→∀xX(x)\Sat{M}{(X(z) \land \lforall[x][(X(x) \lif X(u(x)))]) \lif \lforall[x][X(x)]}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

1 occurrence in this chapter

Equation form expr-9b182ac19a89d8fd

f=s(u)f = s(u)

Read as: f is the function assigned to u by s

Means: f is the function assigned to u by s

1 occurrence in this chapter

Equation form expr-9b4d38e0f0462525

Count≡∃z∃u∀X((X(z)∧∀x(X(x)→X(u(x))))→∀xX(x))\fn{Count} \ident \lexists[z][\lexists[u][\lforall[X][((X(z) \land \lforall[x][(X(x) \lif X(u(x)))]) \lif \lforall[x][X(x)])]]]

Read as: Count abbreviates: there exists an object lower case z and there exists a unary function u such that for every unary relation capital X: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

Means: Count abbreviates: there exists an object lower case z and there exists a unary function u such that for every unary relation capital X: if both of the following hold: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x; then for every object lower case x, capital X holds of x

1 occurrence in this chapter

Equation form expr-9be3cd322046c085

s2(Y)={2,3}s_2(Y) = \{2, 3\}

Read as: s subscript two assigns the set two, three to capital Y

Means: s subscript two assigns the set two, three to capital Y

1 occurrence in this chapter

Equation form expr-9d18af8a23c6e0c3

∀v0(V01(v0)∨¬V01(v0))\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj v_0) \lor \lnot \Obj{V^1_0}(v_0))]

Read as: for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

Means: for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

1 occurrence in this chapter

Equation form expr-9db47e058df5b03b

M,s2⊭∀z(X(z)↔¬Y(z))\Sat/{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s_2]

Read as: structure M under assignment s subscript two does not satisfy the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

Means: structure M under assignment s subscript two does not satisfy the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-9e2bf28607ec4827

P01\Obj{P^1_0}

Read as: the unary predicate symbol P subscript zero

Means: the unary predicate symbol P subscript zero

1 occurrence in this chapter

Equation form expr-9fd6a32e8c129e12

uin\Obj{u^n_i}

Read as: the function variable u with index i and arity n

Means: the function variable u with index i and arity n

1 occurrence in this chapter

Equation form expr-a0dff204c822b3ab

vi\Obj{v_i}

Read as: the object variable v subscript i

Means: the object variable v subscript i

1 occurrence in this chapter

Equation form expr-a10ac4d04e7a664d

f(mk)=mkf(m_k) = m_k

Read as: f of m subscript k equals m subscript k

Means: f of m subscript k equals m subscript k

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: lower case y

Means: lower case y

3 occurrences in this chapter

Equation form expr-a6e24f1633edda7f

M,s[N/Y]⊨(∃yY(y)∧∀z(X(z)↔¬Y(z)))\Sat{M}{(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]

Read as: structure M under assignment s modified to assign N to capital Y satisfies the following: there exists an object lower case y such that capital Y holds of y, and for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

Means: structure M under assignment s modified to assign N to capital Y satisfies the following: there exists an object lower case y such that capital Y holds of y, and for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-a761a91d8cbd6d54

f(mk)=mk+1f(m_k) = m_{k+1}

Read as: f of m subscript k equals m subscript k plus one

Means: f of m subscript k equals m subscript k plus one

2 occurrences in this chapter

Equation form expr-a7fbc7f3ca96a267

m1=f(m0)∈Mm_1 = f(m_0) \in M

Read as: m subscript one equals f of m subscript zero, and belongs to M

Means: m subscript one equals f of m subscript zero, and belongs to M

1 occurrence in this chapter

Equation form expr-a80d5c76d60fc959

s2(X)={1,2}s_2(X) = \{1, 2\}

Read as: s subscript two assigns the set one, two to capital X

Means: s subscript two assigns the set one, two to capital X

1 occurrence in this chapter

Equation form expr-a8390844f44cd629

Vin\Obj V_i^n

Read as: the relation variable capital V with index i and arity n

Means: the relation variable capital V with index i and arity n

1 occurrence in this chapter

Equation form expr-a839449779e03ab1

M⊨Inf\Sat{M}{\fn{Inf}}

Read as: structure M satisfies the following: Inf

Means: structure M satisfies the following: Inf

3 occurrences in this chapter

Equation form expr-a8d1b7373d5c491a

fin\Obj{f^n_i}

Read as: the function symbol f with index i and arity n

Means: the function symbol f with index i and arity n

1 occurrence in this chapter

Equation form expr-a906f1de6d7e082a

u0n\Obj u_0^n

Read as: the function variable u with index zero and arity n

Means: the function variable u with index zero and arity n

1 occurrence in this chapter

Equation form expr-a93de6f6a25752e6

ValsM(t)=s(u)(ValsM(t1),…,ValsM(tn)).\Value{\indfrm}{M}[s] = s(u)(\Value{t_1}{M}[s], \ldots, \Value{t_n}{M}[s]).

Read as: the value of term t in structure M under assignment s equals the function assigned to u by s applied, in order, to the values in structure M under s of t subscript one through t subscript n

Means: the value of term t in structure M under assignment s equals the function assigned to u by s applied, in order, to the values in structure M under s of t subscript one through t subscript n

1 occurrence in this chapter

Equation form expr-a9fa55216afef278

Inf≡∃u(∀x∀y(u(x)=u(y)→x=y)∧∃y∀xy≠u(x)).\fn{Inf} \ident \lexists[u][(\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land \lexists[y][\lforall[x][\eq/[y][u(x)]]])].

Read as: Inf abbreviates: there exists a unary function u such that both of the following hold: for all objects lower case x and lower case y, if u of x equals u of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from u of x

Means: Inf abbreviates: there exists a unary function u such that both of the following hold: for all objects lower case x and lower case y, if u of x equals u of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from u of x

1 occurrence in this chapter

Equation form expr-aae90dfb1ac24e1a

s(Y)s(Y)

Read as: the relation assigned to capital Y by s

Means: the relation assigned to capital Y by s

1 occurrence in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma logically entails A

Means: Gamma logically entails A

1 occurrence in this chapter

Equation form expr-abb91df564528847

Vin\Obj{V_i^n}

Read as: the relation variable capital V with index i and arity n

Means: the relation variable capital V with index i and arity n

1 occurrence in this chapter

Equation form expr-ad0d65f481b0e65d

∀v0(P01(v0)∨¬P01(v0))\lforall[\Obj{v_0}][(\Obj{P^1_0}(\Obj{v_0}) \lor \lnot \Obj{P^1_0}(\Obj{v_0}))]

Read as: for every object variable v subscript zero: P subscript zero holds of v subscript zero, or P subscript zero does not hold of v subscript zero

Means: for every object variable v subscript zero: P subscript zero holds of v subscript zero, or P subscript zero does not hold of v subscript zero

1 occurrence in this chapter

Equation form expr-ae5a050c4657343f

M⊨A→∀X∀yX(y)\Sat{M}{!A \lif \lforall[X][\lforall[y][X(y)]]}

Read as: structure M satisfies the following: if A, then for every unary relation capital X and every object lower case y, capital X holds of y

Means: structure M satisfies the following: if A, then for every unary relation capital X and every object lower case y, capital X holds of y

1 occurrence in this chapter

Equation form expr-afe4b2d5a2c81954

M⊨Γ\Sat{M}{\Gamma}

Read as: structure M satisfies the following: every sentence in Gamma

Means: structure M satisfies the following: every sentence in Gamma

2 occurrences in this chapter

Equation form expr-b124dbaa249a3d08

M⊆|M|nM \subseteq \Domain{M}^n

Read as: the relation M is a subset of the set of n tuples from the domain of structure M

Means: the relation M is a subset of the set of n tuples from the domain of structure M

3 occurrences in this chapter

Equation form expr-b24c2720089cdd3e

↔\liff

Read as: the biconditional connective

Means: the biconditional connective

1 occurrence in this chapter

Equation form expr-b299a756fe5b9f2c

A∨B!A \lor !B

Read as: A or B

Means: A or B

1 occurrence in this chapter

Equation form expr-b334305c8a49a621

M,s[M/X]⊨(X(z)∧∀x(X(x)→X(u(x))))\Sat{M}{(X(z) \land \lforall[x][(X(x) \lif X(u(x)))])}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: capital X holds of lower case z, and for every object lower case x, if capital X holds of x then capital X holds of u of x

1 occurrence in this chapter

Equation form expr-b50bb8940da5b931

L\Lang{L}

Read as: the language L

Means: the language L

3 occurrences in this chapter

Equation form expr-b54bd60af800238a

|M|={1,2,3}\Domain{M} = \{1, 2, 3\}

Read as: the domain of structure M is the set one, two, three

Means: the domain of structure M is the set one, two, three

2 occurrences in this chapter

Equation form expr-b642ce7b79187b05

M,s[f/u]⊨B\Sat{M}{!B}[\Subst{s}{f}{u}]

Read as: structure M under assignment s modified to assign the function f to u satisfies the following: B

Means: structure M under assignment s modified to assign the function f to u satisfies the following: B

2 occurrences in this chapter

Equation form expr-b87dfbb4955eebf7

M,s⊨A\Sat{M}{\indfrm}[s]

Read as: structure M under assignment s satisfies A

Means: structure M under assignment s satisfies A

5 occurrences in this chapter

Equation form expr-b919ee106cef8614

fM\Assign{f}{M}

Read as: the interpretation of f in structure M

Means: the interpretation of f in structure M

2 occurrences in this chapter

Equation form expr-b9b6cd48f4bb3349

s(uin):|M|n→|M|s(\Obj{u_i^n})\colon \Domain{M}^n \to \Domain{M}

Read as: the value assigned by s to the function variable u with index i and arity n is a function from n tuples of domain elements to domain elements of structure M

Means: the value assigned by s to the function variable u with index i and arity n is a function from n tuples of domain elements to domain elements of structure M

1 occurrence in this chapter

Equation form expr-ba25f7136d9d786f

s(y)=bs(y) = b

Read as: s assigns b to lower case y

Means: s assigns b to lower case y

1 occurrence in this chapter

Equation form expr-bb4244c5ceebae5d

M,s[N/Y]⊨∃yY(y)\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]

Read as: structure M under assignment s modified to assign N to capital Y satisfies the following: there exists an object lower case y such that capital Y holds of y

Means: structure M under assignment s modified to assign N to capital Y satisfies the following: there exists an object lower case y such that capital Y holds of y

1 occurrence in this chapter

Equation form expr-bb71e3b730738669

s[M/y]={Mif y≡Xs(y)otherwise.\Subst{s}{M}{y} = \begin{cases} M & \text{if } y \ident X\\ s(y) & \text{otherwise}. \end{cases}

Read as: the source writes assignment s modified to assign M to lower case y, equals the following cases: M if lower case y is the very same variable as capital X; and s of lower case y otherwise

Means: the source writes assignment s modified to assign M to lower case y, equals the following cases: M if lower case y is the very same variable as capital X; and s of lower case y otherwise

1 occurrence in this chapter

Equation form expr-bbeebd879e1dff69

ZZ

Read as: capital Z

Means: capital Z

1 occurrence in this chapter

Equation form expr-bc52480e6f6e75b7

M,s1⊨∀z(X(z)↔¬Y(z))\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s_1]

Read as: structure M under assignment s subscript one satisfies the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

Means: structure M under assignment s subscript one satisfies the following: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-be8dcefb61dddd9f

t1t_1

Read as: t subscript one

Means: t subscript one

2 occurrences in this chapter

Equation form expr-be9ea0b237010de9

s[f/u]\Subst{s}{f}{u}

Read as: assignment s modified to assign the function f to u

Means: assignment s modified to assign the function f to u

1 occurrence in this chapter

Equation form expr-bed3cc022629d507

⟨a,b⟩∈R\tuple{a,b} \in R

Read as: the ordered pair a, b belongs to R

Means: the ordered pair a, b belongs to R

1 occurrence in this chapter

Equation form expr-bf1df883a744abb3

A∧B!A \land !B

Read as: A and B

Means: A and B

1 occurrence in this chapter

Equation form expr-bfaa863bc723ff73

∀X(A→(B→∀xX(x))→∀xX(x))\lforall[X][(!A \lif (!B \lif \lforall[x][X(x)])\lif \lforall[x][X(x)])]

Read as: for every unary relation capital X, the following parenthesized chain of conditionals: A implies, open inner parenthesis, B implies for every object lower case x capital X holds of x, close inner parenthesis, implies for every object lower case x capital X holds of x. End of the outer parenthesized chain

Means: for every unary relation capital X, the following parenthesized chain of conditionals: A implies, open inner parenthesis, B implies for every object lower case x capital X holds of x, close inner parenthesis, implies for every object lower case x capital X holds of x. End of the outer parenthesized chain

1 occurrence in this chapter

Equation form expr-c065192bf1bb57cf

∀X∃Y(∃yY(y)∧∀z(X(z)↔¬Y(z)))\lforall[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]

Read as: for every unary relation capital X: there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

Means: for every unary relation capital X: there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-c277cb0200a3b6b2

V01\Obj{V^1_0}

Read as: the unary relation variable capital V subscript zero

Means: the unary relation variable capital V subscript zero

3 occurrences in this chapter

Equation form expr-c2ed7a9fa236bbf0

tnt_n

Read as: t subscript n

Means: t subscript n

2 occurrences in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not A

Means: not A

1 occurrence in this chapter

Equation form expr-ca5b51d3bfeb95d7

s[M/X]\Subst{s}{M}{X}

Read as: assignment s modified to assign the relation M to capital X

Means: assignment s modified to assign the relation M to capital X

1 occurrence in this chapter

Equation form expr-ca6c5f671cdc3f3a

s(X)s(X)

Read as: the relation assigned to capital X by s

Means: the relation assigned to capital X by s

1 occurrence in this chapter

Equation form expr-ca978112ca1bbdca

aa

Read as: a

Means: a

4 occurrences in this chapter

Equation form expr-cd210f762dcfbd1f

∀uA\lforall[u][!A]

Read as: the expression, quote, for every function u, A, end quote

Means: the expression, quote, for every function u, A, end quote

1 occurrence in this chapter

Equation form expr-cfbeea05e35bda03

M,s⊨∀x∀y(u(x)=u(y)→x=y)∧∃y∀xy≠u(x)\Sat{M}{\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land \lexists[y][\lforall[x][\eq/[y][u(x)]]]}[s]

Read as: structure M under assignment s satisfies the following: for all objects lower case x and lower case y, if u of x equals u of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from u of x

Means: structure M under assignment s satisfies the following: for all objects lower case x and lower case y, if u of x equals u of y then x equals y; and there exists an object lower case y such that, for every object lower case x, y is different from u of x

1 occurrence in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: the conditional connective

Means: the conditional connective

4 occurrences in this chapter

Equation form expr-d0b4e34ba831be62

M≠|M|M \neq \Domain{M}

Read as: the set M is not the entire domain of structure M

Means: the set M is not the entire domain of structure M

1 occurrence in this chapter

Equation form expr-d3177012dcf9ccb6

m∈|M|m \in \Domain{M}

Read as: m belongs to the domain of structure M

Means: m belongs to the domain of structure M

1 occurrence in this chapter

Equation form expr-d32f3c9fb6efaad5

PM\Assign{P}{M}

Read as: the interpretation of P in structure M

Means: the interpretation of P in structure M

1 occurrence in this chapter

Equation form expr-d47d71c1ba1c7d9d

M,s⊭X(y)\Sat/{M}{X(y)}[s]

Read as: structure M under assignment s does not satisfy the following: capital X holds of lower case y

Means: structure M under assignment s does not satisfy the following: capital X holds of lower case y

1 occurrence in this chapter

Equation form expr-d4d5d7f305df615f

M,s2[2/z]⊭¬Y(z)\Sat/{M}{\lnot \Atom{Y}{z}}[\Subst{s_2}{2}{z}]

Read as: structure M under assignment s subscript two modified to assign two to lower case z does not satisfy the following: capital Y does not hold of lower case z

Means: structure M under assignment s subscript two modified to assign two to lower case z does not satisfy the following: capital Y does not hold of lower case z

1 occurrence in this chapter

Equation form expr-d6e527002ded4d50

RM\Assign{R}{M}

Read as: the interpretation of R in structure M

Means: the interpretation of R in structure M

2 occurrences in this chapter

Equation form expr-d966d23c9cfb7083

M,s⊨R*(X)\Sat{M}{R^*(X)}[s]

Read as: structure M under assignment s satisfies the following: R star of capital X

Means: structure M under assignment s satisfies the following: R star of capital X

1 occurrence in this chapter

Equation form expr-daf9c4c11daaf7bb

Inf∧Count\fn{Inf} \land \fn{Count}

Read as: Inf and Count

Means: Inf and Count

1 occurrence in this chapter

Equation form expr-dd5c62a21346cd7c

s(y)=a∈|M|s(y) = a \in \Domain{M}

Read as: s of lower case y equals a, which belongs to the domain of structure M

Means: s of lower case y equals a, which belongs to the domain of structure M

1 occurrence in this chapter

Equation form expr-dd7d690b005e955c

M⊨A\Sat{M}{!A}

Read as: structure M satisfies the following: A

Means: structure M satisfies the following: A

2 occurrences in this chapter

Equation form expr-dd8c6192f01163b5

s[M/X]∼Xs\varAssign{\Subst{s}{M}{X}}{s}{X}

Read as: s modified to assign M to capital X is a capital X variant of s

Means: s modified to assign M to capital X is a capital X variant of s

1 occurrence in this chapter

Equation form expr-de39c10aaee232b7

∀z(X(z)↔¬Y(z))\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]

Read as: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

Means: for every object lower case z: capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-de494def87339346

R(c1,c2)R(c_1, c_2)

Read as: R relates c subscript one to c subscript two

Means: R relates c subscript one to c subscript two

1 occurrence in this chapter

Equation form expr-defa158f709798c0

M⊨¬A\Sat{M}{\lnot !A}

Read as: structure M satisfies the following: not A

Means: structure M satisfies the following: not A

1 occurrence in this chapter

Equation form expr-df04f94df598e408

a≠ba \neq b

Read as: a is different from b

Means: a is different from b

1 occurrence in this chapter

Equation form expr-e0d945b61a35a200

k=0k = 0

Read as: k equals zero

Means: k equals zero

1 occurrence in this chapter

Equation form expr-e0fa6df3cd97a6bf

R⊆R*R \subseteq R^*

Read as: R is included in R star

Means: R is included in R star

1 occurrence in this chapter

Equation form expr-e3b98a4da31a127d

tt

Read as: t

Means: t

1 occurrence in this chapter

Equation form expr-e5033ee847ef8ebe

M,s2[2/z]⊨X(z)\Sat{M}{\Atom{X}{z}}[\Subst{s_2}{2}{z}]

Read as: structure M under assignment s subscript two modified to assign two to lower case z satisfies the following: capital X holds of lower case z

Means: structure M under assignment s subscript two modified to assign two to lower case z satisfies the following: capital X holds of lower case z

1 occurrence in this chapter

Equation form expr-e5875861fc9e642a

M,s⊨AR(x,y)\Sat{M}{!A_R(x, y)}[s]

Read as: structure M under assignment s satisfies the following: A subscript R of lower case x and lower case y

Means: structure M under assignment s satisfies the following: A subscript R of lower case x and lower case y

1 occurrence in this chapter

Equation form expr-e5905f2069359c14

s(u)s(u)

Read as: the function assigned to u by s

Means: the function assigned to u by s

2 occurrences in this chapter

Equation form expr-e5fe9071b8578493

M,s[M/X]⊨B\Sat{M}{!B}[\Subst{s}{M}{X}]

Read as: structure M under assignment s modified to assign the relation M to capital X satisfies the following: B

Means: structure M under assignment s modified to assign the relation M to capital X satisfies the following: B

2 occurrences in this chapter

Equation form expr-e9577d4e4232e0c8

mkm_k

Read as: m subscript k

Means: m subscript k

2 occurrences in this chapter

Equation form expr-ea9014e1666c861b

∃X∃Y(∃yY(y)∧∀z(X(z)↔¬Y(z)))\lexists[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]

Read as: there exists a unary relation capital X such that there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

Means: there exists a unary relation capital X such that there exists a unary relation capital Y such that both of the following hold: there exists an object lower case y such that capital Y holds of y; and for every object lower case z, capital X holds of z if and only if capital Y does not hold of z

1 occurrence in this chapter

Equation form expr-ee1f47f4a246684f

s(vi)∈|M|s(\Obj{v_i}) \in \Domain{M}

Read as: the value assigned by s to the object variable v subscript i belongs to the domain of structure M

Means: the value assigned by s to the object variable v subscript i belongs to the domain of structure M

1 occurrence in this chapter

Equation form expr-efa51acdf0e7c3c4

L\Lang L

Read as: the language L

Means: the language L

5 occurrences in this chapter

Equation form expr-f0e8aa156079e338

X(t1,…,tn)\Atom{X}{t_1,\ldots, t_n}

Read as: capital X applied to the terms t subscript one through t subscript n

Means: capital X applied to the terms t subscript one through t subscript n

1 occurrence in this chapter

Equation form expr-f2708d9e29712594

∃\lexists

Read as: the existential quantifier

Means: the existential quantifier

1 occurrence in this chapter

Equation form expr-f7520751289273ec

m0∈Mm_0 \in M

Read as: m subscript zero belongs to M

Means: m subscript zero belongs to M

2 occurrences in this chapter

Equation form expr-f7abed8e6be0a024

R*(a,b)R^*(a,b)

Read as: R star relates a to b

Means: R star relates a to b

1 occurrence in this chapter

Equation form expr-f96b80a9f5e1e628

s1(Y)={3}s_1(Y) = \{3\}

Read as: s subscript one assigns the singleton set three to capital Y

Means: s subscript one assigns the singleton set three to capital Y

1 occurrence in this chapter

Equation form expr-f9ae8fe6983f49c2

fM:|M|→|M|\Assign{f}{M}: \Domain{M} \to \Domain{M}

Read as: the interpretation of f in structure M is a function from the domain of M to itself

Means: the interpretation of f in structure M is a function from the domain of M to itself

1 occurrence in this chapter

Equation form expr-ff5451cb5239c0ba

∀V01∀v0(V01(v0)∨¬V01(v0))\lforall[\Obj{V^1_0}][\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj{v_0}) \lor \lnot \Obj{V^1_0}(\Obj{v_0}))]]

Read as: for every unary relation variable capital V subscript zero: for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

Means: for every unary relation variable capital V subscript zero: for every object variable v subscript zero: capital V subscript zero holds of v subscript zero, or capital V subscript zero does not hold of v subscript zero

1 occurrence in this chapter

Equation form expr-ffb94af5367c8588

f:|M|n→|M|f\colon \Domain{M}^n \to \Domain{M}

Read as: f is a function from n tuples of domain elements to domain elements of structure M

Means: f is a function from n tuples of domain elements to domain elements of structure M

3 occurrences in this chapter

Definition of second order terms

Extend the first order term definition by allowing a function variable of arity n to be applied to n terms. The resulting application is itself a term. The original first order definition remains linked.

Source

Definition of second order formulas

Extend first order formulas by allowing relation variables applied to the matching number of terms, and universal and existential quantification over function and relation variables. Relation variables and function variables remain distinct from fixed nonlogical symbols.

Source

Second order variable assignments

An assignment gives each object variable a domain element, each n place relation variable a subset of the n fold Cartesian power of the domain, and each n place function variable a function from that Cartesian power into the domain.

Source

Value of a function variable application

Evaluate the argument terms in structure M under assignment s, in their displayed order. Then apply the function that s assigns to u to the resulting n tuple. This extends the first order definition of term value.

Source

Variants of variable assignments

An x variant of s agrees with s at every variable other than possibly x. The same definition applies when the distinguished variable is a second order relation or function variable.

Source

Changing the value of one variable in an assignment

The intended clauses change only the indicated object, relation, or function variable and leave all other assignments unchanged. Three displayed left sides in the source use the test variable y in the replacement slot and omit evaluation at y. Their exact notation is preserved with a source caveat; it is not silently presented as correct.

Source

Satisfaction clauses for second order logic

A relation variable application is satisfied when the tuple of argument values belongs to the assigned relation. Universal relation quantification considers every relation of the correct arity; existential relation quantification considers at least one. The corresponding function clauses range over all functions, or at least one function, of the correct arity. Each clause modifies only the quantified variable in the assignment.

Source

Example of complementary unary relations

Capital X and capital Y are free relation variables, while the object variable z is bound. Satisfaction of their displayed biconditional means their assigned subsets are complements in the whole domain. On the domain one, two, three, the assignments one, two versus three work. The overlapping assignments one, two versus two, three fail at the element two.

Source

Existence of a nonempty complement

The first displayed formula requires a nonempty unary relation Y complementary to X. It is satisfied exactly when the relation assigned to X is not the whole domain. Universally quantifying X therefore yields a false sentence; existentially quantifying X yields a true sentence in every nonempty structure, using the empty set for X.

Source

Defining negation with a universally false second order sentence

The sentence saying every unary relation holds of every object is false in every nonempty structure because the empty relation is among the quantified relations. A conditional from A to this sentence therefore has the same truth conditions as not A.

Source

Exercise defining conjunction and disjunction

The exercise asks for a proof that the displayed second order conditional construction is equivalent to conjunction, and for a formula equivalent to disjunction using only universal quantification and the conditional. The source chain of conditionals has a grouping caveat. No proof or disjunction formula is supplied by this edition.

Source

Second order validity

A second order sentence is valid when every structure satisfies it, using the standard second order satisfaction relation.

Source

Second order entailment

A set Gamma of second order sentences entails A when every structure satisfying every member of Gamma also satisfies A.

Source

Second order satisfiability

Gamma is satisfiable when at least one structure satisfies every sentence in Gamma. If no such structure exists, Gamma is unsatisfiable.

Source

Definability of a binary relation

A formula with only x and y free defines R in structure M when, for every assignment sending x to a and y to b, that formula is satisfied exactly when the ordered pair a, b belongs to R.

Source

Defining identity without the equality symbol

Two objects are identical exactly when they belong to all the same subsets of the domain. The example expresses this by universally quantifying a unary relation variable and comparing its truth at x and y with a biconditional.

Source

Exercise defining identity with a one way conditional

Show that universal quantification over X of the conditional from X of x to X of y defines identity. The displayed connective is a conditional, not a biconditional. The exercise remains unsolved.

Source

Second order definition of transitive closure

R star contains pairs connected by a positive length finite R path. The first auxiliary formula says X contains R and is transitive. The final formula requires X itself to meet those conditions and be included in every relation Y meeting them. This defines the least transitive relation containing R; no reflexivity requirement is added.

Source

Two conditions for a transitive relation containing R

The multiline display is one conjunction, not a proof tree. Its first conjunct says every R pair is an X pair. Its second conjunct says two composable X pairs imply the composite X pair. Each conjunct binds its own object variables.

Source

Inf characterizes infinite domains

The source proves that Inf is satisfied exactly when the domain admits an injective nonsurjective self function, its characterization of infinity. The forward direction extracts the function from the assignment; the converse assigns an existing such function to u.

Source

Count characterizes enumerable domains

Count asserts that some object and some unary function generate the domain in the sense that every subset containing that object and closed under that function is the whole domain. The proof uses an enumeration in one direction and the set of finite iterates in the other. The finite last element convention appears in the preceding prose and is omitted in the proof's successor prescription; that omission is disclosed.

Source

Exercise directly describing denumerable domains

Inf and Count together characterize denumerable domains. The exercise asks the reader to modify Count so that a different single sentence directly expresses denumerability, and prove the characterization. No modification or proof is added.

Source

Cross-reference reference-000787

the definition of first order terms

Source occurrence

Cross-reference reference-000788

the definition of first order formulas

Source occurrence

Cross-reference reference-000789

the definition of first order satisfaction

Source occurrence

Source disclosures

Source-generated case expression tr039-source-macro-0001

t≡u(t1,…,tn)t \ident \Atom{u}{t_1, \ldots, t_n}

Read as: Case: t is syntactically u applied to t subscript one through t subscript n.

Read in context source

Source-generated case expression tr039-source-macro-0002

A≡Xn(t1,…,tn)!A \ident \Atom{X^n}{t_1, \dots, t_n}

Read as: Case: A is syntactically capital X of arity n applied to t subscript one through t subscript n.

Read in context source

Source-generated case expression tr039-source-macro-0003

A≡∀XB!A \ident \lforall[X][!B]

Read as: Case: A is syntactically the formula for every relation capital X, B.

Read in context source

Source-generated case expression tr039-source-macro-0004

A≡∃XB!A \ident \lexists[X][!B]

Read as: Case: A is syntactically the formula there exists a relation capital X such that B.

Read in context source

Source-generated case expression tr039-source-macro-0005

A≡∀uB!A \ident \lforall[u][!B]

Read as: Case: A is syntactically the formula for every function u, B.

Read in context source

Source-generated case expression tr039-source-macro-0006

A≡∃uB!A \ident \lexists[u][!B]

Read as: Case: A is syntactically the formula there exists a function u such that B.

Read in context source