Second-order logic

Second-order Logic and Set Theory

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

% Part: second-order-logic% Chapter: sol-and-set-theory\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sol}{set}{Second-order Logic and Set Theory}\begin{editorial}This section deals with coding powersets and the continuum insecond-order logic. The results are stated but proofs have yet to befilled in. There are no problems yet---and the definitions and resultsthemselves may have problems. Use with caution and report anythingthat's false or unclear.\end{editorial}\olimport{introduction}\olimport{comparing-sets}\olimport{cardinalities}\olimport{power-of-continuum}\OLEndChapterHook\end{document}

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

% Part: second-order-logic% Chapter: sol-and-sets% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{set}{int}\olsection{Introduction}Since second-order logic can quantify over subsets of the domain aswell as functions, it is to be expected that some amount, at least, ofset theory can be carried out in second-order logic. By ``carry out,''we mean that it is possible to express set theoretic properties andstatements in second-order logic, and is possible without any special,non-logical vocabulary for sets (e.g., the membership !!{predicate} ofset theory).  For instance, we can define unions and intersections ofsets and the subset relationship, but also compare the sizes of sets,and state results such as Cantor's Theorem.\end{document}

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

% Part: second-order-logic% Chapter: sol-and-sets% Section: comparing-sets\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{set}{cmp}\olsection{Comparing Sets}\begin{prop}The !!{formula} $\lforall[x][(X(x) \lif Y(x))]$ defines the subsetrelation, i.e., $\Sat{M}{\lforall[x][(X(x) \lif Y(x))]}[s]$ iff $s(X)\subseteq s(Y)$.\end{prop}\begin{prop}The !!{formula} $\lforall[x][(X(x) \liff Y(x))]$ defines the identityrelation on sets, i.e., $\Sat{M}{\lforall[x][(X(x) \liff Y(x))]}[s]$iff $s(X) = s(Y)$.\end{prop}\begin{prop}The !!{formula} $\lexists[x][X(x)]$ defines the property of beingnon-empty, i.e., $\Sat{M}{\lexists[x][X(x)]}[s]$ iff $s(X) \neq\emptyset$.\end{prop}A set~$X$ is no larger than a set~$Y$, $\cardle{X}{Y}$, iff there is!!a{injective} function $f\colon X \to Y$.  Since we can express thata function is injective, and also that its values for arguments in~$X$are in~$Y$, we can also define the relation of being no larger than onsubsets of the domain.\begin{prop}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])]])]\]defines the relation of being no larger than.\end{prop}Two sets are the same size, or ``equinumerous,'' $\cardeq{X}{Y}$, iffthere is !!a{bijective} function~$f\colon X \to Y$.\begin{prop}The formula\begin{multline*}  \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)])])])]\end{multline*}defines the relation of being equinumerous with.\end{prop}We will abbreviate these !!{formula}s, respectively, as $X \subseteq Y$,$X = Y$, $X \neq \emptyset$, $\cardle{X}{Y}$, and$\cardeq{X}{Y}$. (This may be slightly confusing, since we use thesame notation when we speak informally about sets $X$ and $Y$---buthere the notation is an abbreviation for !!{formula}s in second-orderlogic involving one-place relation variables $X$ and~$Y$.)\begin{prop}The !!{sentence} $\lforall[X][\lforall[Y][((\cardle{X}{Y} \land    \cardle{Y}{X}) \lif \cardeq{X}{Y})]]$ is valid.\end{prop}\begin{proof}The !!{sentence} is satisfied in !!a{structure}~$\Struct{M}$ if, forany subsets $X \subseteq \Domain{M}$ and $Y \subseteq \Domain{M}$, if$\cardle{X}{Y}$ and $\cardle{Y}{X}$ then $\cardeq{X}{Y}$.  But thisholds for \emph{any} sets $X$ and $Y$---it is the Schr\"oder-BernsteinTheorem.\end{proof}\end{document}

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

% Part: second-order-logic% Chapter: sol-and-sets% Section: cardinalities\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{set}{crd}\olsection{Cardinalities of Sets}\begin{explain}Just as we can express that the domain is finite or infinite,!!{enumerable} or !!{nonenumerable}, we can define the property of asubset of~$\Domain{M}$ being finite or infinite, !!{enumerable} or!!{nonenumerable}.\end{explain}\begin{prop}The formula $\fn{Inf}(X) \ident$\begin{multline*}\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)])]])]\end{multline*}is satisfied with respect to a variable assignment~$s$ iff $s(X)$ isinfinite.\end{prop}\begin{prop}The formula $\fn{Count}(X) \ident $\begin{multline*}\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])]])\end{multline*}is satisfied with respect to a variable assignment~$s$ iff $s(X)$ is!!{enumerable}.\end{prop}We know from Cantor's Theorem that there are !!{nonenumerable} sets,and in fact, that there are infinitely many different levels ofinfinite sizes.  Set theory develops an entire arithmetic of sizes ofsets, and assigns infinite cardinal numbers to sets.  The naturalnumbers serve as the cardinal numbers measuring the sizes of finitesets. The cardinality of !!{denumerable} sets is the first infinitecardinality, called~$\aleph_0$ (``aleph-nought'' or``aleph-zero''). The next infinite size is~$\aleph_1$. It is thesmallest size a set can be without being countable (i.e., ofsize~$\aleph_0$).  We can define ``$X$ has size $\aleph_0$'' as$\fn{Aleph}_0(X) \liff \fn{Inf}(X) \land \fn{Count}(X)$.  $X$ has size$\aleph_1$ iff all its subsets are finite or have size~$\aleph_0$, butis not itself of size~$\aleph_0$. Hence we can express this by theformula $\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)$. Being of size $\aleph_2$ is defined similarly, etc.There is one size of special interest, the so-called cardinality ofthe continuum.  It is the size of $\Pow{\Nat}$, or, equivalently, thesize of~$\Real$. That a set is the size of the continuum can also beexpressed in second-order logic, but requires a bit more work.\end{document}

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

% Part: second-order-logic% Chapter: sol-and-sets% Section: power-of-continuum\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{set}{pow}\olsection{The Power of the Continuum}\begin{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 \emph{third-order} logic.  For instance, if we wanted tostate Cantor's Theorem that there is no !!{injective} function fromthe power set of a set to the set itself, we might try to formulate itas ``for every set~$X$, and every set~$P$, if $P$ is the power setof~$X$, then not $\cardle{P}{X}$''. And to say that $P$ is the power setof~$X$ would require formalizing that the !!{element}s of $P$ are alland only the subsets of~$X$, so something like $\lforall[Y][(P(Y)  \liff Y \subseteq X)]$. The problem lies in $P(Y)$: that is not!!a{formula} of second-order logic, since only terms can be argumentsto one-place relation variables like~$P$.We can, however, \emph{simulate} quantification over sets of sets, ifthe domain is large enough.  The idea is to make use of the fact thattwo-place relations~$R$ relates !!{element}s of the !!{domain} to!!{element}s of the !!{domain}. Given such an~$R$, we can collect allthe !!{element}s to which some~$x$ is $R$-related: $\Setabs{y \in  \Domain{M}}{R(x,y)}$ is the set ``coded by''~$x$.  Conversely, if$Z \subseteq \Pow{\Domain{M}}$ is some collection of subsetsof~$\Domain{M}$, and there are at least as many !!{element}sof~$\Domain{M}$ as there are sets in~$Z$, then there is also arelation~$R \subseteq \Domain{M}^2$ such that every $Y \in Z$ is codedby some~$x$ using~$R$.\end{explain}\begin{defn}If $R \subseteq \Domain{M}^2$, then \emph{$x$ $R$-codes} $\Setabs{y  \in \Domain{M}}{R(x, y)}$.\end{defn}If !!a{element}~$x \in \Domain{M}$ $R$-codes a set $Z \subseteq\Domain{M}$, then a set $Y \subseteq \Domain{M}$ codes a set of sets,namely the sets coded by the !!{element}s of~$Y$.  So a set $Y$ can$R$-code $\Pow{X}$. It does so iff for every $Z \subseteq X$, some $x\in Y$ $R$-codes~$Z$, and every $x \in Y$ $R$-codes a~$Z \subseteq X$.\begin{prop}The !!{formula}  \[  \fn{Codes}(x, R, Z) \ident \lforall[y][(Z(y) \liff    R(x, y))]  \]expresses that $s(x)$ $s(R)$-codes $s(Z)$.  The!!{formula} \begin{multline*}  \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)]]\end{multline*}expresses that $s(Y)$ $s(R)$-codes the power set of~$s(X)$, i.e., theelements of $s(Y)$ $s(R)$-code exactly the subsets of $s(X)$.\end{prop}\begin{explain}With this trick, we can express statements about the power set byquantifying over the codes of subsets rather than the subsetsthemselves.  For instance, Cantor's Theorem can now be expressedby saying that there is no !!{injective} function from the domainof any relation that codes the power set of~$X$ to~$X$ itself.\end{explain}\begin{prop}The sentence\begin{multline*}  \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)))])])]]]\end{multline*}is valid.\end{prop}\begin{explain}The power set of !!a{denumerable} set is !!{nonenumerable}, and so itscardinality is larger than that of any !!{denumerable} set (which is$\aleph_0$).  The size of $\Pow{\Nat}$ is called the ``power of thecontinuum,'' since it is the same size as the points on the realnumber line,~$\Real$. If the !!{domain} is large enough to code thepower set of !!a{denumerable} set, we can express that a set is thesize of the continuum by saying that it is equinumerous with anyset~$Y$ that codes the power set of set~$X$ of size~$\aleph_0$. (If thedomain is not large enough, i.e., it contains no subset equinumerouswith~$\Real$, then there can also be no relation that codes~$\Pow{X}$.)\end{explain}\begin{prop}If $\cardle{\Real}{\Domain{M}}$, then the !!{formula}\begin{multline*}\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])]])]]\end{multline*}expresses that $\cardeq{s(Y)}{\Real}$.\end{prop}\begin{proof}  $\fn{Pow}(Y, R, X)$ expresses that $s(Y)$ $s(R)$-codes the power set  of~$s(X)$, which $\fn{Aleph}_0(X)$ says is countable. So $s(Y)$ is  at least as large as the power of the continuum, although it may be  larger (if multiple elements of $s(Y)$ code the same subset of~$X$).  This is ruled out be the last conjunct, which requires the  association between elements of $s(Y)$ and subsets of $s(Z)$ via  $s(R)$ to be !!{injective}.\end{proof}\begin{prop}$\cardeq{\Domain{M}}{\Real}$ iff\begin{multline*}  \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)]])])])]]]}.        \end{multline*}  \end{prop}\begin{explain}The Continuum Hypothesis is the statement that the size of thecontinuum is the first !!{nonenumerable} cardinality, i.e, that$\Pow{\Nat}$ has size~$\aleph_1$. \end{explain}\begin{prop}The Continuum Hypothesis is true iff \[\fn{CH} \ident\lforall[X][(\fn{Aleph}_1(X) \liff \fn{Cont}(X))]\] is valid.\end{prop}Note that it isn't true that $\lnot \fn{CH}$ is valid iff theContinuum Hypothesis is false. In !!a{enumerable} domain, there are nosubsets of size~$\aleph_1$ and also no subsets of the size of thecontinuum, so $\fn{CH}$ is always true in !!a{enumerable}domain. However, we can give a different sentence that is valid iffthe Continuum Hypothesis is false:\begin{prop}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})])]\] is valid.\end{prop}\end{document}