Posted: Apr 07, 2012 5:10 pm
VazScep wrote:My lemma isn't quite the same as yours. I basically introduced the notion of false (⊥ or f) as the negation of the tautology "P → P". But I can then easily use this to derive an arbitrary proposition.
I see
.Well I was set on a longer strategy from the start. I saw that I could arrive on (~p ==> p) from the premises
(~p ==> q), (~p ==> ~q) by transforming it into (~p ==> q), (q ==> p) and then applying hypothetical syllogism. After that I just had to prove the tautology "(~p ==> p) ==> p" but that one is much harder. It seems in fact easier to start from mendelson's 3rd to prove it, instead.
It's definitely going on my reading list if I ever land a C++ job. I'm thinking I'll go through Scott Meyers again, and then probably Sutter and Coplien too.
By the way, you should definitely check out the D language sometime. It's a huge improvement over C++ IMHO. I think it's the project Alexandrescu is most involved with right now.