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