<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\documentstyle[11pt,fleqn,amssymbols]{article}
\addtolength{\textwidth}{2cm}
\addtolength{\textheight}{4cm}
\addtolength{\oddsidemargin}{-5mm}
\addtolength{\evensidemargin}{-5mm}
\addtolength{\topmargin}{-2cm}
\addtolength{\parskip}{2mm}
\newcommand{\circum}{\mbox{$\mbox{CIRC}_{\mbox{\small PR}}(T;\overline{P})$}}
\newcommand{\circums}{\mbox{$\mbox{CIRC}_{\mbox{\small SO}}
                                             (T;\overline{P};\overline{S})$}}
\newtheorem{df}{Definition}
\begin{document}
\begin{center}

\begin{center}
{\Large \bf Exercises-3 (Circumscription)\\[12mm]}
\end{center}
\begin{df}[Predicate Circumscription]
\rm  The {\em circumscription schema}
of $P_{1},\ldots ,P_{n}$ in a theory $T$, denoted by
$\mbox{CS}(T;P_{1},\ldots ,P_{n})$, is the second-order
formula
\[
\left[
     T(\Phi_{1},\ldots ,\Phi_{n})\wedge \bigwedge_{i=1}^{n}
     [\Phi_{i}\leq P_{i}]\right]\supset
              \bigwedge_{i=1}^{n} [P_{i}\leq \Phi_{i}]
\]
or, equivalently
\[
\left[
     T(\Phi_{1},\ldots ,\Phi_{n})\wedge \bigwedge_{i=1}^{n}
     [\forall \overline{x}.\;\Phi_{i}(\overline{x})
       \supset P_{i}(\overline{x})]\right]\supset
     \bigwedge_{i=1}^{n}[\forall \overline{x}.\;P_{i}(\overline{x})
       \supset \Phi_{i}(\overline{x})].
\]
Here $\Phi_{1},\ldots ,\Phi_{n}$ are predicate variables with
the same arities as $P_{1},\ldots ,P_{n}$, respectively.
$T(\Phi_{1},\ldots ,\Phi_{n})$ is the sentence obtained from
$T(P_{1},\ldots ,P_{n})$ by replacing all occurrences of
$P_{1},\ldots ,P_{n}$ by $\Phi_{1},\ldots ,\Phi_{n}$, respectively.\\[2mm]
Let $\overline{\mbox{CS}}(T;P_{1},\ldots,P_{n})$ be the set
of all formulas obtainable from $\mbox{CS}(T;P_{1},\ldots ,P_{n})$
by proper substitutions of first-order predicate expressions for
$\Phi_{1},\ldots ,\Phi_{n}$. The {\em predicate circumscription} of
$\overline{P}=(P_{1},\ldots,P_{n})$ in $T$, written
$\mbox{CIRC}_{\mbox{\small PR}}(T;\overline{P})$, is  
$T\cup \overline{\mbox{CS}}(T;P_{1},\ldots,P_{n})$.\\[2mm]
The set of theorems derivable by circumscribing 
$\overline{P}=(P_{1},\ldots,P_{n})$ in $T$ is identified with
the set of theorems classically entailed by 
$\mbox{CIRC}_{\mbox{\small PR}}(T;\overline{P})$.\hspace{3mm} $\blacksquare$
\end{df}

\begin{df}[Second-Order Circumscription] 
\rm Let $\overline{P}$ be a tuple of
distinct predicate constants, let $\overline{S}$ be a tuple of
distinct function and/or predicate constants disjoint with
$\overline{P}$, and suppose that $T(\overline{P},\overline{S})$ is a
first- or second-order theory. The {\em second-order circumscription
of} $\overline{P}$ in $T$ {\em with variable} $\overline{S}$,
written $\mbox{CIRC}_{\mbox{\small SO}}(T;\overline{P};\overline{S})$,
is the sentence

\[
 T(\overline{P},\overline{S})\wedge\forall \overline{\Phi}
 \overline{\Psi}\;
    \neg [T(\overline{\Phi},\overline{\Psi})\wedge
    \overline{\Phi} &lt; \overline{P}]
\]
where $\overline{\Phi}$ and $\overline{\Psi}$ are tuples
of variables similar to $\overline{P}$ and $\overline{S}$, respectively.\\[3mm]
$\circums$ can be rewritten as

\[
T(\overline{P},\overline{S})\wedge
  \forall \overline{\Phi}
 \overline{\Psi}\;
  \left(\rule[-1mm]{0mm}{5mm}
      T(\overline{\Phi},\overline{\Psi})\wedge (\overline{\Phi}\leq
     \overline{P})\supset (\overline{P}
    \leq\overline{\Phi})\right)
\]
which, in turn, is an abbreviation for

\[
  T(\overline{P},\overline{S})\wedge\forall \overline{\Phi}
 \overline{\Psi}
 \left[\left(T(\overline{\Phi},\overline{\Psi})\wedge
  \bigwedge_{i=1}^{n}[\forall \overline{x}.\;\Phi_{i}(\overline{x})
  \supset P_{i}(\overline{x})]\right)\right.\supset
 \left.
  \bigwedge_{i=1}^{n}[\forall \overline{x}.\;P_{i}(\overline{x})
  \supset \Phi_{i}(\overline{x})]\right].
\]

A formula $A$ is said to be a {\em consequence} of second-order
circumscription of $\overline{P}$ in $T$ with {\em variable} $\overline{S}$
iff $\circums\models A$. \hspace{3mm}$\blacksquare$
\end{df}
\pagebreak

\begin{enumerate}
\addtolength{\itemsep}{5mm}
\item Let $T=\{Block(a)\vee Block(b)\}$. \hspace{3mm}$\overline{P}=(Block)$. 
        \\[4mm]
      Show that $\circum\models \forall x.\;[Block(x)\supset x=a]\vee
                \forall x.\;[Block(x)\supset x=b]$.
\item Let $T=\{Nat(0)\wedge\forall x[Nat(x)\supset
               Nat(succ(x)]\}$.\\[3mm]
      Show that using predicate circumscription, with second-order
      substitutions, it is possible to obtain from $T$ the usual
      axiom schema of induction, i.e. the formula
      \[\left[\rule[-1mm]{0mm}{6mm}
      \Psi (0)\wedge\forall x[\Psi (x)\wedge Nat(x)\supset\Psi (succ(x))]\right]
      \supset\forall x[Nat(x)\supset\Psi (x)].
      \]
\item Let $T$ consist of:
      \begin{enumerate}
      \item[] $Bird(Tweety)$
      \item[] $\forall x.\;Penguin(x)\supset Bird(x)\wedge\neg Flies(x)$
      \item[] $\forall x.\;Bird(x)\wedge\neg Ab(x)\supset Flies(x)$.
      \end{enumerate}
      Show that using second-order circumscription, it is possible
      to infer
      \[
       Flies(Tweety)\wedge\forall x\neg Penguin(x)
      \]
      from $T$. 
 \item Assume that the following facts are true:
      \begin{enumerate}
      \item[] A person normally lives in the same city as his wife.
      \item[] Bill's wife lives in Vancouver.
      \end{enumerate}
      This can be represented by the theory $T$: 
      \begin{enumerate}
      \item[] $\forall x.\;\neg Ab(x)\supset city(x)=city(wife(x))$
      \item[] $city(wife(Bill))=Vancouver$.
      \end{enumerate}
      Show that using second-order circumscription, it is possible to
      infer
      \[
       city(Bill)=Vancouver
      \]
       from $T$.
\item Let $T=\{P(a)\wedge P(b)\wedge Q(b)\wedge [Q(a)\supset P(c)]\}$.\\[4mm]
      Show that using second-order circumscription, with $P$ minimized and
      $a,c$ allowed to vary, it is possible to derive $(a=b)\wedge 
      Q(a)\wedge P(c)$. 
\end{enumerate}
\pagebreak
\begin{center}
{\Large \bf Solutions\\[10mm]}
\end{center}
\begin{enumerate}
\item $T=\{Block(a)\vee Block(b)\}$. \hspace{3mm}$\overline{P}=(Block)$.
\item[]  CS($T$;$Block$)=$\left[\rule[-1mm]{0mm}{5mm}
         [\Phi(a)\vee \Phi(b)]\wedge \forall x[\Phi(x)\supset Block(x)]
         \right]\supset \forall x[Block(x)\supset\Phi(x)].$
\item[] Taking the substitutions
      \[
        \{\Phi\leftarrow \lambda x.x=a\}\mbox{\hspace{3mm}and\hspace{3mm}}
        \{\Phi\leftarrow \lambda x.x=b\}
      \]
      we successively obtain
      \[
        \left[\rule[-1mm]{0mm}{5mm}
       [a=a\vee a=b] \wedge\forall x[x=a\supset Block(x)]\right]
       \supset\forall x[Block(x)\supset x=a]
      \]
      which simplifies to
      \[
       \mbox{(1)\hspace{3mm}}Block(a)\supset\forall x[Block(x)\supset x=a]
      \]
      and
      \[
        \left[\rule[-1mm]{0mm}{5mm}
       [b=a\vee b=b] \wedge\forall x[x=b\supset Block(x)]\right]
       \supset\forall x[Block(x)\supset x=b]
      \]
       which simplifies to
      \[
       \mbox{(2)\hspace{3mm}}Block(b)\supset\forall x[Block(x)\supset x=b].
      \] 
       (1), (2) and $T$ yield
      \[
       \circum\models \forall x.\;[Block(x)\supset x=a]\vee
                \forall x.\;[Block(x)\supset x=b]. 
      \]
\vspace*{4mm}        
\item $T=\{Nat(0)\wedge\forall x[Nat(x)\supset
               Nat(succ(x))]\}$. \hspace{3mm} $\overline{P}$=($Nat$).
\item[] 
        \[
         \mbox{CS($T$,$\overline{P}$)=}
         \left[\rule[-1mm]{0mm}{5mm}\Phi (0)\wedge\forall x
         [\Phi(x)\supset \Phi (succ(x))]\wedge\forall x 
         [\Phi(x)\supset Nat(x)]\right]\supset
        \]
        \vspace*{-4mm}
        \[ \mbox{\hspace{80mm}}
         \supset\forall x [Nat(x)\supset \Phi(x)].
        \]
        Applying the substitution $\{\Phi\leftarrow \lambda x[\Psi(x)\wedge
        Nat(x)]\}$, we obtain
        \[\left[\rule[-1mm]{0mm}{5mm}
         [\Psi (0)\wedge Nat(0)]\wedge\forall x[\Psi(x)\wedge Nat(x)
          \supset\Psi (succ(x))\wedge Nat(succ(x))]\right.\wedge
         \]
        \vspace*{-6mm}
         \[ 
        \mbox{\hspace{5mm}}\left.\rule[-1mm]{0mm}{5mm}
        \wedge\forall x[\Psi (x)\wedge Nat(x)\supset Nat(x)]\right]
        \supset\forall x[Nat(x)\supset \Psi (x)\wedge Nat(x)]
         \]
        which simplifies to
         \[\left[\rule[-1mm]{0mm}{5mm}
         [\Psi (0)\wedge Nat(0)]\wedge\forall x[\Psi(x)\wedge Nat(x)
          \supset\Psi (succ(x))\wedge Nat(succ(x))]\right]\supset
         \]
         \vspace{-5mm}
         \[\mbox{\hspace{80mm}}
          \supset\forall x[Nat(x)\supset \Psi (x)].
         \]
         This, together with $T$, yield
         \[ \circum\models\left[\rule[-1mm]{0mm}{5mm}
      \Psi (0)\wedge\forall x[\Psi (x)\wedge Nat(x)\supset\Psi (succ(x))]
         \right]\supset
         \]
         \vspace{-4mm}
       \[ \mbox{\hspace{80mm}}
       \supset\forall x[Nat(x)\supset\Psi (x)].
      \]
\item  $T$ consists of:
       \begin{enumerate}
       \item[] $Bird(Tweety)$
       \item[] $\forall x.\;Penguin(x)\supset Bird(x)\wedge\neg Flies(x)$
       \item[] $\forall x.\;Bird(x)\wedge\neg Ab(x)\supset Flies(x)$.
      \end{enumerate}
      We minimize $\overline{P}$=($Ab$) with $\overline{S}$=
      ($Flies,Penguin$) allowed to vary.\\
\item[] \circums = \\[6mm]
        $
        \mbox{\hspace{10mm}}
        T(\overline{P},\overline{S})
        \wedge\forall\Phi\Psi_{1}\Psi_{2}\left\{\rule[-1mm]{0mm}{6mm}\right.
        \left[\rule[-1mm]{0mm}{5mm}\right.        
        [\forall x.\;\Psi_{2}(x)\supset Bird(x)\wedge\neg\Psi_{1}(x)]\wedge
        $\\
        $
        \mbox{\hspace{50mm}}
         \wedge [\forall x.\;Bird(x)\wedge\neg\Phi (x)\supset\Psi_{1}(x)]\wedge
        $\\
        $
         \mbox{\hspace{50mm}}
         \left.\rule[-1mm]{0mm}{5mm}\wedge [\forall x.\;\Phi(x)\supset Ab(x)]
         \right]\supset [\forall x.\;Ab(x)\supset \Phi(x)]\left.
         \rule[-1mm]{0mm}{6mm}\right\}. 
        $
\item[] Applying the substitution $\{\Phi\leftarrow\lambda x. False,\;
        \Psi_{1}\leftarrow\lambda x.True,\;\Psi_{2}\leftarrow
        \lambda x.\;False\}$, we get\\[6mm]
        $
        \mbox{\hspace{10mm}}
        T(\overline{P},\overline{S})\wedge\left\{\rule[-1mm]{0mm}{6mm}\right.
        \left[\rule[-1mm]{0mm}{5mm}\right.        
        [\forall x.\;False\supset Bird(x)\wedge False]\wedge
        $\\
        $
        \mbox{\hspace{44mm}}
         \wedge [\forall x.\;Bird(x)\wedge True\supset True]\wedge
        $\\
        $
         \mbox{\hspace{44mm}}
         \left.\rule[-1mm]{0mm}{5mm}\wedge [\forall x.\;False\supset Ab(x)]
         \right]\supset [\forall x.\;Ab(x)\supset False]\left.
         \rule[-1mm]{0mm}{6mm}\right\}
        $
\item[] which simplifies to
        \[
        T(\overline{P},\overline{S})\wedge\forall x\;\neg Ab(x).
        \]
        From this, we immediately obtain
        \[
         \circums\models Flies(Tweety)\wedge\forall x\neg Pinguin(x).
        \]
\item[] Taking $Penguin$ as varying predicate may seem unreasonable.
        However, if we restrict  $\overline{S}$ to $Flies$,
        all we can be able to infer is that birds fly, except penguins.
        In particular, since we have no information that Tweety is
        not a penguin, we shall not be able to infer that Tweety
        flies.\\
      
\item $T=\{[\forall x.\;\neg Ab(x)\supset city(x)=city(wife(x))]\wedge
           city(wife(Bill))=Vancouver\}$.\\[3mm]
          We minimize $\overline{P}=(Ab)$ with 
          $\overline{S}=(city)$ allowed to vary.\\
\item[] \circums = \\[6mm]
        $
        \mbox{\hspace{10mm}}
        T(\overline{P},\overline{S})
        \wedge\forall\Phi\psi\left\{\rule[-1mm]{0mm}{6mm}\right.
        \left[\rule[-1mm]{0mm}{5mm}\right.        
        [\forall x.\;\neg \Phi(x)\supset \psi(x)=\psi(wife(x))]\wedge
        $\\
        $
        \mbox{\hspace{15mm}}
         \wedge [\psi(wife(Bill))=Vancouver]\wedge
         \left.\rule[-1mm]{0mm}{5mm}
         [\forall x.\;\Phi(x)\supset Ab(x)]\right]\supset
        $\\
        $
         \mbox{\hspace{80mm}}
         \supset [\forall x.\;Ab(x)\supset \Phi(x)]\left.
         \rule[-1mm]{0mm}{6mm}\right\}. 
        $
\item[] Taking the substitution\footnote{Observe that we substitute here a
        predicate expression for a predicate variable and a function
        expression for a function variable.} 
       $\{\Phi\leftarrow\lambda x.\;False,\;
        \psi\leftarrow\lambda x.\;Vancouver\}$, we get\\[5mm]
       $
        \mbox{\hspace{10mm}}
        T(\overline{P},\overline{S})
        \wedge\left\{\rule[-1mm]{0mm}{6mm}\right.
        \left[\rule[-1mm]{0mm}{5mm}\right.        
        [\forall x.\;True\supset Vancouver=Vancouver]\wedge
        $\\
        $
        \mbox{\hspace{15mm}}
         \wedge [Vancouver=Vancouver]\wedge
         \left.\rule[-1mm]{0mm}{5mm}
         [\forall x.\;False\supset Ab(x)]\right]\supset
        $\\
        $
         \mbox{\hspace{80mm}}
         \supset [\forall x.\;Ab(x)\supset False]\left.
         \rule[-1mm]{0mm}{6mm}\right\}
        $            
\item[] which simplifies to
        \[
        T(\overline{P},\overline{S})\wedge\forall x\;\neg Ab(x).
        \]
        From this, we immediately obtain
        \[
         \circums\models city(Bill)=Vancouver.
        \]
\vspace*{3mm}
\item   $T=\{P(a)\wedge P(b)\wedge Q(b)\wedge [Q(a)\supset P(c)]\}$.
        $\overline{P}$=($P$); $\overline{S}$=($a,c$). \\
\item[] \circums = \\[5mm]
        $
        \mbox{\hspace{10mm}}
        T(\overline{P},\overline{S})
        \wedge\forall\Phi\forall yz\left\{\rule[-1mm]{0mm}{6mm}\right.
        \left[\rule[-1mm]{0mm}{5mm}\right.        
        [\Phi(y)\wedge \Phi(b)\wedge Q(b)]\wedge
        $\\
        $
        \mbox{\hspace{15mm}}
         \wedge [Q(y)\supset \Phi(z)]\wedge
         \left.\rule[-1mm]{0mm}{5mm}
         [\forall x.\;\Phi(x)\supset P(x)]\right]\supset
        $\\
        $
         \mbox{\hspace{80mm}}
         \supset [\forall x.\;P(x)\supset \Phi(x)]\left.
         \rule[-1mm]{0mm}{6mm}\right\}. 
        $
\item[] Taking the substitution $\{\Phi\leftarrow\lambda x.\;x=b,\;
        y\leftarrow\lambda x.\;b,\; z\leftarrow\lambda x.\;b\}$
        and simplifying, we obtain
        \[
         \circums\models \forall x.\;P(x)\supset x=b
        \]
         from which we get
        \[
         \circums\models (a=b)\wedge Q(a)\wedge P(c).
        \]
        \vspace*{3mm}
\item[] {\bf NOTE:} If function constants are allowed to vary, then
        second-order circumscription may serve to obtain
        \begin{itemize}
        \item new ground equality statements
        \item positive instances of circumscribed predicates
        \item new instances of non-variable predicates.
        \end{itemize}
        These types of conclusions cannot be obtained by using
        second-order circumscription if only predicates are allowed
        to vary.

\end{enumerate}
\end{document}

</pre></body></html>