Talk:Peirce's Law is Equivalent to Law of Excluded Middle

Dfeuer: Sorry to have reversed out your work last night, but it seemed we were in danger of drowning in over-reliance upon the ".../Sequent Form/Proof n" style of presentation, which is limited in usefulness - it is difficult to see which proof uses which assumptions, and the clarity gets lost in the anonymity of undifferentiated titles.

The ".../Sequent Form/..." style of presentation was designed solely to make easy the justification of different axiom schemata for natural deduction: arranging the axioms in a formal style makes it more straightforward to handle them.

As for this page, I went through and redid what needed to be done and finally crafted that LEM -> PL proof which had eluded me back whenever it was. You were right, what was there had no reason to exist. --prime mover (talk) 10:14, 1 June 2013 (UTC)

Incidentally, so as to avoid the difficulty surrounding whether $\vdash$ can be used as a connective, and how the wording needs to be made circuitous so as not to use $\vdash$ in a meta-context, I recommend the form:

$\left({p \lor \neg p}\right) \dashv \vdash \left({\left({\left({p \implies q}\right) \implies p}\right) \implies p}\right)$

with or without the parentheses around either side.

Then the entire statement has been reduced to a simple expression of zeroth-order logic.

Or even:

$\vdash \left({p \lor \neg p}\right) \iff \left({\left({\left({p \implies q}\right) \implies p}\right) \implies p}\right)$

which goes one stage further. --prime mover (talk) 10:19, 1 June 2013 (UTC)