I am busy working on Assignment 1 for COS407 2008. (Mathematical Logic for Computer Science)

Q1 (iii) asks us to prove this proposition is valid using truth tables.

(A nand ( B nand C )) equiv (B nand ( A nand C )).

However this is not a valid proposition.

This can be seen clearly for the interpretation when A is true, B is

false and C is true.

(true nand ( false nand true)) euiv (false nand ( true nand true))

(true nand ( true )) equiv ( false nand (false)

false equiv true

Furthermore, Question 2 and Question 5 also asks us to prove that this same proposition is valid using a different method.

Obviously I can’t prove its valid. Unless I change the rules of logic. Hmmph.

And even more problematically Question 6 asks us to do something with the proposition (ie prove it is a theory of the Gentzen system G) that may not be possible. Its possible to prove something is a theory of the system, but its not so easy to prove a proposition is not a theory of the system (if even possible.)

(The only silver lining is that I understand enough to see that the question is faulty.)

I sent an email to the lecturer and she responded very quickly.

Here is her first response:

Hi,

Thanks for pointing this out. I’m not going to change the assignment now, so you should answer the questions with the given formula. E.g. give your counter-example for Question 2 (because this is a semantic argument), and draw an open tableau which builds a counter-model for Question 5.

Regards,

I then responded

Thanks, and for Question 6.

I have not actually read the section on Gentzen systems yet (that is this weekend’s task); I am assuming now that the proposition would not be a theory of the Gentzen system G?

So I assume I should prove that instead. (Forgive me if I am speaking nonsense as I have not yet studied this system.)

I appreciate your quick response!

As I was not sure if it was even possible to do what she suggested; but I have not yet studied the section to make sure if I am right. But I was right and I received this later response.

It’s not so easy to prove that a given formula is NOT a theorem in a Gentzen system. So instead of proving this, you can rather explain why this is not as simple a matter as with the tableau proof. I.e. why are Gentzen proofs not a suitable proof procedure to verify that a given formula is NOT a theorem.

Hope this helps!

So… I now know how to proceed and can stick with my time-schedule. (I want to get this assignment completed by the end of January).

I must admit I am very impressed with the quickness of the response from the lecturer. ðŸ™‚

Maybe they’re trying to trick you into devising new proof strategies?