\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=black,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}

\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\fa}[1]{\forall #1. \, }
\newcommand{\ex}[1]{\exists #1. \, }
\newcommand{\mdl}[1]{\mathfrak{#1}}

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 9}

\medskip

due 6pm Thursday, November 11, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\subsection*{Problem 1 (7 points)}

Fill in the proofs of the propositional formulas found in {\tt assignment9.lean}.


\subsection*{Problem 2 (2 points)}

Let $\mathcal A$ be the structure consisting of ``all objects on
the planet Earth'' with relations {\em Cow(x)}, {\em
EatsGrass(x)}, {\em Car(x)}, etc. Give reasonable formalizations of
the following sentences:
\begin{enumerate}
\item All cows eat grass.
\item There is a car that is blue and old.
\item No car is not pink.
\item All cars that are old must be inspected annually.
\end{enumerate}


\subsection*{Problem 3 (2 points)}

Consider a first-order language, with relation
symbols $<$ and $=$. The intended interpretation is the natural
numbers, with the usual less-than relation and equality. Formalize the following
statements:
\begin{enumerate}
\item 0 is the smallest number.
\item There is a smallest number.
\item There is no largest number.
\item Every number has an immediate successor. (In other words, for
every number, there is another one that is the ``next largest.'')
\end{enumerate}

\subsection*{Problem 4 (3 points)}

Consider a language designed to talk about numbers, with symbols $+$, $\times$, and $<$.
Consider these four interpretations of the language:
\begin{enumerate}
  \item $\mdl N = (\mathbb{N}, +, \times, <)$
  \item $\mdl Z = (\mathbb{Z}, +, \times, <)$
  \item $\mdl Q = (\mathbb{Q}, +, \times, <)$
  \item $\mdl R = (\mathbb{R}, +, \times, <)$
\end{enumerate}
In other words, we consider the natural numbers, the integers, the rational numbers,
and the real numbers, all with the usual interpretations of the symbols.

\begin{enumerate}
  \item Write down a sentence in the language that is satisfied by $\mdl Z$ but not $\mdl N$.
  \item Write down a sentence in the language that is satisfied by $\mdl Q$ but not $\mdl Z$.
  \item Write down a sentence in the language that is satisfied by $\mdl R$ but not $\mdl Q$.
  (Hint: This is tricky. One option is to say that every sufficiently large number has a square root.)
\end{enumerate}


\subsection*{Problem 5 (2 points)}

Remember that substitution $t[s/x]$ for terms is defined recursively,
and there is a similar definition of substitution $A[s/x]$ for formulas.
As we did for propositional logic, we can prove the following, using
the semantic definitions in Section 10.3:
\[
\mdl M \models_\sigma A[t/x] \quad \text{if and only iff} \quad
\mdl M \models_{\sigma[x \mapsto \tval{t}_{\mdl M, \sigma}]} A.
\]
Use this fact (you don't have to prove it), and the semantic definitions,
to show that for every formula $A$,
every model $\mdl M$, every term $t$, and every assignment $\sigma$, we have
\[
\mdl M \models_\sigma (\fa x A) \to A[t/x].
\]

\end{document}