Second-order Logic and Set Theory

Reading preferences

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

Editorial

This section deals with coding powersets and the continuum in second-order logic. The results are stated but proofs have yet to be filled in. There are no problems yet---and the definitions and results themselves may have problems. Use with caution and report anything that's false or unclear.

Introduction

Since second-order logic can quantify over subsets of the domain as well as functions, it is to be expected that some amount, at least, of set theory can be carried out in second-order logic. By “carry out,” we mean that it is possible to express set theoretic properties and statements in second-order logic, and is possible without any special, non-logical vocabulary for sets (e.g., the membership predicate symbol of set theory). For instance, we can define unions and intersections of sets and the subset relationship, but also compare the sizes of sets, and state results such as Cantor's Theorem.

Comparing Sets

Second-order definition of the subset relation

The formula $\lforall[x][(X(x) \lif Y(x))]$ source defines the subset relation, i.e., $\Sat{M}{\lforall[x][(X(x) \lif Y(x))]}[s]$ source iff $s(X) \subseteq s(Y)$ source.

Second-order definition of equality of sets

The formula $\lforall[x][(X(x) \liff Y(x))]$ source defines the identity relation on sets, i.e., $\Sat{M}{\lforall[x][(X(x) \liff Y(x))]}[s]$ source iff $s(X) = s(Y)$ source.

Second-order definition of nonemptiness

The formula $\lexists[x][X(x)]$ source defines the property of being non-empty, i.e., $\Sat{M}{\lexists[x][X(x)]}[s]$ source iff $s(X) \neq \emptyset$ source.

A set $X$ source is no larger than a set $Y$ source, $\cardle{X}{Y}$ source, iff there is an injective function $f\colon X \to Y$ source. Since we can express that a function is injective, and also that its values for arguments in $X$ source are in $Y$ source, we can also define the relation of being no larger than on subsets of the domain.

Proposed cardinal comparison by an injective function

The formula

\lexists[u][(\lforall[x][(X(x) \lif Y(u(x)))] \land \lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]])]

source

defines the relation of being no larger than.

Two sets are the same size, or “equinumerous,” $\cardeq{X}{Y}$ source, iff there is a bijective function $f\colon X \to Y$ source.

Source formula proposed to define equinumerosity

The formula

\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)])])])]

source

defines the relation of being equinumerous with.

We will abbreviate these formulas, respectively, as $X \subseteq Y$ source, $X = Y$ source, $X \neq \emptyset$ source, $\cardle{X}{Y}$ source, and $\cardeq{X}{Y}$ source. (This may be slightly confusing, since we use the same notation when we speak informally about sets $X$ source and $Y$ source---but here the notation is an abbreviation for formulas in second-order logic involving one-place relation variables $X$ source and $Y$ source.)

Second-order sentence intended to express Schroeder Bernstein

The sentence $\lforall[X][\lforall[Y][((\cardle{X}{Y} \land \cardle{Y}{X}) \lif \cardeq{X}{Y})]]$ source is valid.

Proof

The sentence is satisfied in a structure $\Struct{M}$ source if, for any subsets $X \subseteq \Domain{M}$ source and $Y \subseteq \Domain{M}$ source, if $\cardle{X}{Y}$ source and $\cardle{Y}{X}$ source then $\cardeq{X}{Y}$ source. But this holds for any sets $X$ source and $Y$ source---it is the Schröder-Bernstein Theorem.

Cardinalities of Sets

Explain

Just as we can express that the domain is finite or infinite, enumerable or non-enumerable, we can define the property of a subset of $\Domain{M}$ source being finite or infinite, enumerable or non-enumerable.

Source formula proposed to characterize infinite subsets

The formula $\fn{Inf}(X) \ident$ source

\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)])]])]

source

is satisfied with respect to a variable assignment $s$ source iff $s(X)$ source is infinite.

Source formula proposed to characterize enumerable subsets

The formula $\fn{Count}(X) \ident$ source

\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)])]]

source

is satisfied with respect to a variable assignment $s$ source iff $s(X)$ source is enumerable.

We know from Cantor's Theorem that there are non-enumerable sets, and in fact, that there are infinitely many different levels of infinite sizes. Set theory develops an entire arithmetic of sizes of sets, and assigns infinite cardinal numbers to sets. The natural numbers serve as the cardinal numbers measuring the sizes of finite sets. The cardinality of denumerable sets is the first infinite cardinality, called $\aleph_0$ source (“aleph-nought” or “aleph-zero”). The next infinite size is $\aleph_1$ source. It is the smallest size a set can be without being countable (i.e., of size $\aleph_0$ source). We can define “ $X$ source has size $\aleph_0$ source” as $\fn{Aleph}_0(X) \liff \fn{Inf}(X) \land \fn{Count}(X)$ source. $X$ source has size $\aleph_1$ source iff all its subsets are finite or have size $\aleph_0$ source, but is not itself of size $\aleph_0$ source. Hence we can express this by the formula $\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)$ source. Being of size $\aleph_2$ source is defined similarly, etc.

There is one size of special interest, the so-called cardinality of the continuum. It is the size of $\Pow{\Nat}$ source, or, equivalently, the size of $\Real$ source. That a set is the size of the continuum can also be expressed in second-order logic, but requires a bit more work.

The Power of the Continuum

Explain

In second-order logic we can quantify over subsets of the domain, but not over sets of subsets of the domain. To do this directly, we would need third-order logic. For instance, if we wanted to state Cantor's Theorem that there is no injective function from the power set of a set to the set itself, we might try to formulate it as “for every set $X$ source, and every set $P$ source, if $P$ source is the power set of $X$ source, then not $\cardle{P}{X}$ source”. And to say that $P$ source is the power set of $X$ source would require formalizing that the elements of $P$ source are all and only the subsets of $X$ source, so something like $\lforall[Y][(P(Y) \liff Y \subseteq X)]$ source. The problem lies in $P(Y)$ source: that is not a formula of second-order logic, since only terms can be arguments to one-place relation variables like $P$ source.

We can, however, simulate quantification over sets of sets, if the domain is large enough. The idea is to make use of the fact that two-place relations $R$ source relate elements of the domain to elements of the domain. Given such an $R$ source, we can collect all the elements to which some $x$ source is $R$ source-related: $\Setabs{y \in \Domain{M}}{R(x,y)}$ source is the set “coded by” $x$ source. Conversely, if $Z \subseteq \Pow{\Domain{M}}$ source is some collection of subsets of $\Domain{M}$ source, and there are at least as many elements of $\Domain{M}$ source as there are sets in $Z$ source, then there is also a relation $R \subseteq \Domain{M}^2$ source such that every $Y \in Z$ source is coded by some $x$ source using $R$ source.

Coding a subset by an element and a binary relation

If $R \subseteq \Domain{M}^2$ source, then $x$ source $R$ source-codes $\Setabs{y \in \Domain{M}}{R(x, y)}$ source.

If an element $x \in \Domain{M}$ source $R$ source-codes a set $Z \subseteq \Domain{M}$ source, then a set $Y \subseteq \Domain{M}$ source codes a set of sets, namely the sets coded by the elements of $Y$ source. So a set $Y$ source can $R$ source-code $\Pow{X}$ source. It does so iff for every $Z \subseteq X$ source, some $x \in Y$ source $R$ source-codes $Z$ source, and every $x \in Y$ source $R$ source-codes a $Z \subseteq X$ source.

Formulas for coding one subset and a power set

The formula

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

source

expresses that $s(x)$ source $s(R)$ source-codes $s(Z)$ source. The formula

\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)])]

source

expresses that $s(Y)$ source $s(R)$ source-codes the power set of $s(X)$ source, i.e., the elements of $s(Y)$ source $s(R)$ source-code exactly the subsets of $s(X)$ source.

Explain

With this trick, we can express statements about the power set by quantifying over the codes of subsets rather than the subsets themselves. For instance, Cantor's Theorem can now be expressed by saying that there is no injective function from the domain of any relation that codes the power set of $X$ source to $X$ source itself.

Cantor theorem expressed through codes for subsets

The sentence

\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)))])])]]]

source

is valid.

Explain

The power set of a denumerable set is non-enumerable, and so its cardinality is larger than that of any denumerable set (which is $\aleph_0$ source). The size of $\Pow{\Nat}$ source is called the “power of the continuum,” since it is the same size as the points on the real number line, $\Real$ source. If the domain is large enough to code the power set of a denumerable set, we can express that a set is the size of the continuum by saying that it is equinumerous with any set $Y$ source that codes the power set of set $X$ source of size $\aleph_0$ source. (If the domain is not large enough, i.e., it contains no subset equinumerous with $\Real$ source, then there can also be no relation that codes $\Pow{X}$ source.)

Source formula proposed to characterize continuum-sized subsets

If $\cardle{\Real}{\Domain{M}}$ source, then the formula

\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])]])]]

source

expresses that $\cardeq{s(Y)}{\Real}$ source.

Proof

$\fn{Pow}(Y, R, X)$ source expresses that $s(Y)$ source $s(R)$ source-codes the power set of $s(X)$ source, which $\fn{Aleph}_0(X)$ source says is countable. So $s(Y)$ source is at least as large as the power of the continuum, although it may be larger (if multiple elements of $s(Y)$ source code the same subset of $X$ source). This is ruled out by the last conjunct, which requires the association between elements of $s(Y)$ source and subsets of $s(Z)$ source via $s(R)$ source to be injective.

Source equivalence proposed for a continuum-sized domain

$\cardeq{\Domain{M}}{\Real}$ source iff

\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)]])])])]]]}.

source

Explain

The Continuum Hypothesis is the statement that the size of the continuum is the first non-enumerable cardinality, i.e, that $\Pow{\Nat}$ source has size $\aleph_1$ source.

Source sentence intended to express the Continuum Hypothesis

The Continuum Hypothesis is true iff

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

source

is valid.

Note that it isn't true that $\lnot \fn{CH}$ source is valid iff the Continuum Hypothesis is false. In an enumerable domain, there are no subsets of size $\aleph_1$ source and also no subsets of the size of the continuum, so $\fn{CH}$ source is always true in an enumerable domain. However, we can give a different sentence that is valid iff the Continuum Hypothesis is false:

Source sentence intended to express failure of the Continuum Hypothesis

The Continuum Hypothesis is false iff

\fn{NCH} \ident \lforall[X][(\fn{Cont}(X) \lif \lexists[Y][(Y \subseteq X \land \lnot \fn{Count}(Y) \land \lnot \cardeq{X}{Y})])]

source

is valid.

Source disclosures

TR041-SAR-001: Source caveat. The displayed function is required to be injective on the entire domain, not just on capital X. Together with its surjectivity from capital X onto capital Y, this is stronger than a bijection between those subsets. For example, a proper countably infinite subset of a countably infinite domain is equinumerous with the domain, but a bijection from that proper subset onto the whole domain cannot extend to an injective function on the whole domain. The displayed formula and claim are preserved, not corrected. source
TR041-SAR-002: Source caveat. The formula called Inf does not require u to map capital X into capital X. As printed, a singleton in a two element domain can satisfy it: take u to swap the two elements. Thus the displayed condition does not characterize infinitude as claimed. The source formula is preserved. source
TR041-SAR-004: Source caveat. The formula called Count quantifies over every subset capital Y of the domain, then requires equality with capital X whenever capital Y contains z and is closed under u. Taking capital Y to be the whole domain forces capital X to be the whole domain. The formula also requires an element z of capital X and so excludes the empty set. It therefore does not characterize all enumerable subsets as claimed. These mathematical conditions are preserved, not rewritten. source
TR041-SAR-003: Reader correction. The closing parentheses in the Count display have been balanced around the universally quantified implication and the outer conjunction. No quantifier, connective, or variable has been changed. The exact original remains in Source view. source
TR041-SAR-005: Source caveat. The proposed Aleph one condition includes capital X among its own subsets. Even if Inf and Aleph zero had their intended meanings, the displayed condition would exclude a set of size aleph one, while allowing finite sets. The definition is preserved as a source defect, not replaced with a new set theoretic characterization. Later claims using this abbreviation inherit the caveat. source
TR041-SAR-006: two-place relations capital R relate elements of the domain to source
TR041-SAR-007: Reader correction. A missing closing parenthesis has been supplied in the final conjunct of the Pow display. The nested implication remains: if x belongs to capital Y, then every subset coded by x using capital R is a subset of capital X. No mathematical condition has been changed. source
TR041-SAR-009: Source caveat. The proof refers to subsets of the set assigned to capital Z, although the displayed construction uses capital X as the set whose subsets are coded and has no such free capital Z. This apparent variable mismatch is retained in the source wording and identified here, without an unmarked substitution. source
TR041-SAR-008: This is ruled out by the last conjunct, which requires the source
TR041-SAR-010: Source caveat. The final function condition in this proposed characterization is satisfied by the identity function on the whole domain, for any subset capital Y. It therefore does not establish the upper bound on domain size needed for equality with the continuum. The formula also inherits the earlier caveats about Aleph zero. The source statement is preserved, not presented as an independently established equivalence. source
TR041-SAR-011: Source caveat. The following assertions about C H and N C H use the earlier abbreviations Aleph one, Aleph zero, Count, and equinumerosity. Those printed definitions have the documented defects. The source's intended connection with the Continuum Hypothesis is retained, but the printed formulas are not certified as correct characterizations. No missing proof is supplied. source

Reading preferences

Source file content/second-order-logic/sol-and-set-theory/sol-and-set-theory.tex

Editorial

Source file content/second-order-logic/sol-and-set-theory/introduction.tex

Introduction

Source file content/second-order-logic/sol-and-set-theory/comparing-sets.tex

Comparing Sets

Second-order definition of the subset relation

Second-order definition of equality of sets

Second-order definition of nonemptiness

Proposed cardinal comparison by an injective function

Source formula proposed to define equinumerosity

Second-order sentence intended to express Schroeder Bernstein

Proof

Source file content/second-order-logic/sol-and-set-theory/cardinalities.tex

Cardinalities of Sets

Explain

Source formula proposed to characterize infinite subsets

Source formula proposed to characterize enumerable subsets

Source file content/second-order-logic/sol-and-set-theory/power-of-continuum.tex

The Power of the Continuum

Explain

Coding a subset by an element and a binary relation

Formulas for coding one subset and a power set

Explain

Cantor theorem expressed through codes for subsets

Explain

Source formula proposed to characterize continuum-sized subsets

Proof

Source equivalence proposed for a continuum-sized domain

Explain

Source sentence intended to express the Continuum Hypothesis

Source sentence intended to express failure of the Continuum Hypothesis

Source disclosures