\documentclass[12pt]{article}

\usepackage{proof}
\usepackage{fullpage}

\newcommand\os[1] {$\mit{#1}$}
%\newcommand\os[1]{#1}
 
\newcommand\imp\Rightarrow

%\input{qobitree}
\pagestyle{empty}

\begin{document}

\begin{center}
\large 
%\vspace*{-1.5cm}
Harvey Mudd College\\
Computer Science \os{80}\\
Logic for Computer Science\\
Fall Semester \os{2001}\\[16pt]

Assignment \#6 -- Predicate Logic: Syntax, Semantics and Encoding\\
\large
Due { \os{11}:\os{00}am}, Wednesday November \os{21}, \os{2001}
\end{center}

\vspace{0.25in}


\newcommand{\G}{\Gamma}
\newcommand{\D}{\Delta}
\newcommand{\lra}{\longrightarrow}

\begin{enumerate}

\item Questions of Syntax:
\begin{enumerate}
\item Give the set of free variables and and the set of bound variables of the 
formula:
$$\forall z(p(x) \land \forall x[\exists y \{q(y,f(z)) \imp r(g(g(w,x),f(y)))\}])$$

\item Give the result of substituting $f(y)$ for the variable $x$ in that formula.

\item Give the result of substituting $f(y)$ for the variable $w$ in the original
formula (not in the answer from the last substitution).
\end{enumerate}

\item Questions of Semantics:

For each of the following formulas (or, sets of formulas)
show that they are both satisfiable and falsifiable, by giving interpretations for
each case. Make sure you provide an assignment for quantified variables as well,
where that appears necessary. Explanatory prose may also be helpful. For example: 
\begin{itemize}
\item $\forall x(\exists y(l(y,x)))$
\begin{description}
\item{Satisfiable:} Let the domain be the integers, and interpret $l$ as the
less-than relation. Clearly for every integer there is an integer less than it.

(Alternately, let the domain be any non-empty set, and interpret $l$ as any
equivalence relation on that set. Since an equivalence relation is reflexive, then
each element is at least related to itself, if nothing else.)
\item{Falsifiable:} Let the domain be the non-negative integers and interpret $l$ as
the less than relation. Then if $x$ is 0, there is no smaller natural number.
\end{description}
\end{itemize}


\begin{enumerate}
\item $\exists x (\forall y (p(x,y)))$
\item $\forall x (p(x) \imp q(x))$
\item $(q(a) \land q(b) \land p(a)) \imp \forall x (p(x) \imp q(x))$
\item $(jar(j) \land heated(j) \land bug(b) \land in(b,j)) \imp dead(b)$
\item $(\forall x(plus(x,0) \doteq x \land  \\ \forall x(\forall y(
plus(s(x),y)\doteq s(plus(x,y))))) \imp \\
\hspace*{1cm}plus(s(s(0)),s(s(0)))\doteq s(s(s(s(0))))$
\end{enumerate}


\item Questions of Encoding I:

Given the predicates defined in class for the beer-drinkers database example,
provide existential formulas equivalent to the following queries:
\begin{enumerate}
\item What drinkers drink at least one beer served by the Hi-brow?

\item What drinkers drink all the beers served by the Hi-brow?

\item Who likes all the beers Hodas likes?

\item What bars does Hodas go to that serve all the beers he likes for less than
\$3.00?

\item What bars are frequented by the drinkers who like all the beers that Hodas
likes?
\end{enumerate}

\item Questions of Encoding II:

Give first order encodings of each of the following facts. You should note that
being a boletus, or fungus, or any particular sort of thing is a property, which is
to say, a predicate. Also, you will need a constant to represent ``this thing''.

\begin{enumerate}
\item ``Every fungus is either a mushroom or a toadstool."

\item ``Every boletus is a fungus."

\item ``Toadstools are poisonous, as are peach pits."

\item ``A boletus is not a mushroom."

\item ``This thing is a boletus."
\end{enumerate}

\end{enumerate}
\end{document}
