This is a list of recommended exercises (from the course book), and is
precisely those which will be covered during the exercises sessions on
fridays. It will be completed as the course goes along, with
occasional commentary in some unclear cases.

1.1:
2d)
2g)

1.2:
1d)
1g)
1m)
1q)
1u)
1w)
3a)
3b)
3c)
3f)
3g)
3l)
3o)

1.4:
12d)

1.5:
3b) This exercise was unclear to a number of students. The task is to show
that if formulas are formed using only the connectives &, OR and -> (that
is, without NOT nor falsehood), then the resulting set of formulas will
not be able to express everything that can be expressed by propositional
logic. In other words, we need to find a formula that is in propositional
logic, but which cannot be modeled using only the connectives &, OR and ->.
The formula P & NOT P is such a formula. It definetely belongs to
propositional logic, and its truth table (namely F:s in every row) cannot
be achieved with any formula with only the connectives &, OR and ->.
To see that in fact no formula with only the connectives &, OR and -> can
have a truth table with only F:s, consider any such formula and the case
when all its atoms are T. Then this formula must have a T for this row
because X & Y, X OR Y, X -> Y are all T if X and Y are T. (If one is
picky this should be proved by induction.) Now, since any formula
formed using only the connectives &, OR and -> must have a T in at least
one row of its truth table, thers is no possibility to express P & NOT P.

3c) The exercise session leader may have been misleading during the
discussion of this exercise in class, so here is a clarification. {NOT, <->}
is not adequate.

One way to prove this is to consider the all the
possibilities for the shortest kinds of formulas, i.e., the cases NOT A,
A <-> A, NOT A <-> A, A <-> B, NOT A <-> B, (A <-> B) <-> B and (A <-> B) <->
NOT B, (NOT A <-> B) <-> B and check that these no do not express neither OR,
AND or ->. Then show by induction that more complex formulas cannot express
neither OR, AND or -> either.

Another, slightly smarter, proof was suggested by a student. Any
formula with two atoms, formed using only NOT and <->, must have an
even number of T:s in its truth table. This is easily verified with
the shortest kinds of formulas, and from there it is clear it holds
also for composite formulas. If there is no formula with two atoms
which has T in 1 or 3 rows of its truth table, then none of OR, AND,
-> can be expressed.

7c)

2.1:
1a)
2a)

2.2:
6

2.3:
1a)
Show: (y = 0) & (y = x) |- 0 = x
1. y = 0   PREM
2. y = x   PREM
NO: 3. 0 = x   =e 1,2 So F is z = x and do F[t2/z] 

3. y = y   =i
4. 0 = y   =e 1,3 where F is x = y, t1 is y and t2 is 0  
5. 0 = x   =e 2,4 where F is 0 = x, t1 is y and t2 is x

1b)
Show: t1 = t2 |- (t + t2) = (t + t1)
1. t1 = t2               PREM
2. (t + t1) = (t + t1)   =i
3. (t + t2) = (t + t1)   =e 1,2 where F is (t + x) = (t + t1), t1 is t1 and t2 is t2

t is free for x in F = no variable in t "wrongly" gets bound if one replaces all free x:s in F with t.

6a)
Show: AxP(x) |- AyP(y)
1. AxP(x)      PREM
2. y0 P(y0)  Ax e 1
3. AyP(y)      Ay i 2

6b)
Show: Ax(P(x)->Q(x)) |- (Ax-Q(x)) -> (Ax-P(x))
1. Ax(P(x)->Q(x))          PREM
2. Ax-Q(x)                 ASSUMP
3. x0 -Q(x0)
4.    P(x0)->Q(x0)    
5.    -P(x0)               MTT
6.    Ax-P(x0)             Ax i 3-5
7. (Ax-Q(x)) -> (Ax-P(x))  ->i 2-6

6c)
Show: Ax(P(x)->-Q(x)) |- -(Ex(P(x) & Q(x))

7b)
Show: ExEyF(x,y) |- EuEvF(u,v)

Please note the tempting but illegal use of Ee on p. 114 (bottom) in
the book!

9b)
Show: S -> ExQ(x) |- Ex(S -> Q(x))

9c)
Show: ExP(x) -> S |- Ax(P(x) -> S)
1. ExP(x) -> S               PREM
2.   -Ax(P(x) -> S)          ASSUME
3.     S                     ASSUME
4.       P(x_0)              ASSUME
5.       S                   REPEAT 3
6.     P(x_0) -> S           ->I 4-5
7.     Ax(P(x) -> S)         Axi 6
8.     _|_                   -e 2, 7
9.   -S                      -i 3-8
10.  -ExP(x)                 MT 1, 9
11.  Ax-P(x)                 Theorem 2.13 on row 10 in book p. 117
12.      P(y_0)              ASSUME
13.     -P(y_0)              Axe 11
14.     _|_                  -e 12, 13
15.  P(y_0) -> S             ->I 12-14
16.  Ax(P(x) -> S)           Axi 15
17.  _|_                     -e 2, 16
18.Ax(P(x) -> S)             PBC 2-17

Some comments are in order.

Why do have to assume row 2? Couldn't we just do roughly the same
without it? No, we need row 2 to get the contradictions in row 8 and
17. Without it we'd just be stuck with an unstricken S
assumption. It's a bit like the derivation of |- P OR -P where we
first assume -(P OR -P) then try P in order to get -P and get another
contradiction. [In fact, and this is perhaps easier, it is possible to
do 9c by starting from the formula S OR -S.]

What goes on in row 3-6 is just mechanics for the fact that if we have S,
then anything implies S.

In row 6 it seems that x_0 "occurred outside its box". Yes, but this
is fine since we are not doing an existential elimination. In
existential elimination, this is forbidden, but otherwise variables
are names for arbitrary values, like when you do informal proofs ("let
n be .."). If you think about it, getting 7 from row 3 does make
sense intuitively, you just have to master the mechanics of our
specific derivation system; To get quantified statement with "a
complex inside", we do what we do in row 3-7, namely we place
arbitrary variables in the right place, build up the complex formula
with any free variables breathing during the process, and finally
enclose with the quantifier.

13d)
Show: AxAyAz(S(x,y) & S(y,z) -> S(x,z)), Ax-S(x,x) |- AxAy(S(x,y) -> -S(y,x))

Here's a less formal solution:
Assume -AxAy(S(x,y) -> -S(y,x)) for future use of PBC.
Assume -S(t1,t2). Under this S(t1,t2) implies anything, so
in particular S(t1,t2) -> -S(t2,t1). We introduce universal quantifiers
around that formula to get a contradiction with -AxAy(S(x,y) -> -S(y,x)).
With this contradiction we can reject the assumption -S(t1,t2) and
get S(t1,t2) by PBC. Next, assume S(t2,t1). Using the AxAyAz premise on
these two we get S(t1,t1) which is contradicted by the other premise
Ax-S(x,x). So we can reject S(t2,t1) getting -S(t2,t1). Now, S(t1,t2)
-> -S(t2,t1) (actually anything imples -S(t2,t1)). Introduce universal
quantifiers and get AxAy(S(x,y) -> -S(y,x)) which contradicts the first
premise. PBC yields the desired derivation.


2.4:
2)
3)
11a)
11c)

12e)
Show or give countermodel: AxAy(S(x,y) -> (Ez(S(x,z) & S(z,y))))

12f)
Show or give countermodel: (AxAy(S(x,y) -> (x=y))) -> Az-S(z,z)

12h)
Show or give countermodel: AxAy((P(x) -> P(y)) & (P(y) -> P(x)))

12k)
Show or give countermodel: (AxEy(P(x) -> Q(y))) -> (EyAx(P(x) -> Q(y)))
[Difficult]

This formula is in fact valid. Informally, to see why, consider the
(AxEy(P(x) -> Q(y))) part, which can be true in two kinds of ways.  a]
P(x) is false for all x, and then Q "doesn't matter". In this case,
(EyAx(P(x) -> Q(y))) is true as well. b] There are one or more x for
which P(x) is true, and thus one or more y for which Q(y) is true.
Knowing that there is at least one such y, is in fact enough to
guarantee that (EyAx(P(x) -> Q(y))) is true as well. Because even if
AxEy says that there can be different y for different x, which is not
the case for EyAx, the only usage of y, namely Q(y), doesn't "depend" on
x so it cannot change its behaviour depending on which x is under
consideration.

Thierry's exercise 1) Try to look systematically for a countermodel
for the following (and use this to decide if th entailment is correct or not):

a) Ex(P(x) & -M(x)), Ey(M(y) & -S(y)) |=
   Ez(P(z) & -S(z))

b) Ey(S(y) & M(y)), Ax(P(x) -> -M(x)) |=
   Ez(S(z) & -P(z))

Thierry's exercise 2)

Show that the following formula has no finite model
Ax-R(x,x) &
AxAyAz(R(x,y) & R(y,z) -> R(x,z)) &
AxEyR(x,y) 

2.5 
1c) Show that the validity of the following sequent cannot be proved:
(AxP(x)) -> L |- Ax(P(x) -> L

1e)
ExP(x), EyQ(y) |- Ez(P(z) & Q(z))


3.2
2a) G a
i) q3,q4,q3,q4,...
ii) No, not all paths pi from q3 have pi |= G a. E.g. paths than begin q3, q2
2b) a U b
i) q3,q2,q2,q2,... (i=2)
ii) Yes, all the paths q3,q1,q2,.. q3,q2,... and q3,q4,... hold.
2c) a U X (a & -b)
i) q3,q4,q3,... (i=2)
ii) Not in q3, q2, q2, q2, ...
2d) X -b & G (-a OR -b)
i) q3, q1, q2, q2, ...
ii) Not in q3, q4, ...
2e) X (a & b) & F (-a & -b)
i) q3, q4, q3, q1, ..
ii) Not in q3, q1, ...

3.
first & second: immediate

third:
if phi is true always, then phi OR psi is true always.
if phi is true up to a point i-1 and then at i psi is true, then
phi OR psi is true and psi is true up to and including i (also works if i = 1)
if phi OR psi true always it means that either it is phi that is true always or
there is a "hand-over" to of the truth burden to psi at some point i.
if phi OR psi is true up to a point i at which it and psi alone is true,
then phi has to be true to i-1 and then at i psi is true, or the "hand-over"
could be even earlier.

fourth:
if psi is true always then it's clear both ways.
if there is a release at i, then psi is true to i-1 and at i phi & psi is true
if psi is true up to i-1 (i=1 also) and phi & psi is true at i, then
psi is true up to and including i and phi is true at i.

4. Compose first and third in exercise 3.

3.3
1a) For all initial states, for all paths it is true that for all
i (of any path) if we are in a state where req holds, then there
is an later (than) i point in the path where busy holds.
Why? Check all states (i.e. including the initial states), in those
where req is true, the only possible next state is one where busy
holds. [All paths must follow the state transitions charts so all
paths are thus covered]. 
1b) -(req U -busy) means either busy always holds or -busy occurs
only at those i where req is not true at i-1. In other words, if
-busy holds at all, it is when req is not true in the previous state
[also, -busy cannot hold at the start].
Now, is it true for all initial states and for all paths that
"if -busy holds at all, it is when req is not true in the previous state"?
No, if we start in the req+ready state (upper left), then -busy aka
ready holds immediately, which contradicts -(req U -busy).



3.4
#1 2 3(maybe)
#4
5. Does E[req U -busy] hold in all initial states?
s |= E[req U -busy] means "there is a path beginning in s such that
req U -busy holds on it". For the upper left starting state, any path
satisfies it (immediately). The same goes for the the lower left starting
state.

6b)
ii) F t is a LTL formula. The question is, starting from s_0, is it true
that for all paths from s_0, does t hold somewhere in the future?
No, one path, namely s_0, s_0, ... never comes to a state where t holds.
For s_2 on the other hand, all paths have to go through s_1 immediately,
where t holds, so s_2 |= F t.

vi) EF q is a CTL formula. It means, "there is a path such that F q holds
on it". It is true for s_0 as the starting state, given the path that begins
with going to s_3. Also true for s_2 as the starting state.

vii) EG r is a CTL formula. It means, "there is a path such that G r holds
on it". It is true for s_0 as the starting state, given the path that stays
only in s_0. Also true for s_2 as the starting state with the path s2,s1,s2,
s1,s2,...

viii) G (r OR q) is a LTL formula. The question is, starting from s_0, is it
true that for all paths from s_0, does (r OR q) all the time? Since
all states satisfy r OR q, G r OR q holds for any paths starting anywhere.

7c) S - [[phi]] = S - {s in S| s|=phi} = {s in S |/= phi} =
{s in S|s |= -phi} = [[-phi]]

8a) AF q
s_0: Yes, all paths begin at s_0 where q holds (so F q for i=1).
s_2: Yes, either of the two beginnings of paths go to states where
q holds.
8b) AG (EF (p OR r))
s_0, s_2: Yes, because in any state (p OR r) is true.
8c) EX (EX r) "there is a path such that in the next state there is a path
where r holds in the next state".
s_0: Yes, the path s0, s1, s1, s1, ....
s_2: Yes, the path s2, s0, s1, s1, ....
8d) AG (AF q) "for all paths and for all path positions i, on all paths
continuing from i, we can find a state where q holds"
s_0: No, take the path s_0, s1, s1, s1, .... For this path it is not so that
for all i (take e.g. i=100 or any i >= 2), that all continuations from i 
we can find a state where q holds. For example, one continuation from
i will be s1, s1, s1, .... which does not contain any state where q
holds.
s_2: Similar to the above, just go to s_0 first.

10a) EF phi and EG phi: Not equivalent. Set phi true in s_0 (and phi false
in s_1). Let there be only the transitions s_0 to s_1 and s_1 to s_1.

10d) AF -phi and -EG phi: Equivalent. If there are no paths where phi
holds throughout all, then for all paths somewhere -phi is true.
If for all paths somewhere -phi is true, then there is not one path
where phi holds throughout.

10g) T and AG phi -> EG phi: Of course they are equivalent (at least if we
require somewhere that there is always one state. If there is one state,
there is always at least one path -- so much is made clear in the definition
on page 178).

3.7
1c) It's not monotone so we can't use the iteration from the empty set
to find one. However, there is no fixpoint anyway. If a subset Y contains
one of {2,5,9} then {2,5,9} - Y does not contain that element. If a
subset Y does not contain of {2,5,9} then {2,5,9} - Y = {2,5,9} which
is not the same as Y by assumption.

1d) G^2 = G^i for all even i. G^2(Y) is {s_0} if Y == s_0 otherwise {s_1}.

3.7 Using the book's algorithm or Thierry's reformulation of it (i.e.
Thierry's algorithm "first" algorithm with Y:s). Label the states of
fig 3.42 s1 to s7 is in boustrofedon order, i.e. s1-s4 on the upper
row from left to right, and s5-s7 from right to left on the lower
row. So, e.g., s5 is the name of the state with a p.

3a) [[EF p]]

Y0 = [[p]] = s5
Y1 = {s5} UNION {s4}
Y2 = {s5,s4} UNION {s3}
Y3 = {s5,s4,s3,s2}
Y4 = {s5,s4,s3,s2,s1}
Y5 = {s5,s4,s3,s2,s1,s6}
Y6 = {s5,s4,s3,s2,s1,s6} = Y5

3b) [[EG q]]

Y0 = [[q]] = {s2,s6,s7}
Y1 = {s2,s6,s7} INTERSECT {s1,s2,s5,s6,s7} = {s2,s6,s7}
Y2 = {s2,s6,s7} INTERSECT {s1,s2,s5,s6,s7} = {s2,s6,s7} = Y1