Well, it serves me right for writing a logic post so quickly before going to bed; somehow I managed to write the exact opposite of what I intended, and kept writing it, and didn't catch it until I realized, of a sudden in re-reading, that if we kept translating as I was translating we'd get a very weird propositional logic. So some corrections to my previous post:
(1) It's contradiction, not contrariety, that gives the simpler and more elegant proof in each case.
(2) The real First Equivalence proof is:
(1) ~ (p v q)
(2) It is not the case that ~pE~q
(3) ~pI~q
(4) (~p & ~q)
(3) The real Second Equivalence proof is:
(1) ~ (p & q)
(2) It is not the case that pIq
(3) pEq
(4) (~p v ~q)
(4) The contrariety-based proofs are to be changed on the same principles.
So that's how it really works. Assuming I haven't made a similar mistake!
For some reason when I was writing the post, I kept mistranslating the conjunctions as implications. It took me embarrassingly long to figure out what I was doing wrong, too. It was like one of those math problems where you know exactly how to solve it, but keep getting a wacky answer because you keep making a simple addition mistake in the beginning.
In any case, the problem wasn't that we didn't get a result in propositional logic, but that we got a result from the wrong propositional logic. I was aiming to prove a result for a standard propositional logic and proved a result for a nonstandard one. It's an interesting nonstandard logic, though; in it all implications are equivalent to conjunctions, so from (p → q) you can directly conclude p. An interesting question: what additional assumptions do you have to make to treat this nonstandard logic as truth-functionally legitimate? The Welton diagram for implication in the standard case is:
| | X | | |
while for conjunction it is the much, much stronger:
| | X | X | X |
To move from the weaker to the stronger, the universe would have to be explicitly set up so that a false consequent is never admissible: we can never make something a consequent unless we have supposed it to be true. (Which makes simple sense: a logic in which implications are equivalent to conjunctions is a logic in which every implication acts like a modus ponens.) Or, to put it in terms of truth tables, to treat implications like conjunctions you need a context where you can ignore the truth-functional differences between the two -- and the differences occur when q is false.
