Second-order logic

Second-order Logic and Set Theory

Equation form expr-018d386ab2d8f3f7

Aleph0(X)\fn{Aleph}_0(X)

Read as: Aleph zero of capital X

Means: Aleph zero of capital X

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: s

2 occurrences in this chapter

Equation form expr-0501841a6c4781eb

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

Read as: for every x, x belongs to capital X if and only if x belongs to capital Y

Means: for every x, x belongs to capital X if and only if x belongs to capital Y

1 occurrence in this chapter

Equation form expr-15369659ae90c985

Pow(Y,R,X)\fn{Pow}(Y, R, X)

Read as: Pow applied to capital Y, capital R, and capital X

Means: Pow applied to capital Y, capital R, and capital X

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

3 occurrences in this chapter

Equation form expr-18f5384d58bcb1bb

YY

Read as: capital Y

Means: capital Y

8 occurrences in this chapter

Equation form expr-1d6d1d21c16e6418

Z⊆XZ \subseteq X

Read as: capital Z contained in capital X

Means: capital Z contained in capital X

2 occurrences in this chapter

Equation form expr-1f529c8fd1261a9e

s(X)=s(Y)s(X) = s(Y)

Read as: the set assigned to capital X by s equals the set assigned to capital Y by s

Means: the set assigned to capital X by s equals the set assigned to capital Y by s

1 occurrence in this chapter

Equation form expr-25772b7a9d87171e

∃u(∀x(X(x)→Y(u(x)))∧∀x∀y(u(x)=u(y)→x=y))\lexists[u][(\lforall[x][(X(x) \lif Y(u(x)))] \land \lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]])]

Read as: there exists a unary function u on the domain such that both of the following hold. First, for every x, if x belongs to capital X, then u of x belongs to capital Y. Second, for all x and y in the domain, if u of x equals u of y, then x equals y

Means: there exists a unary function u on the domain such that both of the following hold. First, for every x, if x belongs to capital X, then u of x belongs to capital Y. Second, for all x and y in the domain, if u of x equals u of y, then x equals y

1 occurrence in this chapter

Equation form expr-276193f4d3a4e963

X=YX = Y

Read as: capital X equals capital Y

Means: capital X equals capital Y

1 occurrence in this chapter

Equation form expr-284372a80e387f86

M,s⊨∃xX(x)\Sat{M}{\lexists[x][X(x)]}[s]

Read as: M under assignment s satisfies the formula: there exists x belonging to capital X

Means: M under assignment s satisfies the formula: there exists x belonging to capital X

1 occurrence in this chapter

Equation form expr-2933679b5a3991fd

NCH≡∀X(Cont(X)→∃Y(Y⊆X∧¬Count(Y)∧¬X≈Y))\fn{NCH} \ident \lforall[X][(\fn{Cont}(X) \lif \lexists[Y][(Y \subseteq X \land \lnot \fn{Count}(Y) \land \lnot \cardeq{X}{Y})])]

Read as: N C H abbreviates: for every subset capital X of the domain, if Cont holds of capital X, then there exists a subset capital Y of the domain such that capital Y is a subset of capital X, Count does not hold of capital Y, and capital X and capital Y are not equinumerous

Means: N C H abbreviates: for every subset capital X of the domain, if Cont holds of capital X, then there exists a subset capital Y of the domain such that capital Y is a subset of capital X, Count does not hold of capital Y, and capital X and capital Y are not equinumerous

1 occurrence in this chapter

Equation form expr-2a4c17ad662640b2

Aleph1(X)≡∀Y(Y⊆X→(¬Inf(Y)∨Aleph0(Y)))∧¬Aleph0(X)\fn{Aleph_1}(X) \ident \lforall[Y][(Y \subseteq X \lif (\lnot\fn{Inf}(Y) \lor \fn{Aleph}_0(Y)))] \land \lnot \fn{Aleph}_0(X)

Read as: Aleph one of capital X abbreviates the conjunction of two conditions. For every subset capital Y of the domain, if capital Y is a subset of capital X, then either not Inf of capital Y or Aleph zero of capital Y. And not Aleph zero of capital X

Means: Aleph one of capital X abbreviates the conjunction of two conditions. For every subset capital Y of the domain, if capital Y is a subset of capital X, then either not Inf of capital Y or Aleph zero of capital Y. And not Aleph zero of capital X

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: x

4 occurrences in this chapter

Equation form expr-30b2ec76b34c30fe

X≼Y\cardle{X}{Y}

Read as: capital X has cardinality at most that of capital Y

Means: capital X has cardinality at most that of capital Y

3 occurrences in this chapter

Equation form expr-33a9c96304bcc292

|M|\Domain{M}

Read as: the domain of M

Means: the domain of M

3 occurrences in this chapter

Equation form expr-3ac75a1a46cfcd10

Cont(Y)≡∃X∃R((Aleph0(X)∧Pow(Y,R,X))∧∀x∀y((Y(x)∧Y(y)∧∀zR(x,z)↔R(y,z))→x=y))\fn{Cont}(Y) \ident \lexists[X][\lexists[R][((\fn{Aleph}_0(X) \land \fn{Pow}(Y, R, X)) \land \\ \lforall[x][\lforall[y][((Y(x) \land {} Y(y) \land \lforall[z][R(x,z) \liff R(y,z)]) \lif \eq[x][y])]])]]

Read as: Cont of capital Y abbreviates: there exist a subset capital X of the domain and a binary relation capital R on the domain such that all three conditions hold. Aleph zero holds of capital X. Pow holds of capital Y, capital R, and capital X. And for all x and y, if x and y both belong to capital Y and, for every z, capital R relates x to z if and only if capital R relates y to z, then x equals y

Means: Cont of capital Y abbreviates: there exist a subset capital X of the domain and a binary relation capital R on the domain such that all three conditions hold. Aleph zero holds of capital X. Pow holds of capital Y, capital R, and capital X. And for all x and y, if x and y both belong to capital Y and, for every z, capital R relates x to z if and only if capital R relates y to z, then x equals y

1 occurrence in this chapter

Equation form expr-3bba9e996d9ab30b

s(X)⊆s(Y)s(X) \subseteq s(Y)

Read as: the set assigned to capital X by s is a subset of the set assigned to capital Y by s

Means: the set assigned to capital X by s is a subset of the set assigned to capital Y by s

1 occurrence in this chapter

Equation form expr-3bd52a5f8fc05fb1

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

Read as: x in the domain of M

Means: x in the domain of M

1 occurrence in this chapter

Equation form expr-3d0daddcb50d89f6

{y∈|M|:R(x,y)}\Setabs{y \in \Domain{M}}{R(x,y)}

Read as: the set of elements y of the domain of M such that capital R relates x to y

Means: the set of elements y of the domain of M such that capital R relates x to y

1 occurrence in this chapter

Equation form expr-407b3d81358c18b5

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

Read as: capital X of the domain of M

Means: capital X of the domain of M

1 occurrence in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: M

Means: M

1 occurrence in this chapter

Equation form expr-4565921d7f25c186

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

Read as: capital Y of the domain of M

Means: capital Y of the domain of M

2 occurrences in this chapter

Equation form expr-4812541c0868f169

∀X∀Y∀R(Pow(Y,R,X)→¬∃u(∀x∀y(u(x)=u(y)→x=y)∧∀x(Y(x)→X(u(x)))))\lforall[X][\lforall[Y][\lforall[R][(\fn{Pow}(Y, R, X) \lif \\ \lnot \lexists[u][(\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land {}\\ \lforall[x][(Y(x) \lif X(u(x)))])])]]]

Read as: for all subsets capital X and capital Y of the domain and all binary relations capital R on the domain: if Pow holds of capital Y, capital R, and capital X, then there does not exist a unary function u on the domain satisfying both conditions. First, for all x and y in the domain, if u of x equals u of y, then x equals y. Second, for every x, if x belongs to capital Y, then u of x belongs to capital X

Means: for all subsets capital X and capital Y of the domain and all binary relations capital R on the domain: if Pow holds of capital Y, capital R, and capital X, then there does not exist a unary function u on the domain satisfying both conditions. First, for all x and y in the domain, if u of x equals u of y, then x equals y. Second, for every x, if x belongs to capital Y, then u of x belongs to capital X

1 occurrence in this chapter

Equation form expr-483ae665a06166fb

P≼X\cardle{P}{X}

Read as: capital P has cardinality at most that of capital X

Means: capital P has cardinality at most that of capital X

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: capital X

Means: capital X

15 occurrences in this chapter

Equation form expr-4f948d1a4e9c9d91

ℵ2\aleph_2

Read as: aleph two

Means: aleph two

1 occurrence in this chapter

Equation form expr-50313993f6604d8b

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

Read as: for every x, if x belongs to capital X, then x belongs to capital Y

Means: for every x, if x belongs to capital X, then x belongs to capital Y

1 occurrence in this chapter

Equation form expr-53f0e0c999550424

CH≡∀X(Aleph1(X)↔Cont(X))\fn{CH} \ident \lforall[X][(\fn{Aleph}_1(X) \liff \fn{Cont}(X))]

Read as: C H abbreviates: for every subset capital X of the domain, Aleph one of capital X if and only if Cont of capital X

Means: C H abbreviates: for every subset capital X of the domain, Aleph one of capital X if and only if Cont of capital X

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: capital P

Means: capital P

5 occurrences in this chapter

Equation form expr-61054bdda4653e94

s(Y)≈ℝ\cardeq{s(Y)}{\Real}

Read as: the set assigned to capital Y by s and the real numbers are equinumerous

Means: the set assigned to capital Y by s and the real numbers are equinumerous

1 occurrence in this chapter

Equation form expr-6880858d39535e2d

∃z∃u(X(z)∧∀x(X(x)→X(u(x)))∧∀Y((Y(z)∧∀x(Y(x)→Y(u(x))))→X=Y))\lexists[z][\lexists[u][(X(z) \land \lforall[x][(X(x) \lif X(u(x)))] \land {} \\ \lforall[Y][((Y(z) \land \lforall[x][(Y(x) \lif Y(u(x)))]) \lif X = Y)])]]

Read as: there exist an element z and a unary function u on the domain such that all three conditions hold. First, z belongs to capital X. Second, for every x, if x belongs to capital X, then u of x belongs to capital X. Third, for every subset capital Y of the domain, if z belongs to capital Y and, for every x, membership of x in capital Y implies membership of u of x in capital Y, then capital X equals capital Y

Means: there exist an element z and a unary function u on the domain such that all three conditions hold. First, z belongs to capital X. Second, for every x, if x belongs to capital X, then u of x belongs to capital X. Third, for every subset capital Y of the domain, if z belongs to capital Y and, for every x, membership of x in capital Y implies membership of u of x in capital Y, then capital X equals capital Y

1 occurrence in this chapter

Equation form expr-69f41eb504b570b7

Count(X)≡\fn{Count}(X) \ident

Read as: Count of capital X abbreviates

Means: Count of capital X abbreviates

1 occurrence in this chapter

Equation form expr-6e82ac27792a9ac6

ℝ\Real

Read as: the real numbers

Means: the real numbers

3 occurrences in this chapter

Equation form expr-71440bd4be4b042d

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

Read as: M under assignment s satisfies the formula: for every x, if x belongs to capital X, then x belongs to capital Y

Means: M under assignment s satisfies the formula: for every x, if x belongs to capital X, then x belongs to capital Y

1 occurrence in this chapter

Equation form expr-809b9d11acfce1de

Y≼X\cardle{Y}{X}

Read as: capital Y has cardinality at most that of capital X

Means: capital Y has cardinality at most that of capital X

1 occurrence in this chapter

Equation form expr-8211d6f5a6559603

∀X∀Y((X≼Y∧Y≼X)→X≈Y)\lforall[X][\lforall[Y][((\cardle{X}{Y} \land \cardle{Y}{X}) \lif \cardeq{X}{Y})]]

Read as: for all subsets capital X and capital Y of the domain, if capital X has cardinality at most that of capital Y and capital Y has cardinality at most that of capital X, then capital X and capital Y are equinumerous

Means: for all subsets capital X and capital Y of the domain, if capital X has cardinality at most that of capital Y and capital Y has cardinality at most that of capital X, then capital X and capital Y are equinumerous

1 occurrence in this chapter

Equation form expr-84c0da03d30444e6

Y∈ZY \in Z

Read as: capital Y in capital Z

Means: capital Y in capital Z

1 occurrence in this chapter

Equation form expr-8608ea2a7d88b8c8

¬CH\lnot \fn{CH}

Read as: not C H

Means: not C H

1 occurrence in this chapter

Equation form expr-8b19ee8f92e456bf

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

Read as: capital R, a subset of the Cartesian square of the domain of M,

Means: capital R, a subset of the Cartesian square of the domain of M,

2 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: capital R

Means: capital R

9 occurrences in this chapter

Equation form expr-8cafa9e3d0a185fe

ℵ0\aleph_0

Read as: aleph zero

Means: aleph zero

7 occurrences in this chapter

Equation form expr-90a868ad60abd86d

ℝ≼|M|\cardle{\Real}{\Domain{M}}

Read as: the real numbers have cardinality at most that of the domain of M

Means: the real numbers have cardinality at most that of the domain of M

1 occurrence in this chapter

Equation form expr-911f79779f2b99f1

Z⊆℘(|M|)Z \subseteq \Pow{\Domain{M}}

Read as: capital Z, a subset of the power set of the domain of M,

Means: capital Z, a subset of the power set of the domain of M,

1 occurrence in this chapter

Equation form expr-92608bc8c558991d

Codes(x,R,Z)≡∀y(Z(y)↔R(x,y))\fn{Codes}(x, R, Z) \ident \lforall[y][(Z(y) \liff R(x, y))]

Read as: Codes applied to x, capital R, and capital Z abbreviates: for every y, y belongs to capital Z if and only if capital R relates x to y

Means: Codes applied to x, capital R, and capital Z abbreviates: for every y, y belongs to capital Z if and only if capital R relates x to y

1 occurrence in this chapter

Equation form expr-9b7316c8483dfaf3

∃xX(x)\lexists[x][X(x)]

Read as: there exists x belonging to capital X

Means: there exists x belonging to capital X

1 occurrence in this chapter

Equation form expr-9cf3f61306fb2ac6

℘(X)\Pow{X}

Read as: the power set of capital X

Means: the power set of capital X

2 occurrences in this chapter

Equation form expr-a66c4da13d46d4b4

∀Y(P(Y)↔Y⊆X)\lforall[Y][(P(Y) \liff Y \subseteq X)]

Read as: for every capital Y, capital P applied to capital Y if and only if capital Y is a subset of capital X

Means: for every capital Y, capital P applied to capital Y if and only if capital Y is a subset of capital X

1 occurrence in this chapter

Equation form expr-a854c3843117862a

Aleph0(X)↔Inf(X)∧Count(X)\fn{Aleph}_0(X) \liff \fn{Inf}(X) \land \fn{Count}(X)

Read as: Aleph zero of capital X if and only if both Inf of capital X and Count of capital X

Means: Aleph zero of capital X if and only if both Inf of capital X and Count of capital X

1 occurrence in this chapter

Equation form expr-aa7ea6bef90554fa

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

Read as: M under assignment s satisfies the formula: for every x, x belongs to capital X if and only if x belongs to capital Y

Means: M under assignment s satisfies the formula: for every x, x belongs to capital X if and only if x belongs to capital Y

1 occurrence in this chapter

Equation form expr-aae90dfb1ac24e1a

s(Y)s(Y)

Read as: the set assigned to capital Y by s

Means: the set assigned to capital Y by s

6 occurrences in this chapter

Equation form expr-acad017ad5996bbe

M⊨∃X∃Y∃R(Aleph0(X)∧Pow(Y,R,X)∧∃u(∀x∀y(u(x)=u(y)→x=y)∧∀y(Y(y)→∃xy=u(x)))).\Sat{M}{\lexists[X][\lexists[Y][\lexists[R][(\fn{Aleph}_0(X) \land \fn{Pow}(Y, R, X) \land \\ \lexists[u][(\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land {} \\\lforall[y][(Y(y) \lif \lexists[x][\eq[y][u(x)]])])])]]]}.

Read as: M satisfies the following sentence. There exist subsets capital X and capital Y of the domain and a binary relation capital R on the domain such that Aleph zero holds of capital X, Pow holds of capital Y, capital R, and capital X, and there exists a unary function u on the domain satisfying both conditions. For all x and y in the domain, if u of x equals u of y, then x equals y. And for every y, if y belongs to capital Y, then there exists x such that y equals u of x

Means: M satisfies the following sentence. There exist subsets capital X and capital Y of the domain and a binary relation capital R on the domain such that Aleph zero holds of capital X, Pow holds of capital Y, capital R, and capital X, and there exists a unary function u on the domain satisfying both conditions. For all x and y in the domain, if u of x equals u of y, then x equals y. And for every y, if y belongs to capital Y, then there exists x such that y equals u of x

1 occurrence in this chapter

Equation form expr-b15cca1bfa606d89

|M|≈ℝ\cardeq{\Domain{M}}{\Real}

Read as: the domain of M and the real numbers are equinumerous

Means: the domain of M and the real numbers are equinumerous

1 occurrence in this chapter

Equation form expr-b20569e7ce237efb

s(X)≠∅s(X) \neq \emptyset

Read as: the set assigned to capital X by s is not empty

Means: the set assigned to capital X by s is not empty

1 occurrence in this chapter

Equation form expr-b3516dd26a364c2b

f:X→Yf\colon X \to Y

Read as: f from capital X to capital Y

Means: f from capital X to capital Y

2 occurrences in this chapter

Equation form expr-b4dd71ab2d35e450

X≈Y\cardeq{X}{Y}

Read as: capital X and capital Y are equinumerous

Means: capital X and capital Y are equinumerous

3 occurrences in this chapter

Equation form expr-b61dce792ab0b770

Inf(X)≡\fn{Inf}(X) \ident

Read as: Inf of capital X abbreviates

Means: Inf of capital X abbreviates

1 occurrence in this chapter

Equation form expr-b68413abaccaf397

∃u(∀x∀y(u(x)=u(y)→x=y)∧∃y(X(y)∧∀x(X(x)→y≠u(x)))\lexists[u][(\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land {} \\\lexists[y][(X(y) \land \lforall[x][(X(x) \lif \eq/[y][u(x)])]])]

Read as: there exists a unary function u on the domain such that both of the following hold. First, for all x and y in the domain, if u of x equals u of y, then x equals y. Second, there exists y belonging to capital X such that, for every x, if x belongs to capital X, then y is not equal to u of x

Means: there exists a unary function u on the domain such that both of the following hold. First, for all x and y in the domain, if u of x equals u of y, then x equals y. Second, there exists y belonging to capital X such that, for every x, if x belongs to capital X, then y is not equal to u of x

1 occurrence in this chapter

Equation form expr-baedede7771d86e6

X⊆YX \subseteq Y

Read as: capital X is a subset of capital Y

Means: capital X is a subset of capital Y

1 occurrence in this chapter

Equation form expr-bbeebd879e1dff69

ZZ

Read as: capital Z

Means: capital Z

2 occurrences in this chapter

Equation form expr-bd46bac95472c172

CH\fn{CH}

Read as: C H

Means: C H

1 occurrence in this chapter

Equation form expr-c1ead49718892dcc

s(R)s(R)

Read as: the relation assigned to capital R by s

Means: the relation assigned to capital R by s

5 occurrences in this chapter

Equation form expr-c70fd563ab6ac56d

s(x)s(x)

Read as: the element assigned to x by s

Means: the element assigned to x by s

1 occurrence in this chapter

Equation form expr-ca6c5f671cdc3f3a

s(X)s(X)

Read as: the set assigned to capital X by s

Means: the set assigned to capital X by s

5 occurrences in this chapter

Equation form expr-d73049bc18fd94bc

{y∈|M|:R(x,y)}\Setabs{y \in \Domain{M}}{R(x, y)}

Read as: the set of elements y of the domain of M such that capital R relates x to y

Means: the set of elements y of the domain of M such that capital R relates x to y

1 occurrence in this chapter

Equation form expr-da407436acdca71d

ℵ1\aleph_1

Read as: aleph one

Means: aleph one

4 occurrences in this chapter

Equation form expr-e48934d91c2df56f

X≠∅X \neq \emptyset

Read as: capital X is not empty

Means: capital X is not empty

1 occurrence in this chapter

Equation form expr-e7181254da2ec7ac

∃u(∀x(X(x)→Y(u(x)))∧∀x∀y(u(x)=u(y)→x=y)∧∀y(Y(y)→∃x(X(x)∧y=u(x))))\lexists[u][(\lforall[x][(X(x) \lif Y(u(x)))] \land {}\\ \lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land {} \\\lforall[y][(Y(y) \lif \lexists[x][(X(x) \land \eq[y][u(x)])])])]

Read as: there exists a unary function u on the domain such that all three conditions hold. First, for every x, if x belongs to capital X, then u of x belongs to capital Y. Second, for all x and y in the domain, if u of x equals u of y, then x equals y. Third, for every y, if y belongs to capital Y, then there exists x belonging to capital X such that y equals u of x

Means: there exists a unary function u on the domain such that all three conditions hold. First, for every x, if x belongs to capital X, then u of x belongs to capital Y. Second, for all x and y in the domain, if u of x equals u of y, then x equals y. Third, for every y, if y belongs to capital Y, then there exists x belonging to capital X such that y equals u of x

1 occurrence in this chapter

Equation form expr-ea81fe522f819d56

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

Read as: capital Z contained in the domain of M

Means: capital Z contained in the domain of M

1 occurrence in this chapter

Equation form expr-f56a918ca6e74df7

x∈Yx \in Y

Read as: x in capital Y

Means: x in capital Y

2 occurrences in this chapter

Equation form expr-f8d2d8e58812a24b

s(Z)s(Z)

Read as: the set assigned to capital Z by s

Means: the set assigned to capital Z by s

2 occurrences in this chapter

Equation form expr-f90b26b04c19ec9c

P(Y)P(Y)

Read as: capital P applied to capital Y

Means: capital P applied to capital Y

1 occurrence in this chapter

Equation form expr-f933d1b137a7ff7b

Pow(Y,R,X)≡∀Z(Z⊆X→∃x(Y(x)∧Codes(x,R,Z)))∧∀x(Y(x)→∀Z(Codes(x,R,Z)→Z⊆X))\fn{Pow}(Y, R, X) \ident \\ \lforall[Z][(Z \subseteq X \lif \lexists[x][(Y(x) \land \fn{Codes}(x, R, Z))])] \land {} \\ \lforall[x][(Y(x) \lif \lforall[Z][(\fn{Codes}(x, R, Z) \lif Z \subseteq X)])]

Read as: Pow applied to capital Y, capital R, and capital X abbreviates two conditions. First, for every subset capital Z of the domain, if capital Z is a subset of capital X, then there exists x belonging to capital Y such that Codes holds of x, capital R, and capital Z. Second, for every x, if x belongs to capital Y, then for every subset capital Z of the domain, if Codes holds of x, capital R, and capital Z, then capital Z is a subset of capital X

Means: Pow applied to capital Y, capital R, and capital X abbreviates two conditions. First, for every subset capital Z of the domain, if capital Z is a subset of capital X, then there exists x belonging to capital Y such that Codes holds of x, capital R, and capital Z. Second, for every x, if x belongs to capital Y, then for every subset capital Z of the domain, if Codes holds of x, capital R, and capital Z, then capital Z is a subset of capital X

1 occurrence in this chapter

Second-order definition of the subset relation

For every domain element x, membership in capital X implies membership in capital Y. Under an assignment s, the formula is satisfied exactly when the set assigned to capital X is a subset of the set assigned to capital Y. This compares subsets through unary relation variables, without adding a set membership predicate to the language.

Source

Second-order definition of equality of sets

The two unary relation variables agree on every domain element. Under assignment s this says that their assigned subsets have exactly the same members and hence are equal.

Source

Second-order definition of nonemptiness

There exists a domain element satisfying capital X. The assigned subset is therefore not empty.

Source

Proposed cardinal comparison by an injective function

The displayed second-order formula quantifies over a unary function on the whole domain. It sends every member of capital X into capital Y and is injective on all domain elements. The scope of the injectivity condition is preserved explicitly, rather than silently restricted to capital X.

Source

Source formula proposed to define equinumerosity

The function sends capital X into capital Y, is injective on the whole domain, and maps capital X onto capital Y. A source caveat explains why requiring a globally injective extension is stronger than a bijection between arbitrary subsets. The formula and the source claim are both retained.

Source

Three conjuncts of the source equinumerosity formula

Read the three conditions in order: image of capital X lies in capital Y; equality of function values implies equality of arguments throughout the domain; every element of capital Y is the image of an element of capital X. The third conjunct does not cancel or restrict the domain-wide quantifiers in the second.

Source

Second-order sentence intended to express Schroeder Bernstein

For any two subsets, cardinal comparison in each direction is asserted to imply equinumerosity. The source proof appeals to the Schroeder Bernstein theorem for ordinary sets. Its use of the source's formal equinumerosity abbreviation remains subject to the preceding caveat about global injectivity.

Source

Source formula proposed to characterize infinite subsets

Inf of capital X asks for an injective unary function on the domain and an element of capital X absent from the image of capital X. The source does not require the function to map capital X into itself. The caveat records that even a singleton in a two element domain can satisfy this printed condition.

Source

Injectivity and omitted-image conditions in Inf

The first conjunct quantifies over all domain elements and expresses injectivity. The second selects an element y in capital X and states that no x in capital X maps to y. No closure conjunct is added in either MathML or the spoken formula.

Source

Source formula proposed to characterize enumerable subsets

Count of capital X asks for an initial member z, closure under a unary function, and equality with every subset containing z and closed under that function. Only delimiter nesting is repaired. The mathematical caveat explains that equality with the whole domain is forced and that the empty set is excluded.

Source

Initial element, closure, and equality conditions in Count

The existential z and function u bind all three conjuncts. In the final conjunct, every unary relation variable capital Y is considered, not merely subsets of capital X. Its conclusion is equality with capital X, exactly as printed, rather than inclusion.

Source

Coding a subset by an element and a binary relation

An element x codes, using capital R, the subset consisting of all domain elements y related to x by capital R. The order of arguments matters: x is the code, and y ranges over members of the coded subset.

Source

Formulas for coding one subset and a power set

Codes of x, capital R, and capital Z says that capital Z contains exactly the elements related to x by capital R. Pow of capital Y, capital R, and capital X says that every subset of capital X has a code in capital Y and that every code in capital Y represents a subset of capital X. Multiple elements of capital Y may code the same subset.

Source

Both directions of the power set coding condition

Every subset capital Z of capital X is coded by some element x of capital Y. Conversely, if x belongs to capital Y, every subset that x codes with capital R is a subset of capital X. The missing outer closing parenthesis is disclosed and balanced without changing these conditions.

Source

Cantor theorem expressed through codes for subsets

The source asserts validity of a sentence saying that, if capital Y codes the power set of capital X using capital R, no injective domain function can send all of capital Y into capital X. Quantification ranges over two subsets, a binary relation, and then the proposed unary function. The source supplies no proof here, and none is added.

Source

Negated existence of an injection on a power set coding domain

For every capital X, capital Y, and capital R satisfying Pow, negate the existence of a function with both global injectivity and image of capital Y contained in capital X. The negation applies to the entire existential conjunction, not just one of its conditions.

Source

Source formula proposed to characterize continuum-sized subsets

Assuming the domain is at least continuum-sized, Cont of capital Y asks for a set capital X satisfying Aleph zero and a relation coding its power set with capital Y. The final conjunct requires distinct elements of capital Y to code distinct subsets. The source proof describes this injectivity argument, with its variable mismatch and earlier definitional dependencies disclosed.

Source

Power set coding with unique codes in Cont

The first conditions are Aleph zero of capital X and Pow of capital Y, capital R, and capital X. The last condition says that any two elements x and y of capital Y having the same capital R successors are equal. Equality of coded subsets is tested by equivalence for every z in the domain.

Source

Source equivalence proposed for a continuum-sized domain

The source equates domain size with the continuum using the existence of a countable base, a power set coding set, and an injective domain function whose range contains that coding set. The last condition is satisfied by the identity and does not provide the claimed upper bound. The formula and claim are preserved with a caveat, not silently replaced.

Source

Satisfaction statement using a power set code and a function range

M satisfies an existential statement about capital X, capital Y, capital R, and u. The function is injective on the domain, and every member of capital Y has a preimage. The source does not require every image of u to belong to capital Y; the two directions must not be reversed in speech.

Source

Source sentence intended to express the Continuum Hypothesis

C H universally equates the Aleph one and Cont conditions on subsets of the domain. The source states that its validity is equivalent to the Continuum Hypothesis. This remains a source assertion with the earlier definitional defects disclosed. No missing proof or replacement definition is supplied.

Source

Source sentence intended to express failure of the Continuum Hypothesis

N C H says that every subset satisfying Cont has a subset that fails Count and is not equinumerous with it. The source asserts that validity of this sentence is equivalent to failure of the Continuum Hypothesis. The same earlier definitional caveats apply, and the absence of a source proof is preserved.

Source

Source disclosures