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:
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.
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. 🙂