Talk:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2/Forward Implication

Is there a specific reason for posting this result up when we have Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2 which does the job in one go?

The reason the existing results are posted is because they can be found in texts. There is no particular other reason to post up the ones that exist there.

So unless this result can be cited in a particular source, which will then be listed in the "Sources" section, then I'm afraid there is no reason for it to exist here. --prime mover (talk) 19:40, 24 March 2013 (UTC)

There are two reasons. Reason #1: I will soon post a similar one for the reverse implication and a new proof of the full rule that uses both. Reason #2: I specifically need the forward implication for a proof I will post soon, and it seems awfully silly to have to invoke double implication elimination on a rule proven using double implication introduction. So for both reasons, this page should stay. --Dfeuer (talk) 20:46, 24 March 2013 (UTC)

"seems awfully silly to" etc. Huh? not really. If you need to invoke this distributive law, you just need to invoke it as is. Oh, no no no no, pleeeeease tell me you're not going to use Natural Deduction to prove something in set theory?

Yes I expect you are going to post a similar one for the reverse implication for which I offer the same reply: seems a bit unnecessary.

I will see the proof that supposedly purports to need the individual bits of this result and a judgment will be made then as to whether this dichotomy has any worth, then rewrite and/or revert and/or delete as appropriate. --prime mover (talk) 21:05, 24 March 2013 (UTC)

Said proof is trivial. This operation is called "refactoring". It allows a proof to be broken up into smaller results which are then combined. Sometimes one or more of the smaller results is useful on its own. How do you suggest reasoning in set theory? Just claim things and leave it entirely up to the reader to figure out why? $(p \lor q) \land (r \lor s) \vdash p \lor r \lor (q \land s)$ is not hard to prove, but I wouldn't call it immediately obvious (the particular text I'm using glosses over it at least once with an argument that appears to require LEM, which is not actually necessary). --Dfeuer (talk) 21:18, 24 March 2013 (UTC)

Refactoring huh? Never heard of it. Sounds silly to me.

But seriously, though, clumsy rhetoric and argumentum ad passiones aside, while I can see that you are keen to post up a proof of your current result du jour, it still seems like overkill to me to split up this existing result into two separate pieces - can you not just link to whichever of Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 1 you think you may need instead? After all, that's all you're doing when you're posting these piffling proofs up. --prime mover (talk) 21:43, 24 March 2013 (UTC)

In this context, using the implication form rather than the sequent form will allow the proof to be considerably more straightforward/readable. --Dfeuer (talk) 21:48, 24 March 2013 (UTC)

I await the fruits of your intellect with bated breath. --prime mover (talk) 21:50, 24 March 2013 (UTC)