Marker's comments on Problem Set 5 (Dustin Wehr)

Average 43 / 53.

Problem 1: 10 marks. About half of you gave formulas that are not in
the language L_A, by using Beta or Prime as function symbols, and lost
marks for that. Everyone seemed to understand how to use the Godel
Beta function.

Problem 2: 10 marks. I took off one point if your proof involved a
messy nested induction, AND you mixed up the two induction hypotheses
at some point. I took off a point if you used associativity of +
informally.

Problem 3: 4 marks for P7, 6 marks for P8. Most students formulated an
induction hypothesis and then never used it. Several students proved
P9 instead of, or in addition to, P7 or P8.

Problem 4: 3 marks for Corollaries 1 and 2 each. For Corollary 4, 3
marks for showing the set is recursively enumerable, 1 mark for
showing it's not decidable. Most students did not attempt, or did not
attempt seriously, to show the set is undecidable.

Problem 5: 10 marks. The most common mistake was adding a false axiom
that is too strong, and might result in an inconsistent theory. In
particular, some students added Forall x, Exists y, A(x,y) - every
program halts when given an encoding of itself as input. No one gave a
convincing argument for why the resulting theory was still consistent.
It really depends on the precise definition of A(x,y), but it's not
hard to imagine a program x that doesn't halt for some very simple
reason (an example suggested by Professor Cook: x just goes back and
forth between two non-accept states, without using any memory). So
then induction is not necessary to prove x doesn't halt, and in
particular if RA |- Not Exists y, A(x,y), then the extended theory
would be inconsistent.

Problem 6: 3 marks. If your solution was much longer than the sample
solution, you are probably not familiar enough with the results in the
notes.