Second-order logic

Metatheory of Second-order Logic

Equation form expr-03911c48ca11189d

N={ValM(n¯):n∈ℕ}N = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}

Read as: N is the set of values in structure M of the numeral for n, as n ranges over the natural numbers

Means: N is the set of values in structure M of the numeral for n, as n ranges over the natural numbers

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: s

1 occurrence in this chapter

Equation form expr-05f635e6ef2c8851

B(x,Y)≡Y(x)∧∀y(Y(y)→Y(y′))!B(x, Y) \ident Y(x) \land \lforall[y][(Y(y) \lif Y(y'))]

Read as: B of lower case x and capital Y abbreviates: capital Y holds of x, and for every lower case y, if capital Y holds of y then it holds of the successor of y

Means: B of lower case x and capital Y abbreviates: capital Y holds of x, and for every lower case y, if capital Y holds of y then it holds of the successor of y

1 occurrence in this chapter

Equation form expr-07af73b66908fe39

M,s⊨X(0)\Sat{M}{X(\Obj{0})}[s]

Read as: structure M under assignment s satisfies: capital X holds of zero

Means: structure M under assignment s satisfies: capital X holds of zero

1 occurrence in this chapter

Equation form expr-0bfe935e70c321c7

uu

Read as: u

Means: u

2 occurrences in this chapter

Equation form expr-119f3bcdda6eecb6

u(n′)=u(n)′u(n')=u(n)'

Read as: u of the successor of n equals the successor of u of n

Means: u of the successor of n equals the successor of u of n

1 occurrence in this chapter

Equation form expr-11b41534cdf61584

u′′u''

Read as: the function variable u double prime

Means: the function variable u double prime

1 occurrence in this chapter

Equation form expr-12c0ee82d50e69d4

¬Count\lnot \fn{Count}

Read as: not Count

Means: not Count

1 occurrence in this chapter

Equation form expr-1356c5c74760e2dd

A≤(x,y)!A_\le(x, y)

Read as: A subscript less than or equal to, of lower case x and lower case y

Means: A subscript less than or equal to, of lower case x and lower case y

1 occurrence in this chapter

Equation form expr-153d5553d5667041

℘(ℕ)\Pow{\Nat}

Read as: the power set of the natural numbers

Means: the power set of the natural numbers

1 occurrence in this chapter

Equation form expr-199649af431f6dc9

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

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

Means: N is a subset of the domain of structure M

1 occurrence in this chapter

Equation form expr-1a4057b9c504ea3e

ValM(n¯)\Value{\num{n}}{M}

Read as: the value of the numeral for n in structure M

Means: the value of the numeral for n in structure M

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

3 occurrences in this chapter

Equation form expr-1c9ccfbd01237d98

A≤(x,y)≡∀Y(B(x,Y)→Y(y))!A_\le(x, y) \ident \lforall[Y][(!B(x, Y) \lif Y(y))]

Read as: A subscript less than or equal to, of lower case x and lower case y, abbreviates: for every unary relation capital Y, if B of x and capital Y then capital Y holds of y

Means: A subscript less than or equal to, of lower case x and lower case y, abbreviates: for every unary relation capital Y, if B of x and capital Y then capital Y holds of y

1 occurrence in this chapter

Equation form expr-1cbe9e80cbbaaa9c

PA2⊨A\Th{PA^2} \Entails !A

Read as: the theory P A superscript two logically entails A

Means: the theory P A superscript two logically entails A

3 occurrences in this chapter

Equation form expr-2244fed9c082d12b

x=ValM(n¯)x = \Value{\num{n}}{M}

Read as: lower case x equals the value of the numeral for n in structure M

Means: lower case x equals the value of the numeral for n in structure M

1 occurrence in this chapter

Equation form expr-236f9f346108708a

′M(x)\Assign{\prime}{M}(x)

Read as: the successor function of structure M applied to lower case x

Means: the successor function of structure M applied to lower case x

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

1 occurrence in this chapter

Equation form expr-26cef8ee8850deb8

N⊨A≤(n¯,m¯)\Sat{N}{!A_\le(\num n, \num m)}

Read as: the standard natural number structure satisfies A subscript less than or equal to, applied to the numeral for n and the numeral for m

Means: the standard natural number structure satisfies A subscript less than or equal to, applied to the numeral for n and the numeral for m

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

6 occurrences in this chapter

Equation form expr-346e64715a2113ac

f:ℕ→Sent(L)f\colon \Nat \to \Sent[L]

Read as: f from the natural numbers to the sentences of language L

Means: f from the natural numbers to the sentences of language L

1 occurrence in this chapter

Equation form expr-349ba76d907adfab

×\times

Read as: multiplication

Means: multiplication

2 occurrences in this chapter

Equation form expr-3aa931e2e73b177c

f:ℕ→Sent(LA)f\colon \Nat \to \Sent[L_A]

Read as: f from the natural numbers to the sentences of the language of arithmetic, L subscript A

Means: f from the natural numbers to the sentences of the language of arithmetic, L subscript A

1 occurrence in this chapter

Equation form expr-3bd52a5f8fc05fb1

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

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

Means: lower case x in the domain of structure M

2 occurrences in this chapter

Equation form expr-3c25d37aa3f2b6e9

x∈Nx \in N

Read as: lower case x belongs to N

Means: lower case x belongs to N

1 occurrence in this chapter

Equation form expr-3c36c1104eda1897

M⊨∀X((X(0)∧∀x(X(x)→X(x′)))→∀xX(x)), thusM,s⊨(X(0)∧∀x(X(x)→X(x′)))→∀xX(x).\Sat{M}{\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)])]}, & \text{ thus}\\ \Sat{M}{(X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)]}[s]. &

Read as: Structure M satisfies: for every unary relation capital X: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x. Thus, structure M under assignment s satisfies: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x

Means: Structure M satisfies: for every unary relation capital X: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x. Thus, structure M under assignment s satisfies: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x

1 occurrence in this chapter

Equation form expr-3d2df79065b6f165

Q\Th{Q}

Read as: the theory Q

Means: the theory Q

3 occurrences in this chapter

Equation form expr-3f1b6dc519af96a7

′\prime

Read as: the successor symbol

Means: the successor symbol

1 occurrence in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: structure M

Means: structure M

3 occurrences in this chapter

Equation form expr-43d16cb8a9bca153

k+l=mk+l=m

Read as: k plus l equals m

Means: k plus l equals m

2 occurrences in this chapter

Equation form expr-4a5c2981ff3f2546

A≥n∈Γ!A^{\ge n} \in \Gamma

Read as: A superscript at least n belongs to Gamma

Means: A superscript at least n belongs to Gamma

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: capital X

Means: capital X

1 occurrence in this chapter

Equation form expr-4c268426039b3d02

Bf(x,y)!B_f(x, y)

Read as: B subscript f of lower case x and lower case y

Means: B subscript f of lower case x and lower case y

1 occurrence in this chapter

Equation form expr-4e1259f09671da63

ValM(n¯)∈|M|\Value{\num{n}}{M} \in \Domain{M}

Read as: the value of the numeral for n in structure M belongs to the domain of M

Means: the value of the numeral for n in structure M belongs to the domain of M

1 occurrence in this chapter

Equation form expr-4ecc1d2041326535

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 x and y, if u of x equals u of y then x equals y. And there exists an object y such that for every object 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 x and y, if u of x equals u of y then x equals y. And there exists an object y such that for every object x, y is different from u of x

1 occurrence in this chapter

Equation form expr-501c3ef8886861db

Γ0⊨/A\Gamma_0 \Entails/ !A

Read as: Gamma subscript zero does not logically entail A

Means: Gamma subscript zero does not logically entail A

1 occurrence in this chapter

Equation form expr-50571d5a47e7af9e

M⊨P→A\Sat{M}{!P \lif !A}

Read as: structure M satisfies the conditional if P then A

Means: structure M satisfies the conditional if P then A

1 occurrence in this chapter

Equation form expr-53521c257ae7d657

A≥k∈Γ!A^{\ge k} \in \Gamma

Read as: A superscript at least k belongs to Gamma

Means: A superscript at least k belongs to Gamma

1 occurrence in this chapter

Equation form expr-562c9fff831aa3e6

P!P

Read as: P

Means: P

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

9 occurrences in this chapter

Equation form expr-57a641fd810b5a91

⊢\Proves

Read as: the derivability relation

Means: the derivability relation

1 occurrence in this chapter

Equation form expr-594e519ae499312b

zz

Read as: lower case z

Means: lower case z

1 occurrence in this chapter

Equation form expr-5afa20230f875253

n∈ℕn \in \Nat

Read as: n is a natural number

Means: n is a natural number

2 occurrences in this chapter

Equation form expr-5b63a60fdb499c3a

N\Struct{N}

Read as: the standard structure of natural numbers

Means: the standard structure of natural numbers

3 occurrences in this chapter

Equation form expr-5cd888c50377bc38

|M|={ValM(n¯):n∈ℕ}\Domain{M} = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}

Read as: the domain of structure M equals the set of values in M of the numeral for n, as n ranges over the natural numbers

Means: the domain of structure M equals the set of values in M of the numeral for n, as n ranges over the natural numbers

1 occurrence in this chapter

Equation form expr-6193864491e4d7b1

N⊨A\Sat{N}{!A}

Read as: the standard natural number structure satisfies A

Means: the standard natural number structure satisfies A

2 occurrences in this chapter

Equation form expr-6dde76d58bab9736

∀x(X(x)→X(x′))\lforall[x][(X(x) \lif X(x'))]

Read as: for every lower case x, if capital X holds of x then capital X holds of the successor of x

Means: for every lower case x, if capital X holds of x then capital X holds of the successor of x

1 occurrence in this chapter

Equation form expr-6e82ac27792a9ac6

ℝ\Real

Read as: the real numbers

Means: the real numbers

1 occurrence in this chapter

Equation form expr-72758d600b83e3d1

m=u(l)m = u(l)

Read as: m equals u of l

Means: m equals u of l

1 occurrence in this chapter

Equation form expr-72b77499f524bf4b

{m:n≤m}⊆Y\Setabs{m}{n \le m} \subseteq Y

Read as: the set of m such that n is less than or equal to m is a subset of capital Y

Means: the set of m such that n is less than or equal to m is a subset of capital Y

1 occurrence in this chapter

Equation form expr-72dfcfb0c470ac25

LL

Read as: the binary relation variable L

Means: the binary relation variable L

1 occurrence in this chapter

Equation form expr-761a69f8c3dd38ec

ValM(0)∈N\Value{\Obj{0}}{M} \in N

Read as: the value of the constant zero in structure M belongs to N

Means: the value of the constant zero in structure M belongs to N

1 occurrence in this chapter

Equation form expr-7737c1b6f1e8ceb7

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

Read as: structure M satisfies not Inf

Means: structure M satisfies not Inf

1 occurrence in this chapter

Equation form expr-79d4c7f9c8579543

ℕ\Nat

Read as: the natural numbers

Means: the natural numbers

1 occurrence in this chapter

Equation form expr-7a03384e6e8b8519

≤\le

Read as: the less than or equal to relation

Means: the less than or equal to relation

2 occurrences in this chapter

Equation form expr-7f024b2d7f1db4d4

n¯\num{n}

Read as: the numeral for n

Means: the numeral for n

1 occurrence in this chapter

Equation form expr-81aa5a490db29cc9

A(x)!A(x)

Read as: A of lower case x

Means: A of lower case x

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

5 occurrences in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: k

3 occurrences in this chapter

Equation form expr-859f79875f7ec4e6

M⊨PA2\Sat{M}{\Th{PA^2}}

Read as: structure M satisfies the theory P A superscript two

Means: structure M satisfies the theory P A superscript two

2 occurrences in this chapter

Equation form expr-8930429e1fba8298

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

Read as: capital X equals the whole domain of structure M

Means: capital X equals the whole domain of structure M

1 occurrence in this chapter

Equation form expr-8ce86a6ae65d3692

NN

Read as: the set N

Means: the set N

1 occurrence in this chapter

Equation form expr-931b68275b41f73c

N⊨A+(k¯,l¯,m¯)\Sat{N}{!A_+(\num k, \num l, \num m)}

Read as: the standard natural number structure satisfies A subscript plus applied to the numeral for k, the numeral for l, and the numeral for m

Means: the standard natural number structure satisfies A subscript plus applied to the numeral for k, the numeral for l, and the numeral for m

1 occurrence in this chapter

Equation form expr-977f19219c49b665

0M\Assign{\Obj{0}}{M}

Read as: the interpretation of the constant zero in structure M

Means: the interpretation of the constant zero in structure M

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 a unary function u such that for every unary relation capital X, if capital X holds of z and, for every lower case x, capital X holding of x implies capital X holding of u of x, then capital X holds of every lower case x

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

1 occurrence in this chapter

Equation form expr-9cf0b0db68282d5a

∀z∀u∀u′∀u′′∀L(P′→A′)\lforall[z][\lforall[u][\lforall[u'][\lforall[u''][\lforall[L][(!P' \lif !A')]]]]]

Read as: for every object lower case z, every unary function u, every binary function u prime, every binary function u double prime, and every binary relation L: if P prime then A prime

Means: for every object lower case z, every unary function u, every binary function u prime, every binary function u double prime, and every binary relation L: if P prime then A prime

1 occurrence in this chapter

Equation form expr-9dc71e6c9f690c16

∃xBf(x,y)\lexists[x][!B_f(x, y)]

Read as: there exists a lower case x such that B subscript f of x and lower case y

Means: there exists a lower case x such that B subscript f of x and lower case y

1 occurrence in this chapter

Equation form expr-9ee50f8fa8a24921

∀xx′≠0∀x∀y(x′=y′→x=y)∀x(x=0∨∃yx=y′)∀x(x+0)=x∀x∀y(x+y′)=(x+y)′∀x(x×0)=0∀x∀y(x×y′)=((x×y)+x)∀x∀y(x<y↔∃z(z′+x)=y)plus all sentences of the form(A(0)∧∀x(A(x)→A(x′)))→∀xA(x).& \lforall[x][\eq/[x'][\Obj 0]]\\ & \lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]]\\ & \lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])]\\ & \lforall[x][\eq[(x + \Obj 0)][x]]\\ & \lforall[x][\lforall[y][\eq[(x + y')][(x + y)']]]\\ & \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]]\\ & \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]]\\ & \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]]\\ \intertext{plus all sentences of the form} & (!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)].

Read as: Eight arithmetic axioms. First: for every x, the successor of x is not zero. Second: for all x and y, if the successor of x equals the successor of y then x equals y. Third: for every x, x equals zero or there exists y such that x equals the successor of y. Fourth: for every x, x plus zero equals x. Fifth: for all x and y, x plus the successor of y equals the successor of the sum x plus y. Sixth: for every x, x times zero equals zero. Seventh: for all x and y, x times the successor of y equals x times y, plus x. Eighth: for all x and y, x is less than y if and only if there exists z such that the successor of z plus x equals y. Plus all sentences of the following form: if A of zero and, for every x, A of x implies A of the successor of x, then for every x, A of x. End of arithmetic axioms and induction schema.

Means: Eight arithmetic axioms. First: for every x, the successor of x is not zero. Second: for all x and y, if the successor of x equals the successor of y then x equals y. Third: for every x, x equals zero or there exists y such that x equals the successor of y. Fourth: for every x, x plus zero equals x. Fifth: for all x and y, x plus the successor of y equals the successor of the sum x plus y. Sixth: for every x, x times zero equals zero. Seventh: for all x and y, x times the successor of y equals x times y, plus x. Eighth: for all x and y, x is less than y if and only if there exists z such that the successor of z plus x equals y. Plus all sentences of the following form: if A of zero and, for every x, A of x implies A of the successor of x, then for every x, A of x. End of arithmetic axioms and induction schema.

1 occurrence in this chapter

Equation form expr-a25d9c9866c45520

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Read as: Gamma subscript zero of Gamma

Means: Gamma subscript zero of Gamma

3 occurrences in this chapter

Equation form expr-a318c24216defe20

++

Read as: addition

Means: addition

2 occurrences in this chapter

Equation form expr-a390ab6e4e79645c

′M(x)=ValM(n+1¯)∈N\Assign{\prime}{M}(x) = \Value{\num{n+1}}{M} \in N

Read as: the successor function of structure M applied to lower case x equals the value in M of the numeral for n plus one, and this value belongs to N

Means: the successor function of structure M applied to lower case x equals the value in M of the numeral for n plus one, and this value belongs to N

1 occurrence in this chapter

Equation form expr-a8c35e7f8ed53dd8

PA2†\Th{PA^{2\dagger}}

Read as: the theory P A superscript two dagger

Means: the theory P A superscript two dagger

3 occurrences in this chapter

Equation form expr-aa9e97f22b80913b

A+(x,y,z)≡∃u(u(0)=x∧∀wu(x′)=u(x)′∧u(y)=z)!A_+(x,y,z) \ident \lexists[u][(u(\Obj 0)=x \land \lforall[w][u(x')=u (x)'] \land u(y)=z)]

Read as: A subscript plus of lower case x, lower case y, and lower case z abbreviates: there exists a unary function u such that u of zero equals x; and for every lower case w, u of the successor of x equals the successor of u of x; and u of y equals z

Means: A subscript plus of lower case x, lower case y, and lower case z abbreviates: there exists a unary function u such that u of zero equals x; and for every lower case w, u of the successor of x equals the successor of u of x; and u of y equals z

1 occurrence in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma logically entails A

Means: Gamma logically entails A

4 occurrences in this chapter

Equation form expr-abee72e2b1910eab

A≥n≡∃x1…∃xn(x1≠x2∧x1≠x3∧…∧xn−1≠xn).!A^{\ge n} \ident \lexists[x_1][\dots\lexists[x_n][(\eq/[x_1][x_2] \land \eq/[x_1][x_3] \land \dots \land \eq/[x_{n-1}][x_n])]].

Read as: A superscript at least n abbreviates: there exist x subscript one through x subscript n such that x subscript one differs from x subscript two, x subscript one differs from x subscript three, and so on through all distinct pairs, ending with x subscript n minus one different from x subscript n

Means: A superscript at least n abbreviates: there exist x subscript one through x subscript n such that x subscript one differs from x subscript two, x subscript one differs from x subscript three, and so on through all distinct pairs, ending with x subscript n minus one different from x subscript n

1 occurrence in this chapter

Equation form expr-ad70ad93d8384ee0

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

Read as: structure M under assignment s satisfies: for every lower case x, capital X holds of x

Means: structure M under assignment s satisfies: for every lower case x, capital X holds of x

1 occurrence in this chapter

Equation form expr-aeec131990b9d2b3

Y⊆ℕY \subseteq \Nat

Read as: capital Y contained in the natural numbers

Means: capital Y contained in the natural numbers

1 occurrence in this chapter

Equation form expr-b50bb8940da5b931

L\Lang{L}

Read as: the language L

Means: the language L

1 occurrence in this chapter

Equation form expr-b5fc0005953b9c6a

∀X((X(0)∧∀x(X(x)→X(x′)))→∀xX(x)).\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)])].

Read as: for every unary relation capital X: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x

Means: for every unary relation capital X: if capital X holds of zero and, for every lower case x, capital X holding of x implies capital X holding of the successor of x, then capital X holds of every lower case x

1 occurrence in this chapter

Equation form expr-b9b81453ce6fa9c8

Γ={¬Inf,A≥1,A≥2,A≥3,…}.\Gamma = \{\lnot \fn{Inf}, !A^{\ge 1}, !A^{\ge 2}, !A^{\ge 3}, \dots\}.

Read as: Gamma is the set containing not Inf, A superscript at least one, A superscript at least two, A superscript at least three, and so on

Means: Gamma is the set containing not Inf, A superscript at least one, A superscript at least two, A superscript at least three, and so on

1 occurrence in this chapter

Equation form expr-bc02950301011977

x∈s(X)=Nx \in s(X) = N

Read as: lower case x belongs to s of capital X, which equals N

Means: lower case x belongs to s of capital X, which equals N

1 occurrence in this chapter

Equation form expr-bd8e57da8dec8b7c

¬Count\lnot\fn{Count}

Read as: not Count

Means: not Count

1 occurrence in this chapter

Equation form expr-be58d8ae65b26403

0\Obj{0}

Read as: the constant zero

Means: the constant zero

1 occurrence in this chapter

Equation form expr-cbbba670a3f47b53

Γ⊢A\Gamma \Proves !A

Read as: A is derivable from Gamma

Means: A is derivable from Gamma

2 occurrences in this chapter

Equation form expr-ccd796da9a34d7d7

s(X)=Ns(X) = N

Read as: s assigns the set N to capital X

Means: s assigns the set N to capital X

1 occurrence in this chapter

Equation form expr-d36bf9bda45df250

⊨P→A\Entails !P \lif !A

Read as: the conditional if P then A is logically valid

Means: the conditional if P then A is logically valid

1 occurrence in this chapter

Equation form expr-d89ad7af62404a57

PA\Th{PA}

Read as: the theory P A

Means: the theory P A

1 occurrence in this chapter

Equation form expr-dabd3aff769f07eb

<<

Read as: the less than relation

Means: the less than relation

1 occurrence in this chapter

Equation form expr-dba793bd4a4137ec

M⊭A≥k+1\Sat/{M}{!A^{\ge k+1}}

Read as: structure M does not satisfy A superscript at least k plus one

Means: structure M does not satisfy A superscript at least k plus one

1 occurrence in this chapter

Equation form expr-de00ae955eee826e

B(n¯,Y)!B(\num n, Y)

Read as: B of the numeral for n and capital Y

Means: B of the numeral for n and capital Y

1 occurrence in this chapter

Equation form expr-df3e4a7b2aba0b5a

PA2\Th{PA^2}

Read as: the theory P A superscript two

Means: the theory P A superscript two

7 occurrences in this chapter

Equation form expr-e0dda27af4e64c02

M,s⊨X(0)∧∀x(X(x)→X(x′))\Sat{M}{X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]}[s]

Read as: structure M under assignment s satisfies both: capital X holds of zero, and for every lower case x, if capital X holds of x then it holds of the successor of x

Means: structure M under assignment s satisfies both: capital X holds of zero, and for every lower case x, if capital X holds of x then it holds of the successor of x

1 occurrence in this chapter

Equation form expr-e2aebbf920d8c881

u(0)=ku(0)=k

Read as: u of zero equals k

Means: u of zero equals k

1 occurrence in this chapter

Equation form expr-e318924191332bd4

n>kn>k

Read as: n is greater than k

Means: n is greater than k

1 occurrence in this chapter

Equation form expr-e3e00f3b268aa876

Γ0⊨A\Gamma_0 \Entails !A

Read as: Gamma subscript zero logically entails A

Means: Gamma subscript zero logically entails A

1 occurrence in this chapter

Equation form expr-e6eb9461cf697cf8

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

Read as: Count and Inf

Means: Count and Inf

1 occurrence in this chapter

Equation form expr-e6f495cadbcdbe35

A≥n!A^{\ge n}

Read as: A superscript at least n

Means: A superscript at least n

1 occurrence in this chapter

Equation form expr-e71c23f3006cc346

′M(x)∈N\Assign{\prime}{M}(x) \in N

Read as: the successor function of structure M applied to lower case x has its value in N

Means: the successor function of structure M applied to lower case x has its value in N

1 occurrence in this chapter

Equation form expr-e9a7a8390e22001b

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

Read as: the domain of structure M is included in N

Means: the domain of structure M is included in N

1 occurrence in this chapter

Equation form expr-ec7d40a789aa2d83

u′u'

Read as: the function variable u prime

Means: the function variable u prime

1 occurrence in this chapter

Equation form expr-efbc656af2a75a16

n≤mn \le m

Read as: n is less than or equal to m

Means: n is less than or equal to m

1 occurrence in this chapter

Equation form expr-f2354955dc96cccd

M⊨Γ0\Sat{M}{\Gamma_0}

Read as: structure M satisfies every sentence in Gamma subscript zero

Means: structure M satisfies every sentence in Gamma subscript zero

1 occurrence in this chapter

Arithmetic axioms and first order induction schema

The aligned display contains eight separately quantified arithmetic axioms, followed by the family of induction instances. They concern nonzero and injective successor, predecessors, recursion for addition and multiplication, and the less than relation. The final schema uses a formula A, not a quantified relation variable. Every row is read in full in the formula speech.

Source

Every element of a second order arithmetic model is named by a numeral

For a model of P A superscript two, form N from the values of all standard numerals. The proof shows N lies inside the domain and is closed under successor. Full second order induction applies to this actual subset, forcing it to contain the whole domain. No nonstandard domain elements remain.

Source

Instantiating the second order induction axiom

The first row states satisfaction of the universally quantified induction axiom. The second row, introduced by thus, states satisfaction of its instance under assignment s. This is an implication from a universal relation quantifier to a particular assignment, not an equation between rows.

Source

Categoricity of second order Peano arithmetic

Any two models of P A superscript two are isomorphic. The source combines the preceding theorem that numerals exhaust the domain with the linked theorem about standard models of Q, identifying every such model with the standard natural number structure.

Source

Definability of arithmetic from successor and second order induction

The theory P A superscript two dagger contains only the first two successor axioms and second order induction. The proposition says that order, addition, and multiplication are definable. The source sketches order by successor-closed sets and addition by a successor-preserving function. The printed addition formula has a variable mismatch and the prose about closed sets has a caveat; both are disclosed. Multiplication is left to the following exercise.

Source

Exercise completing the definability proof

Complete the proof that the reduced second order arithmetic theory defines order, addition, and multiplication. The reference points to the preceding proposition. No missing multiplication definition or proof is supplied.

Source

Undecidability of second order logic

A first order sentence is valid under first order semantics exactly when it is valid when considered in second order logic. Therefore a decision procedure for second order validity would decide first order validity, contrary to the known undecidability result.

Source

No sound and complete effective second order proof system

The source reduces truth in the standard natural numbers to validity of a pure second order sentence. It conjoins the nine second order arithmetic axioms, replaces arithmetic symbols by object, function, and relation variables, and universally quantifies those variables. A sound complete effective proof system would enumerate arithmetic truth; representability would then define that truth set, contradicting Tarski's theorem. The source's omitted explicit quantification over structures in one displayed equivalence is disclosed.

Source

Failure of compactness for second order logic

Gamma contains the sentence asserting finiteness together with a sentence requiring at least n elements for every positive integer n. Each finite collection of requirements can be satisfied in a sufficiently large finite domain, whereas their union cannot. The proof's use of Gamma in place of its finite subset when choosing a bound is retained with a source caveat.

Source

Exercise on noncompact entailment

Give a set Gamma and sentence A such that Gamma entails A but no finite subset of Gamma entails A. The negative entailment condition is preserved explicitly. No example or solution is added.

Source

Failure of downward Loewenheim Skolem in second order logic

The negation of Count has models on nonenumerable domains such as the power set of the natural numbers or the real numbers, but it has no enumerable model. Thus a second order sentence can have infinite models without an enumerable model.

Source

Failure of upward Loewenheim Skolem in second order logic

Count and Inf together hold in the natural numbers but not in any nonenumerable domain. This gives a sentence with a denumerable model and no nonenumerable model.

Source

Cross-reference reference-000790

the theorem that second order arithmetic models contain only numeral values

Source occurrence

Cross-reference reference-000791

the proposition about standard models of Q

Source occurrence

Cross-reference reference-000792

the proposition defining arithmetic from successor and second order induction

Source occurrence

Source disclosures