Assignment 2: Some solutions and marking scheme
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
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
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
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
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,
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,
(*) |- (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.
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
(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
Grader: There is also the question of how to grade
a step in an equational proof (say, a bullet proof) that
(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),
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
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).
(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!,