delcypher/propositional-logic-induction-proofs — pull request #1 by henryaddison (2012-05-14 19:20:23+00:00)
Title: making use of double negation rule explicit in proof of second part of 2.1

Hi Dan,

Really helpful set of proofs and awesome typesetting.

I believe there was a small problem with your proof that ¬A v B entails A --> B in that you were using the Double Negation rule implicitly. When applying v-elimination you have to do it with the strict negation of one of then entries, so that would be ¬¬A rather than A. Here's my correction to explicitly reference the double negation rule.

On a separate note, if I get time, I might add the de Morgan's rules of quantifiers in predicate logic.

Henry