Talk:Double Negation Elimination implies Law of Excluded Middle

"Wouldn't that require that the converse implication is also valid?"

Well yes it does, and in the page Double Negation/Double Negation Elimination/Sequent Form exactly that has been demonstrated.

I fully admit that this needs to be rethought somewhat, as when this was originally put together, the only plan was to demonstrate the properties of the particular axiom schema that I had to hand. This presentation is loosely based on the strategy outlined on 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems.

Having established that LEM could be taken as an axiom, it was the intention to point out that DNE could be used instead, the two being (within the context of the rest of the axiomatic framework) interderivable. My initial analysis gave it to make sense to me to make LEM the "axiom" and DNE the "derived rule" (contrary to Huth and Ryan's presentation) solely because LEM was one of the basic Aristotelian axioms, and so more "historically significant", if that makes sense.

As I say, the whole area needs to be reshuffled into our proposed axiomatic presentational technique, whereby we have a number of axiom schemata, with the resulting (common) foundational frameworks they lead to being demonstrated. In this case, the parallel nature of the LEM and DNE is to be emphasised.

This will follow, but first I need to extract the "basic" pages out of the compound pages in the usual manner of the refactoring task. This is (as you can see) going to be a fairly heavy task, and as such will need to be done in stages. During that time, it is appreciated that, more than likely, the logical flow is not going to be optimal. This will be improved in due course. --prime mover (talk) 11:35, 6 January 2013 (UTC)

Excellent. I recall how hard it was to rewrite some of the formal language stuff, and that wasn't even really dealing with different approaches; consequently, I'll try to be less of a pest hampering your appreciated work in this realm :). --Lord_Farin (talk) 11:42, 6 January 2013 (UTC)