Second-order logic

Metatheory of Second-order Logic

content/second-order-logic/metatheory/metatheory.tex

% Part: second-order-logic% Chapter: metatheory\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sol}{met}{Metatheory of Second-order Logic}\olimport{introduction}\olimport{second-order-arithmetic}\olimport{undecidability-and-axiomatizability}\olimport{compactness}\olimport{loewenheim-skolem}\OLEndChapterHook\end{document}

content/second-order-logic/metatheory/introduction.tex

% Part: second-order-logic% Chapter: metatheory% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{met}{int}\olsection{Introduction}First-order logic has a number of nice properties. We know it is notdecidable, but at least it is axiomatizable. That is, there are proofsystems for first-order logic which are sound and complete, i.e., theygive rise to !!a{derivability} relation~$\Proves$ with the propertythat for any set of !!{sentence}s~$\Gamma$ and !!{sentence}~$!A$,$\Gamma \Entails !A$ iff $\Gamma \Proves !A$.  This means inparticular that the validities of first-order logic are !!{computably  enumerable}. There is a computable function~$f\colon \Nat \to\Sent[L]$ such that the values of~$f$ are all and only the valid!!{sentence}s of~$\Lang{L}$. This is so because !!{derivation}s can beenumerated, and those that !!{derive} a single~!!{sentence} are thenmapped to that !!{sentence}.  Second-order logic is more expressivethan first-order logic, and so it is in general more complicated tocapture its validities.  In fact, we'll show that second-order logicis not only undecidable, but its validities are not even !!{computably  enumerable}. This means there can be no sound and complete proofsystem for second-order logic (although sound, but incomplete proofsystems are available and in fact are important objects of research).First-order logic also has two more properties: it is compact (ifevery finite subset of a set~$\Gamma$ of !!{sentence}s is satisfiable,$\Gamma$ itself is satisfiable) and the L\"owenheim--Skolem Theoremholds for it (if $\Gamma$ has an infinite model it has!!a{denumerable} model). Both of these results fail for second-orderlogic. Again, the reason is that second-order logic can express factsabout the size of !!{domain}s that first-order logic cannot.\end{document}

content/second-order-logic/metatheory/second-order-arithmetic.tex

% Part: second-order-logic% Chapter: metatheory% Section: second-order-arithmetic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{met}{spa}\olsection{Second-order Arithmetic}Recall that the theory $\Th{PA}$ of Peano arithmetic includes theeight axioms of~$\Th{Q}$,\begin{align*}& \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)].\end{align*}The latter is a ``schema,'' i.e., a pattern that generates infinitelymany !!{sentence}s of the language of arithmetic, one for each!!{formula}~$!A(x)$. We call this schema the (first-order)\emph{axiom schema of induction}. In \emph{second-order} Peano arithmetic~$\Th{PA^2}$, inductioncan be stated as a single sentence. $\Th{PA^2}$consists of the first eight axioms above plus the (second-order)\emph{induction axiom}:\[\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)])].\]It says that if a subset~$X$ of the !!{domain}contains~$\Assign{\Obj{0}}{M}$ and with any~$x \in \Domain{M}$ alsocontains~$\Assign{\prime}{M}(x)$ (i.e., it is ``closed undersuccessor'') it contains everything in the !!{domain} (i.e., $X =\Domain{M})$.The induction axiom guarantees that any !!{structure} satisfying itcontains only those !!{element}s of~$\Domain{M}$ the axioms require tobe there, i.e., the values of~$\num{n}$ for $n \in \Nat$. A model of$\Th{PA^2}$ contains no non-standard numbers.\begin{thm}\ollabel{thm:sol-pa-standard}If $\Sat{M}{\Th{PA^2}}$ then $\Domain{M} =\Setabs{\Value{\num{n}}{M}}{n \in \Nat}$.\end{thm}\begin{proof}Let $N = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}$, and suppose$\Sat{M}{\Th{PA^2}}$. Of course, for any $n \in \Nat$,$\Value{\num{n}}{M} \in \Domain{M}$, so $N \subseteq \Domain{M}$.Now for inclusion in the other direction. Consider a variableassignment $s$ with $s(X) = N$. By assumption,\begin{align*}\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]. & \end{align*}Consider the antecedent of this conditional.  $\Value{\Obj{0}}{M} \inN$, and so $\Sat{M}{X(\Obj{0})}[s]$.  The second conjunct,$\lforall[x][(X(x) \lif X(x'))]$ is also satisfied. For suppose $x \inN$. By definition of~$N$, $x = \Value{\num{n}}{M}$ for some~$n$.  Thatgives $\Assign{\prime}{M}(x) = \Value{\num{n+1}}{M} \in N$. So,$\Assign{\prime}{M}(x) \in N$.We have that $\Sat{M}{X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]}[s]$.Consequently, $\Sat{M}{\lforall[x][X(x)]}[s]$. But that means that forevery $x \in \Domain{M}$ we have $x \in s(X) = N$. So, $\Domain{M}\subseteq N$.\end{proof}\begin{cor}\ollabel{cor:sol-pa-categorical}Any two models of~$\Th{PA^2}$ are isomorphic.\end{cor}\begin{proof}By \olref{thm:sol-pa-standard}, the domain of any model of $\Th{PA^2}$is exhausted by $\Value{\num{n}}{M}$. Any such model is also a modelof~$\Th{Q}$. By \olref[mod][mar][stm]{prop:thq-standard}, any suchmodel is standard, i.e., isomorphic to~$\Struct{N}$.\end{proof}Above we defined $\Th{PA^2}$ as the theory that contains the first eight arithmetical axioms plus the second-order induction axiom.  In fact, thanksto the expressive power of second-order logic, only the \emph{first two} of the arithmetical axioms plus induction are needed for second-order Peano arithmetic.\begin{prop}\ollabel{prop:sol-pa-definable}Let $\Th{PA^{2\dagger}}$ be the second-order theory containing thefirst two arithmetical axioms (the successor axioms) and thesecond-order induction axiom. Then $\le$, $+$, and $\times$ are definablein $\Th{PA^{2\dagger}}$.\end{prop}\begin{proof}To show that $\le$ is definable, we have to find a formula~$!A_\le(x, y)$such that $\Sat{N}{!A_\le(\num n, \num m)}$ iff $n \le m$. Consider the formula\[!B(x, Y) \ident Y(x) \land \lforall[y][(Y(y) \lif Y(y'))]\]Clearly, $!B(\num n, Y)$ is satisfied by a set $Y \subseteq \Nat$ iff$\Setabs{m}{n \le m} \subseteq Y$, so we can take $!A_\le(x, y) \ident\lforall[Y][(!B(x, Y) \lif Y(y))]$.To see that addition is definable observe that $k+l=m$ iff there is afunction $u$ such that $u(0)=k$, $u(n')=u(n)'$ for all $n$, and $m = u(l)$. We can use this equivalence to define addition in $\Th{PA^{2\dagger}}$ by the following formula:\[!A_+(x,y,z) \ident \lexists[u][(u(\Obj 0)=x \land \lforall[w][u(x')=u (x)'] \land u(y)=z)]\] It should be clear that $\Sat{N}{!A_+(\num k, \num l, \num m)}$ iff $k+l=m$.\end{proof}\begin{prob}Complete the proof of \olref[sol][met][spa]{prop:sol-pa-definable}.\end{prob}\end{document}

content/second-order-logic/metatheory/undecidability-and-axiomatizability.tex

% Part: second-order-logic% Chapter: metatheory% Section: undecidability-and-axiomatizability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{met}{nax}\olsection{Second-order Logic is not Axiomatizable}\begin{thm}\ollabel{thm:sol-undecidable}Second-order logic is undecidable.\end{thm}\begin{proof}A first-order !!{sentence} is valid in first-order logic iff it isvalid in second-order logic, and first-order logic is undecidable.\end{proof}\begin{thm}\ollabel{cor:sol-not-axiomatizable}There is no sound and complete !!{derivation} system for second-order logic.\end{thm}\begin{proof}Let $!A$ be !!a{sentence} in the language of arithmetic.  $\Sat{N}{!A}$iff $\Th{PA^2} \Entails !A$. Let $!P$ be the conjunction of the nineaxioms of~$\Th{PA^2}$. $\Th{PA^2} \Entails !A$ iff $\Entails !P \lif!A$, i.e., $\Sat{M}{!P \lif !A$}. Now consider the !!{sentence}$\lforall[z][\lforall[u][\lforall[u'][\lforall[u''][\lforall[L][(!P' \lif !A')]]]]]$ resulting byreplacing $\Obj{0}$ by $z$, $\prime$ by the one-place functionvariable $u$, $+$ and $\times$ by the two-place function-variables $u'$ and  $u''$, respectively,and $<$ by the two-place relation variable~$L$ anduniversally quantifying.  It is a valid sentence of pure second-orderlogic iff the original sentence was valid iff $\Th{PA^2} \Entails !A$iff $\Sat{N}{!A}$.  Thus if there were a sound and complete proofsystem for second-order logic, we could use it to define a computableenumeration $f\colon \Nat \to \Sent[L_A]$ of the !!{sentence}s truein~$\Struct{N}$. This function would be representable in~$\Th{Q}$ bysome first-order formula~$!B_f(x, y)$. Then the!!{formula}~$\lexists[x][!B_f(x, y)]$ would define the set of truefirst-order !!{sentence}s of~$\Struct{N}$, contradicting Tarski'sTheorem.\end{proof}\end{document}

content/second-order-logic/metatheory/compactness.tex

% Part: second-order-logic% Chapter: metatheory% Section: compactness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{met}{com}\olsection{Second-order Logic is not Compact}\begin{explain}Call a set of sentences~$\Gamma$ \emph{finitely satisfiable} if everyone of its finite subsets is satisfiable.  First-order logic has theproperty that if a set of !!{sentence}s~$\Gamma$ is finitelysatisfiable, it is satisfiable.  This property is called\emph{compactness}.  It has an equivalent version involvingentailment: if $\Gamma \Entails !A$, then already $\Gamma_0 \Entails!A$ for some finite subset~$\Gamma_0 \subseteq \Gamma$. In thisversion it is an immediate corollary of the completeness theorem: forif $\Gamma \Entails !A$, by completeness $\Gamma \Proves !A$. But a!!{derivation} can only make use of finitely many !!{sentence}sof~$\Gamma$.Compactness is not true for second-order logic. There are sets ofsecond-order !!{sentence}s that are finitely satisfiable but notsatisfiable, and that entail some~$!A$ without a finite subsetentailing~$!A$.  \end{explain}\begin{thm}\ollabel{thm:sol-undecidable}Second-order logic is not compact.\end{thm}\begin{proof}Recall that \[\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)]]])]\]is satisfied in !!a{structure} iff its domain is infinite. Let$!A^{\ge n}$ be a sentence that asserts that the domain has at least$n$ !!{element}s, e.g.,\[!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])]].\]Consider the set of !!{sentence}s\[\Gamma = \{\lnot \fn{Inf}, !A^{\ge 1}, !A^{\ge 2}, !A^{\ge 3}, \dots\}.\]It is finitely satisfiable, since for any finite subset~$\Gamma_0\subseteq \Gamma$there is some $k$ so that $!A^{\ge k} \in \Gamma$ but no $!A^{\ge n}\in \Gamma$ for $n>k$. If $\Domain{M}$ has $k$ !!{element}s,$\Sat{M}{\Gamma_0}$. But, $\Gamma$ is not satisfiable: if$\Sat{M}{\lnot \fn{Inf}}$, $\Domain{M}$ must be finite, say, ofsize~$k$. Then $\Sat/{M}{!A^{\ge k+1}}$.\end{proof}\begin{prob}Give an example of a set~$\Gamma$ and !!a{sentence}~$!A$ so that$\Gamma \Entails !A$ but for every finite subset~$\Gamma_0 \subseteq\Gamma$, $\Gamma_0 \Entails/ !A$.\end{prob}\end{document}

content/second-order-logic/metatheory/loewenheim-skolem.tex

% Part: second-order-logic% Chapter: metatheory% Section: compactness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{met}{lst}\olsection{The L\"owenheim--Skolem Theorem Fails for Second-order Logic}\begin{explain}The (Downward) L\"owenheim--Skolem Theorem states that every set of!!{sentence}s with an infinite model has !!a{enumerable} model.  It,too, is a consequence of the completeness theorem: the proof ofcompleteness generates a model for any consistent set of!!{sentence}s, and that model is !!{enumerable}.  There is also anUpward L\"owenheim--Skolem Theorem, which guarantees that if a set of!!{sentence}s has !!a{denumerable} model it also has!!a{nonenumerable} model.  Both theorems fail in second-order logic.\end{explain}\begin{thm}\ollabel{thm:sol-no-ls} The L\"owenheim--Skolem Theorem fails forsecond-order logic: There are !!{sentence}s with infinite models butno !!{enumerable} models.\end{thm}\begin{proof}Recall that \[\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)])]]]\]is true in !!a{structure}~$\Struct{M}$ iff $\Domain{M}$ is!!{enumerable}, so $\lnot\fn{Count}$ is true in~$\Struct{M}$iff $\Domain{M}$ is !!{nonenumerable}.  There aresuch !!{structure}s---take any !!{nonenumerable} set as the!!{domain}, e.g., $\Pow{\Nat}$ or~$\Real$. So $\lnot \fn{Count}$ has infinite models but no !!{enumerable} models.\end{proof}\begin{thm}There are !!{sentence}s with !!{denumerable} but no!!{nonenumerable} models.\end{thm}\begin{proof}$\fn{Count} \land \fn{Inf}$ is true in $\Nat$ but not in any  !!{structure}~$\Struct{M}$ with $\Domain{M}$ !!{nonenumerable}.\end{proof}\end{document}