For historical reference.

# Tutorial I (Tue 21 Jan 2014)

## The questions

1. Assume $x:\mathbb N$. Express the predicate “$x$ is divisible by $7$” (usually written $7|x$).
2. Assume $y:\mathbb N$. Express the predicate “$x$ is divisible by $y$” (usually written $y|x$).
3. Write a sets expression for the divisors of $x$.
4. Express the predicate “$y:\mathbb N$ is the integer square root of $x$” (this is $\lfloor \sqrt{x} \rfloor$; the greatest integer whose square is not greater than $x$).
5. Assume a function $f:\mathbb N\rightarrow\mathbb Z$ (modelling velocity over time, or voltage at a wire over time, or signal received from a satellite over time, and so on). Express the predicate “$f(x)$ is strictly positive for some $x$”.
6. Express the predicate “$f(x)$ is strictly positive for infinitely many $x$”.

OK, so students who write $x\ \mathit{div}\ 7 = 0$ get zero marks. This course isn’t about downloading an off-the-shelf library function that does the question for you. It’s not that kind of course.
So think about when $x$ is divisible by $7$. That’s when there exists some $z:\mathbb N$ such that $x=7*z$. Right? So write that in predicate logic:
$$\exists z:\mathbb N\bullet x=7*z .$$
That’s it; you’re done!
Clearly the examiner wants you to build on your answer to the previous question. Here we go:
$$\exists z:\mathbb N\bullet x=y*z .$$
A useful sanity check is to look at the free variables. Question 1 has free variable $x$, and its answer $\exists z:\mathbb N\bullet x=7*z$ also has free variable $x$. Question 2 has free variables $x$ and $y$ and so does the answer.
If you answer a question with free variables $foo$ and $bar$ with an answer that has free variables other than $foo$ and $bar$, then something’s probably gone wrong.
Remember the notation for sets comprehension. The set of divisors of $x$ is the set of $y$ such that $y|x$. It’s OK to write $y|x$ now because we defined it in a previous question—-it’s like a subroutine or function call for us now:
$$\{ y:\mathbb N \mid y|x\} .$$
Again, check the free variables. Something that looks like this $\{x:\mathbb N \mid y|x \}$ or like this $\{y:\mathbb N \mid \exists x:\mathbb N\bullet y|x\}$ is guaranteed wrong, because neither possibility has $x$ free.
Anything that looks like this is not just wrong, but invalid syntax: $\{\exists y:\mathbb N \mid \dots\}$. Do not follow a $\{$ with a $\forall$ or an $\exists$. Students are expected to generate syntactically valid and correct Z syntax.
You’ve just got to think about this one. The integer square root of $x$ is the greatest number whose square is less than $x$. The free variables of the question are $y$ and $x$. So I suggest this:
$$y*y\leq x\ \land\ x<(y+1)*(y+1) .$$
Easy. There exists an $x:\mathbb N$ such that $f(x)>0$. Or in symbols:
$$\exists x:\mathbb N\bullet f(x)>0 .$$
I used animated collapse to hide the answers. This is a great library but it requires me to give each element a unique name (“Answer 1”, “Answer 2”, …). I would prefer not to have to do this; so if you know a library that allows me to attach a hide/unhide action to a div without giving it a unique ID (without naming it), then let me know.