## Law of Excluded Middle

Somebody interested in logic could perhaps add a proof that this is indeed a valid sequent in propositional logic. I assume that it follows in a few steps from the Law of Excluded Middle - or perhaps they are even equivalent? In any event, I unfortunately do not know how to write such proofs. KarlFrei (talk) 13:51, 11 October 2018 (EDT)

Did you see the sequent form and the variants (and that they are links to subpages)? If so, could you clarify? — Lord_Farin (talk) 14:22, 11 October 2018 (EDT)
Sorry! Indeed I did not notice that the proofs were on the subpages. So, looking at them, it seems that they do not rely on the law of excluded middle, nor is there a dependence the other way around (as apparently LEM depends on nothing). Or did I miss it?
So - perhaps you could explain this to me, if it is not too much trouble? Intuitively, I would expect these two things to be closely related, so it is very confusing to me that I don't see a relation. Unfortunately I did not seriously study logic for 25 years. KarlFrei (talk) 14:38, 11 October 2018 (EDT)
Having studied propositional logic in quite some depth, and having spent a ridiculous amount of time trying to get it organised on PW, I can say that whether you base A on B or B on A is often a matter of whichever axiom and formalisation system you enjoy working with. (Case in point, you can either define $\neg p =_{\text{def}} p \implies \bot$ or instead define $\bot =_{\text{def}} p \land \neg p$.) So what exactly makes sense to "prove" is a very diffuse matter indeed.
And since at PW, we aim to avoid such choices, it becomes very hard to find a good approach to propositional logic... Therefore, it is probably not possible to learn propositional logic from reading ProofWiki pages alone. But if one is looking up certain ways to prove A from B or vice versa, or just refresh one's knowledge about the details of the Praeclarum Theorema, PW is a good place.
I hope that makes some kind of sense. — Lord_Farin (talk) 14:52, 11 October 2018 (EDT)
Regarding your actual question, then, the answer might be that nobody could be bothered to add yet another approach to PropLog to PW just to establish this relation (in either or both directions). You could flag it up with an Expand template invocation. — Lord_Farin (talk) 14:56, 11 October 2018 (EDT)
Thank you! I did not realize (or plain forgot) that things were so complicated at this level. It reminds me of the various ways to define the real numbers. I will add this template as you suggested. KarlFrei (talk) 02:10, 12 October 2018 (EDT)
Hmm, given what you wrote, probably you want to check out Reductio ad Absurdum. — Lord_Farin (talk) 02:45, 12 October 2018 (EDT)
Thanks! That completely resolves my confusion. I have expanded the Also known as section to explain this further. KarlFrei (talk) 03:42, 12 October 2018 (EDT)