Assignment 2: Some solutions and marking scheme

Problem 1: Prove that |- A \/ B == A \/ ¬B == A . 10 marks (I.e., give a bullet proof that the above lives in the room of theorems. You may use any theorems up through 2.4.10 in your proof.) Well, this is embarrassingly easy.... I will type the Boolean constant "falsum" as "bottom" here (and the other one, "verum", as, maybe, "top"). Pf: A \/ B == A \/ ¬B <==> < ax. (8) > 4 marks A \/ ( B == ¬B ) <==> < ax. (4) > 3 marks A \/ bottom <==> < 2.4.10 > 3 marks A. // There are various correct variants on the above. Some people will begin the proof by writing out the whole wff on line 1, then ax. (8), then ax. (4), then 2.4.10, and finally write down that the result on line 4 of the "stack" of wffs is 2.1.12. That's fine. Give 4 marks, 2 marks, 2 marks, and 2 marks for those four steps in that order. Grader: Please make deductions for various things -- If the student writes something like < 2.4.10 -- i.e., does not put an angle bracket on the right -- please deduct enough so that people who do this will STOP doing it. Record your decision on how much to deduct and send back to me your decision about such things when you return the papers to me. -- This goes for all supplementary marking scheme decisions you make. (I suggest 0.3 off for the first angle bracket missing in a "justification" of a step, 0.2 off for each of the next three omissions, and 0.1 off for each omission after that. Start the count again with a new problem. I don't want people who convince us that they feel that they are too important to have to write what everyone else writes to get marks as good as the marks we give to the "everyone else" who has the decency to write angle brackets. I see that some people are even leaving BOTH angle brackets off. Double the above deductions for those people, please.) If the student writes a triple bar instead of a <==> in the left margin of an "equational" proof, this is a LARGE error. Triple bar is a boolean connective, and the student is trying to use it as an English STATEMENT ABOUT a wff whose main connective is a triple bar. No good. The students were warned about this. Deduct 1.5 the first time this is done, 1 the second, and 0.5 for more times it is done. Start the count over again in a new problem. = in the left margin is also not good. Neither is <-->. Same deductions as for triple bar. The "//" at the end of a pf. is not necessary. Some people, instead of just jumping in and writing out the above obvious proof, will probably have run to the text book to find "similar" proofs. Such people would have been delighted to find something on page 63 (2.4.12), and would have begun their proof in the strange way suggested there: A \/ B == A <==> < 2.4.10 > A \/ B == (A \/ bottom), etc. This is certainly not WRONG, and should get full marks if all steps are written up adequately. The reasons are the same as the ones in the first proof I gave above, but in a different order. There may be other proofs as well, though they should be longer than the above. Please make up marking schemes worth a total of 10 marks to deal with such proofs, in the same spirit as the above. As for FATAL ERRORS -- i.e., a wrong step saying that a wff is syntactically equiv. to another when it ISN'T: One way to handle these is just to give part marks for anything correct and sensible done up to the point where the fatal error is made, and give 0 from then on, even if there is "good" stuff after the fatal error. People must learn that a single error RUINS a proof. If you find students making an error and proceeding and making a SECOND error just to get things to turn out right, you can give 0 or even a negative score for such nonsense. It is FAR better to give a partial proof that is free of error/bilge than to give a complete "proof" with two errors in it, the second one made just out of desperation to "get the right answer". By writing "proofs" with errors in them, one has already failed to "get the right answer".
I will put some more comments here, mainly for the benefit of the grader, who has not attended our lectures: A "bullet" proof is an equational proof, in which one is ALLOWED to (not required to, not forced to, but allowed to) omit mention of any use of any of the following: derived inference rule "Trans", Equanimity in either of its two forms, Leibniz, Associativity and symmetry of both == and \/. The students know from class that they must cite theorem/axiom numbers whenever citing a theorem/axiom as a reason for a step in a bullet proof. It is not enough for me if students use the Tourlakis reason "axiom", and they have been told this. This means students can play very fast-and-loosely the game of shuffling around subwffs of a wff that is a chain of ==s, and grouping (parenthesizing) them any way they want because of Generalized Associativity of an associative connective (which they are also allowed to use without comment). I have MANY times in class also advocated student use of little decorations of wffs to indicate to graders that they know exactly what they are doing in each step. Here's an example: Suppose we have already established, before a bullet proof begins, that (*) |- (C == D) == E and (**) |- (D == V) == H, for wffs as above of certain types. Then students can do things like this: E == V --- <==> < (*) > __________ C == D == V. ---------- <==> < (**) > ___ C == H . I.e., they can use Leibniz as above one way on the wff in the second line (parenthesized "leftward") and then turn around in the next step and use it again on the SAME wff, but parenthe- sized "rightward". But I have advised them to make very clear to the grader that they know exactly what they are doing (which they probably don't, but never mind...) by use of overlining and underlining, as above. Even more egregious examples of this sort of thing could, I suppose, be given, but I don't have the time for it now.
Problem 2: Prove that |- A /\ (A \/ B) == A . 10 marks (I.e., give a bullet proof. You may use any theorems up through 2.4.12, and, of course, as always, any axioms.) This one is also disgustingly easy. (First, a comment: There is only ONE theorem before 2.4.17 that deals with /\ at all. It follows that ANY proof of the purported theorem in this problem (bullet, annotated Hilbert, whatever) MUST use that theorem -- ax. (10), "the Golden Rule". I recommend using it immediately.) Pf: A /\ (A \/ B) <==> < ax. (10) > 4 marks A == A \/ B == A \/ A \/ B <==> < ax. (7) > 2 marks A == A \/ B == A \/ B <==> < ax. (2). Or 2.1.12. > 4 marks A. // (2.1.12 is an acceptable reason for such a step in a bullet proof, because by associativity and symmetry of ==, the syntactic equivalence asserted in this step follows from the synt. equiv. |- A == (A \/ B) == A == (A \/ B), and this is an instance of theorem scheme 2.1.12.) Ax. (2) is clearly also a legitimate reason since what I wrote above is just a vertical version of |-- ( (A == (A \/ B)) == (A \/ B) ) == A, which is one instance of a particular grouping of ax. (2) via parentheses. It's ok to write ax. n for ax. (n); I have indulged in this sort of sloppi- ness in class a lot. There are probably several other ways of justifying the last step, for 4 marks. One is to use 2.1.21 to replace A\/B == A\/B by top (2 marks), then state finally that A == top <==> < 2.1.21 again! > A. (final 2 marks) I predict that lots of people will do this. Tourlakis likes to use 2.1.21. I like to avoid top and do sexy stuff like the last step of my first solution of Problem 2 above. Grader: There is also the question of how to grade a step in an equational proof (say, a bullet proof) that is correct (meaning, there is a syntactic equivalence where the student says there is one, and the justification bullet- wise consists of mentioning a single theorem, say), but for which the reason given is WRONG. I guess this will be a judgment call each time it happens. If the student SHOULD have cited theorem n but instead cites theorem n+1 in a long list of theorems, and n obviously justifies the step and n+1 is a totally different sort of theorem that no idiot could possibly think justifies the step (I am speaking sloppily here, of course), one can perhaps assume that the student just read the list wrong and put down a wrong theorem number -- something should still be deducted (maybe 30% of the marks for the justification for that step), but maybe not nearly as much as if a student gives a wrong reason for a step and the error could be regarded as "genuine" -- a sign of ignorance/desperation/hoping-to-be-right-by- accident. I very much dislike guessing of this sort -- to me, honesty demands that someone who is guessing or just "trying something on" should SAY so to the grader -- something like "Not sure at all about this step, Boss." I very much dislike seeing a "proof" with some bonehead error in it somewhere and no comments anywhere and a proud "//" at the end of it. I react badly to this when it comes time to decide on marks. Problem 3: Another very easy proof. I start with the right side below, but one could start with the left, or write down the whole thing and arrive at 2.1.12 or so. |-- A \/ (B /\ C) == (A \/ B) /\ (A \/ C). Pf: (A \/ B) /\ (A \/ C) <==> < ax. 10 > (ok to say "Golden Rule" instead) (A \/ B) == (A \/ C) == ( (A \/ B) \/ (A \/ C) ) <==> < ax. 7 > A\/B == A\/C == A\/B\/C <==> < ax. 8 > A \/ (B == C) == A \/ B \/ C <==> < ax. 8 > A \/ (B == C == (B \/ C)) <==> < ax. 10 > A \/ (B /\ C). // Another proof: Start at the bottom above and work upward. Third proof: Write out 2.4.23(i) fully and play with it. Use ax. 10 once 2 marks again 1 mark ax. 8 once 2 marks again 1 mark ax. 7 2 marks And finally note that the last line is an instance of either 2.1.12 or ax. 2 or even ax. 1. Given our total freedom in bullet proofs to "see" parentheses in many different places in an unparenthesized string, and "see" subwffs occurring in different orders when connected by a symmetric connective (== or \/, anyway), any of the above three is ok at the end. My usual way of noting that a theorem has been reached is just to put a long dash and the theorem number and an exclamation point: -- 2.1.12!, for instance.