Second-order logic

Syntax and Semantics

content/second-order-logic/syntax-and-semantics/syntax-and-semantics.tex

% Part: second-order-logic% Chapter: syntax-and-semantics\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sol}{syn}{Syntax and Semantics}\begin{editorial}Basic syntax and semantics for SOL covered so far. As a chapter it'stoo short. Substitution for second-order variables has to be coveredto be able to talk about !!{derivation} systems for SOL, and there's somesubtle issues there.\end{editorial}\olimport{introduction}\olimport{terms-formulas}\olimport{satisfaction}\olimport{semantic-notions}\olimport{expressive-power}\olimport{inf-count}\OLEndChapterHook\end{document}

content/second-order-logic/syntax-and-semantics/introduction.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{int}\olsection{Introduction}In first-order logic, we combine the non-logical symbols of a givenlanguage, i.e., its !!{constant}s, !!{function}s, and !!{predicate}s,with the logical symbols to express things about first-order!!{structure}s.  This is done using the notion of satisfaction, whichrelates !!a{structure}~$\Struct{M}$, together with a variableassignment~$s$, and !!a{formula}~$!A$: $\Sat{M}{!A}[s]$ holds iff what$!A$ expresses when its !!{constant}s, !!{function}s, and!!{predicate}s are interpreted as $\Struct{M}$ says, and its freevariables are interpreted as~$s$ says, is true.  The interpretation ofthe !!{identity}~$\eq$ is built into the definition of$\Sat{M}{!A}[s]$, as is the interpretation of~$\lforall$ and$\lexists$. The former is always interpreted as the identity relationon the !!{domain}~$\Domain{M}$ of the structure, and the quantifiersare always interpreted as ranging over the entire !!{domain}.  But,crucially, quantification is only allowed over elements of the!!{domain}, and so only object !!{variable}s are allowed to follow aquantifier.In second-order logic, both the language and the definition ofsatisfaction are extended to include free and bound function andpredicate variables, and quantification over them.  These variablesare related to !!{function}s and !!{predicate}s the same way thatobject variables are related to !!{constant}s.  They play the samerole in the formation of terms and !!{formula}s of second-order logic,and quantification over them is handled in a similar way.  In the\emph{standard} semantics, the second-order quantifiers range over allpossible objects of the right type ($n$-place functions from$\Domain{M}$ to~$\Domain{M}$ for function variables, $n$-placerelations for predicate variables).  For instance, while$\lforall[\Obj{v_0}][(\Obj{P^1_0}(\Obj{v_0}) \lor \lnot  \Obj{P^1_0}(\Obj{v_0}))]$ is a formula in both first- and second-orderlogic, in the latter we can also consider$\lforall[\Obj{V^1_0}][\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj{v_0}) \lor    \lnot \Obj{V^1_0}(\Obj{v_0}))]]$ and$\lexists[\Obj{V^1_0}][\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj{v_0}) \lor    \lnot \Obj{V^1_0}(\Obj{v_0}))]]$. Since these contain no free variables,they are !!{sentence}s of second-order logic. Here, $\Obj{V^1_0}$ is asecond-order $1$-place predicate variable.  The allowableinterpretations of $\Obj{V^1_0}$ are the same that we can assign to a$1$-place !!{predicate} like $\Obj{P^1_0}$, i.e., subsetsof~$\Domain{M}$.  Quantification over them then amounts to saying that$\lforall[\Obj{v_0}][(\Obj{V^1_0}(\Obj v_0) \lor \lnot  \Obj{V^1_0}(v_0))]$ holds for all ways of assigning a subsetof~$\Domain{M}$ as the value of $\Obj{V^1_0}$, or for at least one.Since every set either contains or fails to contain a given object,both are true in any !!{structure}.\end{document}

content/second-order-logic/syntax-and-semantics/terms-formulas.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: terms-formulas\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{frm}\olsection{Terms and \printtoken{P}{formula}}Like in first-order logic, expressions of second-order logic are builtup from a basic vocabulary containing \emph{!!{variable}s},\emph{!!{constant}s}, \emph{!!{predicate}s} and sometimes\emph{!!{function}s}.  From them, together with logical connectives,quantifiers, and punctuation symbols such as parentheses and commas,\emph{terms} and \emph{!!{formula}s} are formed.  The difference isthat in addition to variables for objects, second-order logic alsocontains variables for relations and functions, and allowsquantification over them. So the logical symbols of second-order logicare those of first-order logic, plus:\begin{enumerate}\item A !!{denumerable}s set of second-order relation !!{variable}s of  every arity~$n$: $\Obj V_0^n$, $\Obj V_1^n$, $\Obj V_2^n$, \dots\item A !!{denumerable}s set of second-order function !!{variable}s:  $\Obj u_0^n$, $\Obj u_1^n$, $\Obj u_2^n$, \dots\end{enumerate}Just as we use $x$, $y$, $z$ as meta-variables for first-ordervariables $\Obj v_i$, we'll use $X$, $Y$, $Z$, etc., as metavariablesfor $\Obj V_i^n$ and $u$, $v$, etc., as meta-variables for~$\Obj u_i^n$.\begin{explain}The non-logical symbols of a second-order language are specified thesame way a first-order language is: by listing its !!{constant}s,!!{function}s, and !!{predicate}s.In first-order logic, the !!{identity}~$\eq$ is usually included. Infirst-order logic, the non-logical symbols of a language~$\Lang{L}$are crucial to allow us to express anything interesting. There are ofcourse !!{sentence}s that use no non-logical symbols, but withonly~$\eq$ it is hard to say anything interesting.  In second-orderlogic, since we have an unlimited supply of relation and functionvariables, we can say anything we can say in a first-order languageeven without a special supply of non-logical symbols.\end{explain}\begin{defn}[Second-order Terms]The set of \emph{second-order terms} of~$\Lang L$, $\TrmSOL[L]$, isdefined by adding to \olref[fol][syn][frm]{defn:terms} the clause\begin{enumerate}\item If $u$ is an $n$-place function variable and $t_1$, \dots, $t_n$  are terms, then $\Atom{u}{t_1, \ldots, t_n}$ is a term.\end{enumerate}\end{defn}\begin{explain}So, a second-order term looks just like a first-order term, exceptthat where a first-order term contains !!a{function}~$\Obj{f^n_i}$, asecond-order term may contain a function variable~$\Obj{u^n_i}$ in itsplace.\end{explain}\begin{defn}[Second-order \usetoken{s}{formula}]The set of \emph{second-order !!{formula}s}~$\FrmSOL[L]$ of thelanguage~$\Lang L$ is defined by adding to\olref[fol][syn][frm]{defn:formulas} the clauses\begin{enumerate}\item If $X$ is an $n$-place predicate variable and $t_1$, \dots,  $t_n$ are second-order terms of~$\Lang L$, then  $\Atom{X}{t_1,\ldots, t_n}$ is an atomic !!{formula}.\tagitem{prvAll}{If $!A$ is !!a{formula} and $u$ is a function variable,  then $\lforall[u][!A]$ is !!a{formula}.}{}\tagitem{prvAll}{If $!A$ is !!a{formula} and $X$ is a predicate variable,  then $\lforall[X][!A]$ is !!a{formula}.}{}\tagitem{prvEx}{If $!A$ is !!a{formula} and $u$ is a function variable,  then $\lexists[u][!A]$ is !!a{formula}.}{}\tagitem{prvEx}{If $!A$ is !!a{formula} and $X$ is a predicate variable,  then $\lexists[X][!A]$ is !!a{formula}.}{}\end{enumerate}\end{defn}\end{document}

content/second-order-logic/syntax-and-semantics/satisfaction.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: satisfaction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{sat}\olsection{Satisfaction}\begin{explain}To define the satisfaction relation $\Sat{M}{!A}[s]$ for second-order!!{formula}s, we have to extend the definitions to cover second-order!!{variable}s.  The notion of !!a{structure} is the same for second-orderlogic as it is for first-order logic. There is only a difference forvariable assignments~$s$: these now must not just provide values forthe first-order !!{variable}s, but also for the second-order !!{variable}s.\end{explain}\begin{defn}[Variable Assignment]A \emph{variable assignment}~$s$ for !!a{structure}~$\Struct{M}$ is afunction which maps each\begin{enumerate}\item object !!{variable}~$\Obj{v_i}$ to an element of~$\Domain M$,  i.e., $s(\Obj{v_i}) \in \Domain{M}$\item $n$-place relation variable~$\Obj{V_i^n}$ to an $n$-place  relation on~$\Domain{M}$, i.e., $s(\Obj{V_i^n}) \subseteq \Domain{M}^n$;\item $n$-place function variable~$\Obj{u_i^n}$ to an $n$-place  function from $\Domain{M}$ to $\Domain{M}$, i.e.,  $s(\Obj{u_i^n})\colon \Domain{M}^n \to \Domain{M}$;\end{enumerate}\end{defn}\begin{explain}!!^a{structure} assigns !!a{value} to each !!{constant} and!!{function}, and a second-order variable assignment assigns objects andfunctions to each object and function variable. Together, they let usassign a value to every term.\end{explain}\begin{defn}[\usetoken{S}{value} of a Term]If $t$ is a term of the language~$\Lang L$, $\Struct M$ is!!a{structure} for~$\Lang L$, and $s$ is !!a{variable} assignmentfor~$\Struct M$, the \emph{!!{value}}~$\Value{t}{M}[s]$ is defined asfor first-order terms, plus the following clause:\begin{quote}\indcase{t}{\Atom{u}{t_1, \ldots, t_n}}{\[\Value{\indfrm}{M}[s] = s(u)(\Value{t_1}{M}[s], \ldots,\Value{t_n}{M}[s]).\]}\end{quote}\end{defn}\begin{defn}[$x$-Variant]If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$,then any !!{variable} assignment $s'$ for $\Struct M$ which differsfrom $s$ at most in what it assigns to $x$ is called an\emph{$x$-variant} of~$s$.  If $s'$ is an $x$-variant of $s$ we write$\varAssign{s'}{s}{x}$. (Similarly for second-order variables $X$ or $u$.)\end{defn}\begin{defn}  If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$  and $m \in \Domain{M}$, then the assignment~$\Subst{s}{m}{x}$ is the  !!{variable} assignment defined by  \[\Subst{s}{m}{y} = \begin{cases}    m & \text{if } y \ident x\\    s(y) & \text{otherwise},  \end{cases}\]  If $X$ is an $n$-place relation !!{variable} and $M \subseteq  \Domain{M}^n$, then $\Subst{s}{M}{X}$ is the !!{variable} assignment  defined by  \[\Subst{s}{M}{y} = \begin{cases}    M & \text{if } y \ident X\\    s(y) & \text{otherwise}.   \end{cases}\]  If $u$ is an $n$-place function !!{variable} and $f\colon \Domain{M}^n  \to \Domain{M}$, then $\Subst{s}{f}{u}$ is the !!{variable} assignment  defined by  \[\Subst{s}{f}{y} = \begin{cases}    f & \text{if } y \ident u\\    s(y) & \text{otherwise}.  \end{cases}\]  In each case, $y$ may be any first- or second-order !!{variable}.\end{defn}\begin{defn}[Satisfaction]For second-order !!{formula}s~$!A$, the definition of satisfaction islike \olref[fol][syn][sat]{defn:satisfaction} with the addition of:\begin{enumerate}\item \indcase{!A}{\Atom{X^n}{t_1, \dots, t_n}}{$\Sat{M}{\indfrm}[s]$  iff $\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in  s(X^n)$.}\tagitem{prvAll}{%  \indcase{!A}{\lforall[X][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every $M  \subseteq \Domain{M}^n$, $\Sat{M}{!B}[\Subst{s}{M}{X}]$.}}{}\tagitem{prvEx}{%  \indcase{!A}{\lexists[X][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least  one $M \subseteq \Domain{M}^n$ so that  $\Sat{M}{!B}[\Subst{s}{M}{X}]$.}}{}\tagitem{prvAll}{%  \indcase{!A}{\lforall[u][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every  $f\colon \Domain{M}^n \to \Domain{M}$,  $\Sat{M}{!B}[\Subst{s}{f}{u}]$.}}{}\tagitem{prvEx}{%  \indcase{!A}{\lexists[u][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least  one $f\colon \Domain{M}^n \to \Domain{M}$ so that  $\Sat{M}{!B}[\Subst{s}{f}{u}]$.}}{}\end{enumerate}\end{defn}\begin{ex}  Consider the !!{formula} $\lforall[z][(\Atom{X}{z} \liff \lnot    \Atom{Y}{z})]$. It contains no second-order quantifiers, but does  contain the second-order !!{variable}s $X$ and~$Y$ (here understood to  be one-place). The corresponding first-order !!{sentence}  $\lforall[z][(\Atom{P}{z} \liff \lnot \Atom{R}{z})]$ says that  whatever falls under the interpretation of~$P$ does not fall under  the interpretation of~$R$ and vice versa. In !!a{structure}, the  interpretation of !!a{predicate}~$P$ is given by the  interpretation~$\Assign{P}{M}$. But for second-order !!{variable}s  like $X$ and~$Y$, the interpretation is provided, not by the  !!{structure} itself, but by !!a{variable} assignment. Since the  second-order !!{formula} is not !!a{sentence} (it includes free  !!{variable}s $X$ and~$Y$), it is only satisfied relative to  !!a{structure}~$\Struct{M}$ together with !!a{variable}  assignment~$s$.  $\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s]$  whenever the !!{element}s of~$s(X)$ are not !!{element}s of~$s(Y)$,  and vice versa, i.e., iff $s(Y) = \Domain{M} \setminus s(X)$. For  instance, take $\Domain{M} = \{1, 2, 3\}$. Since no !!{predicate}s,  !!{function}s, or !!{constant}s are involved, the domain  of~$\Struct{M}$ is all that is relevant. Now for $s_1(X) = \{1, 2\}$  and $s_1(Y) = \{3\}$, we have $\Sat{M}{\lforall[z][(\Atom{X}{z}      \liff \lnot \Atom{Y}{z})]}[s_1]$.  By contrast, if we have $s_2(X) = \{1, 2\}$ and $s_2(Y) = \{2, 3\}$,  $\Sat/{M}{\lforall[z][(\Atom{X}{z} \liff \lnot      \Atom{Y}{z})]}[s_2]$. That's because   $\Sat{M}{\Atom{X}{z}}[\Subst{s_2}{2}{z}]$ (since $2 \in \Subst{s_2}{2}{z}(X)$) but  $\Sat/{M}{\lnot \Atom{Y}{z}}[\Subst{s_2}{2}{z}]$ (since also $2 \in  \Subst{s_2}{2}{z}(Y)$).\end{ex}\begin{ex}  $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land  \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ if there  is an $N \subseteq \Domain{M}$ such that  $\Sat{M}{(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z}  \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]$. And that is the case  for any $N \neq \emptyset$ (so that  $\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]$) and, as in the  previous example, $N = \Domain{M} \setminus s(X)$. In other words,  $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land  \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ iff  $\Domain{M} \setminus s(X)$ is non-empty, i.e., $s(X) \neq  \Domain{M}$. So, the !!{formula} is satisfied, e.g., if $\Domain{M}  = \{1, 2, 3\}$ and $s(X) = \{1, 2\}$, but not if $s(X) = \{1, 2, 3\}  = \Domain{M}$.  Since the !!{formula} is not satisfied whenever $s(X) = \Domain{M}$,  the !!{sentence}  \[  \lforall[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land      \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]  \]  is never satisfied: For any !!{structure}~$\Struct{M}$, the  assignment~$s(X) = \Domain{M}$ will make the !!{sentence} false. On  the other hand, the sentence  \[  \lexists[X][\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land      \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]]  \]  is satisfied relative to any assignment~$s$, since we can always  find $M \subseteq \Domain{M}$ but $M \neq \Domain{M}$ (e.g., $M = \emptyset$).\end{ex}\begin{ex}  The second-order !!{sentence}~$\lforall[X][\lforall[y][X(y)]]$ says  that every $1$-place relation, i.e., every property, holds of every  object. That is clearly never true, since in every~$\Struct{M}$, for  a variable assignment~$s$ with $s(X) = \emptyset$, and $s(y) = a \in  \Domain{M}$ we have $\Sat/{M}{X(y)}[s]$. This means that $!A \lif  \lforall[X][\lforall[y][X(y)]]$ is equivalent in second-order logic  to $\lnot !A$, that is: $\Sat{M}{!A \lif  \lforall[X][\lforall[y][X(y)]]}$ iff $\Sat{M}{\lnot !A}$. In other  words, in second-order logic we can define $\lnot$ using $\lforall$  and~$\lif$.\end{ex}\begin{prob}  Show that in second-order logic $\lforall$ and~$\lif$ can define the other  connectives:  \begin{enumerate}    \item Prove that in second-order logic $!A \land !B$ is equivalent    to $\lforall[X][(!A \lif (!B \lif \lforall[x][X(x)])\lif    \lforall[x][X(x)])]$.    \item Find a second-order formula using only $\lforall$ and $\lif$    equivalent to $!A \lor !B$.  \end{enumerate}\end{prob}\end{document}

content/second-order-logic/syntax-and-semantics/semantic-notions.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: semantic-notions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{sem}\olsection{Semantic Notions}\begin{explain}The central logical notions of \emph{validity}, \emph{entailment}, and\emph{satisfiability} are defined the same way for second-order logicas they are for first-order logic, except that the underlyingsatisfaction relation is now that for second-order !!{formula}s.  Asecond-order !!{sentence}, of course, is !!a{formula} in which allvariables, including predicate and function variables, are bound.\end{explain}\begin{defn}[Validity]A sentence $!A$ is \emph{valid}, $\Entails !A$, iff $\Sat{M}{!A}$ for every!!{structure}~$\Struct M$.\end{defn}\begin{defn}[Entailment]A set of sentences~$\Gamma$ \emph{entails} a sentence~$!A$, $\Gamma\Entails !A$, iff for every !!{structure}~$\Struct M$ with$\Sat{M}{\Gamma}$, $\Sat{M}{!A}$.\end{defn}\begin{defn}[Satisfiability]A set of sentences~$\Gamma$ is \emph{satisfiable} if $\Sat{M}{\Gamma}$for some !!{structure}~$\Struct M$.  If $\Gamma$ is not satisfiable it iscalled \emph{unsatisfiable}.\end{defn}\end{document}

content/second-order-logic/syntax-and-semantics/expressive-power.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: expressive-power\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{exp}\olsection{Expressive Power}\begin{explain}Quantification over second-order variables is responsible for animmense increase in the expressive power of the language over that offirst-order logic.  Second-order existential quantification lets ussay that functions or relations with certain properties exist. Infirst-order logic, the only way to do that is to specify a non-logicalsymbol (i.e., !!a{function} or !!{predicate}) for thispurpose. Second-order universal quantification lets us say that allsubsets of, relations on, or functions from the !!{domain} to the!!{domain} have a property.  In first-order logic, we can only saythat the subsets, relations, or functions assigned to one of thenon-logical symbols of the language have a property.  And when we saythat subsets, relations, functions exist that have a property, or thatall of them have it, we can use second-order quantification inspecifying this property as well. This lets us define relations notdefinable in first-order logic, and express properties of the domainnot expressible in first-order logic.\end{explain}\begin{defn}If $\Struct{M}$ is !!a{structure} for a language~$\Lang{L}$, arelation~$R \subseteq \Domain{M}^2$ is \emph{definable} in~$\Lang{L}$if there is some !!{formula}~$!A_R(x, y)$ with only the variables $x$and~$y$ free, such that $R(a, b)$ holds (i.e., $\tuple{a,b} \in R$)iff $\Sat{M}{!A_R(x, y)}[s]$ for $s(x) = a$ and $s(y) = b$.\end{defn}\begin{ex}In first-order logic we can define the identityrelation~$\Id{\Domain{M}}$ (i.e., $\Setabs{\tuple{a,a}}{a \in  \Domain{M}}$) by the formula $\eq[x][y]$.  Insecond-order logic, we can define this relation\emph{without~$\eq$}. For if $a$ and $b$ are the same !!{element}of~$\Domain{M}$, then they are !!{element}s of the same subsetsof~$\Domain{M}$ (since sets are determined by their!!{element}s). Conversely, if $a$ and $b$ are different, then they arenot !!{element}s of the same subsets: e.g., $a \in \{a\}$ but $b\notin \{a\}$ if $a \neq b$.  So ``being !!{element}s of the samesubsets of~$\Domain{M}$'' is a relation that holds of $a$ and $b$ iff$a = b$. It is a relation that can be expressed in second-order logic,since we can quantify over all subsets of~$\Domain{M}$. Hence, thefollowing !!{formula} defines $\Id{\Domain{M}}$:\[\lforall[X][(X(x) \liff X(y))]\]\end{ex}\begin{prob}Show that $\lforall[X][(X(x) \lif X(y))]$ (note:$\lif$ not~$\liff$!) defines $\Id{\Domain{M}}$.\end{prob}\begin{ex}If $R$ is a two-place !!{predicate}, $\Assign{R}{M}$ is a two-placerelation on~$\Domain{M}$.  Perhaps somewhat confusingly, we'll use $R$as the !!{predicate} for~$R$ and for the relation~$\Assign{R}{M}$itself.  The \emph{transitive closure}~$R^*$ of~$R$ is the relationthat holds between $a$ and $b$ iff for some $c_1$, \dots, $c_k$,$R(a,c_1)$, $R(c_1, c_2)$, \dots, $R(c_k,b)$ holds. This includes thecase if $k = 0$, i.e., if $R(a,b)$ holds, so does $R^*(a,b)$. Thismeans that $R \subseteq R^*$. In fact, $R^*$ is the smallest relationthat includes~$R$ and that is transitive.  We can say in second-orderlogic that $X$ is a transitive relation that includes~$R$:\begin{multline*}  !B_R(X) \ident \lforall[x][\lforall[y][(R(x,y) \lif X(x, y))]] \land {}\\\lforall[x][\lforall[y][\lforall[z][((X(x,y) \land X(y,z)) \lif X(x,      z))]]].\end{multline*}The first conjunct says that $R \subseteq X$ and the secondthat $X$ is transitive.To say that $X$ is the smallest such relation is to say that it isitself included in every relation that includes $R$ and istransitive. So we can define the transitive closure of~$R$ by the!!{formula}\[R^*(X) \ident !B_R(X) \land \lforall[Y][(!B_R(Y) \lif  \lforall[x][\lforall[y][(X(x, y) \lif Y(x,y))]])].\]We have $\Sat{M}{R^*(X)}[s]$ iff $s(X) = R^*$. The transitive closureof~$R$ cannot be expressed in first-order logic.\end{ex}\end{document}

content/second-order-logic/syntax-and-semantics/inf-count.tex

% Part: second-order-logic% Chapter: syntax-and-semantics% Section: size-of-domain\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sol}{syn}{siz}\olsection{Describing Infinite and \usetoken{S}{enumerable}  \usetoken{P}{domain}}A set~$M$ is (Dedekind) infinite iff there is !!a{injective} function~$f\colon M\to M$ which is not !!{surjective}, i.e., with $\ran{f} \neq M$. Infirst-order logic, we can consider a one-place !!{function}~$f$ andsay that the function~$\Assign{f}{M}$ assigned to it in!!a{structure}~$\Struct{M}$ is !!{injective} and $\ran{f} \neq\Domain{M}$:\[\lforall[x][\lforall[y][(\eq[f(x)][f(y)] \to \eq[x][y])]] \land\lexists[y][\lforall[x][\eq/[y][f(x)]]].\]If $\Struct{M}$ satisfies this !!{sentence}, $\Assign{f}{M}:\Domain{M} \to \Domain{M}$ is !!{injective}, and so $\Domain{M}$ mustbe infinite. If $\Domain{M}$ is infinite, and hence such a functionexists, we can let $\Assign{f}{M}$ be that function and $\Struct{M}$will satisfy the !!{sentence}.  However, this requires that our languagecontains the non-logical symbol~$f$ which we use for this purpose. Insecond-order logic, we can simply say that such a function\emph{exists}. This no-longer requires~$f$, and we obtain the!!{sentence} in pure second-order logic\[\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)]]])].\]$\Sat{M}{\fn{Inf}}$ iff $\Domain{M}$ is infinite.  We can then define$\fn{Fin} \ident \lnot \fn{Inf}$; $\Sat{M}{\fn{Fin}}$ iff $\Domain{M}$is finite. No single !!{sentence} of pure first-order logic canexpress that the !!{domain} is infinite although an infinite set ofthem can. There is no set of !!{sentence}s of pure first-order logicthat is satisfied in !!a{structure} iff its domain is finite.\begin{prop}$\Sat{M}{\fn{Inf}}$ iff $\Domain{M}$ is infinite.\end{prop}\begin{proof}$\Sat{M}{\fn{Inf}}$ iff  $\Sat{M}{\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]]    \land \lexists[y][\lforall[x][\eq/[y][u(x)]]]}[s]$ for  some~$s$. If it does, $s(u)$ is !!a{injective} function, and some $y  \in \Domain{M}$ is not in the range of~$s(u)$. Conversely, if there  is !!a{injective} $f\colon \Domain{M} \to \Domain{M}$ with $\ran{f}  \neq \Domain{M}$, then $s(u) = f$ is such a variable  assignment.\end{proof}A set $M$ is !!{enumerable} if there is an enumeration\[m_0, m_1, m_2, \dots\]of its !!{element}s (without repetitions but possibly finite).  Such an enumeration existsiff there is !!a{element} $z \in M$ and a function $f\colon M \to M$such that $z$, $f(z)$, $f(f(z))$, \dots, are all the !!{element}s of~$M$. Forif the enumeration exists, $z = m_0$ and $f(m_k) = m_{k+1}$ (or$f(m_k) = m_k$ if $m_k$ is the last !!{element} of the enumeration)are the requisite !!{element} and function. On the other hand, if sucha $z$ and $f$ exist, then $z$, $f(z)$, $f(f(z))$, \dots, is anenumeration of~$M$, and $M$ is !!{enumerable}.  We can express theexistence of $z$ and~$f$ in second-order logic to produce a!!{sentence} true in !!a{structure} iff the !!{structure} is!!{enumerable}:\[\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)])]]]\]\begin{prop}$\Sat{M}{\fn{Count}}$ iff $\Domain{M}$ is !!{enumerable}.\end{prop}\begin{proof}Suppose $\Domain{M}$ is !!{enumerable}, and let $m_0$, $m_1$, \dots, be anenumeration. By removing repetitions we can guarantee that no $m_k$appears twice. Define $f(m_k) = m_{k+1}$ and let $s(z) = m_0$ and$s(u) = f$. We show that\[\Sat{M}{\lforall[X][((X(z) \land \lforall[x][(X(x) \lif X(u(x)))])    \lif \lforall[x][X(x)])]}[s]\]Suppose $M \subseteq \Domain{M}$ is arbitrary. Suppose further that$\Sat{M}{(X(z) \land \lforall[x][(X(x) \lifX(u(x)))])}[\Subst{s}{M}{X}]$. Then $\Subst{s}{M}{X}(z) \in M$ andwhenever $x \in M$, also $(\Subst{s}{M}{X}(u))(x) \in M$. In otherwords, since $\varAssign{\Subst{s}{M}{X}}{s}{X}$, $m_0 \in M$ and if$x \in M$ then $f(x) \in M$, so $m_0 \in M$, $m_1 = f(m_0) \in M$,$m_2 = f(f(m_0)) \in M$, etc. Thus, $M = \Domain{M}$, and so$\Sat{M}{\lforall[x][X(x)]}[\Subst{s}{M}{X}]$. Since $M \subseteq\Domain{M}$ was arbitrary, we are done:$\Sat{M}{\fn{Count}}$.Now assume that $\Sat{M}{\fn{Count}}$, i.e., \[\Sat{M}{\lforall[X][((X(z) \land \lforall[x][(X(x) \lif X(u(x)))])    \lif \lforall[x][X(x)])]}[s]\]for some~$s$. Let $m = s(z)$ and $f = s(u)$ and consider $M = \{m,f(m), f(f(m)), \dots\}$. $M$ so defined is clearly !!{enumerable}.Then\[\Sat{M}{(X(z) \land \lforall[x][(X(x) \lif X(u(x)))])    \lif \lforall[x][X(x)]}[\Subst{s}{M}{X}]\]by assumption. Also, $\Sat{M}{X(z)}[\Subst{s}{M}{X}]$ since $M \ni m =\Subst{s}{M}{X}(z)$, and also $\Sat{M}{\lforall[x][(X(x) \lifX(u(x)))]}[\Subst{s}{M}{X}]$ since whenever $x \in M$ also $f(x) \inM$. So, since both antecedent and conditional are satisfied, theconsequent must also be: $\Sat{M}{\lforall[x][X(x)]}[\Subst{s}{M}{X}]$. But thatmeans that $M = \Domain{M}$, and so $\Domain{M}$ is !!{enumerable}since $M$ is, by definition.\end{proof}\begin{prob}The !!{sentence} $\fn{Inf} \land \fn{Count}$ is true in all and only!!{denumerable} domains.  Adjust the definition of $\fn{Count}$ sothat it becomes a different !!{sentence} that directly expresses thatthe domain is !!{denumerable}, and prove that it does.\end{prob}\end{document}