Axiomatic Proof Of Negation Elimination Law
Axiomatic proof of the Negation Elimination is below.
[L1] ((¬p→((p→(¬q→¬p))→(p→q)))→((¬p→(p→(¬q→¬p)))→(¬p→(p→q)))) by substitution of [A2] with p↦¬p, q↦(p→(¬q→¬p)), r↦(p→q) [L2] (((p→(¬q→¬p))→(p→q))→(¬p→((p→(¬q→¬p))→(p→q)))) by substitution of [A1] with p↦((p→(¬q→¬p))→(p→q)), q↦¬p [L3] (((p→(¬q→¬p))→((p→(¬q→p))→(p→q)))→(((p→(¬q→¬p))→(p→(¬q→p)))→((p→(¬q→¬p))→(p→q)))) by substitution of [A2] with p↦(p→(¬q→¬p)), q↦(p→(¬q→p)), r↦(p→q) [L4] (((p→(¬q→¬p))→((p→((¬q→p)→q))→((p→(¬q→p))→(p→q))))→(((p→(¬q→¬p))→(p→((¬q→p)→q)))→((p→(¬q→¬p))→((p→(¬q→p))→(p→q))))) by substitution of [A2] with p↦(p→(¬q→¬p)), q↦(p→((¬q→p)→q)), r↦((p→(¬q→p))→(p→q)) [L5] (((p→((¬q→p)→q))→((p→(¬q→p))→(p→q)))→((p→(¬q→¬p))→((p→((¬q→p)→q))→((p→(¬q→p))→(p→q))))) by substitution of [A1] with p↦((p→((¬q→p)→q))→((p→(¬q→p))→(p→q))), q↦(p→(¬q→¬p)) [L6] ((p→((¬q→p)→q))→((p→(¬q→p))→(p→q))) by substitution of [A2] with p↦p, q↦(¬q→p), r↦q [L7] ((p→(¬q→¬p))→((p→((¬q→p)→q))→((p→(¬q→p))→(p→q)))) by detachment of [L5] and [L6] [L8] (((p→(¬q→¬p))→(p→((¬q→p)→q)))→((p→(¬q→¬p))→((p→(¬q→p))→(p→q)))) by detachment of [L4] and [L7] [L9] ((p→((¬q→¬p)→((¬q→p)→q)))→((p→(¬q→¬p))→(p→((¬q→p)→q)))) by substitution of [A2] with p↦p, q↦(¬q→¬p), r↦((¬q→p)→q) [L10] (((¬q→¬p)→((¬q→p)→q))→(p→((¬q→¬p)→((¬q→p)→q)))) by substitution of [A1] with p↦((¬q→¬p)→((¬q→p)→q)), q↦p [L11] (p→((¬q→¬p)→((¬q→p)→q))) by detachment of [L10] and [A3] [L12] ((p→(¬q→¬p))→(p→((¬q→p)→q))) by detachment of [L9] and [L11] [L13] ((p→(¬q→¬p))→((p→(¬q→p))→(p→q))) by detachment of [L8] and [L12] [L14] (((p→(¬q→¬p))→(p→(¬q→p)))→((p→(¬q→¬p))→(p→q))) by detachment of [L3] and [L13] [L15] ((p→(¬q→p))→((p→(¬q→¬p))→(p→(¬q→p)))) by substitution of [A1] with p↦(p→(¬q→p)), q↦(p→(¬q→¬p)) [L16] (p→(¬q→p)) by substitution of [A1] with p↦p, q↦¬q [L17] ((p→(¬q→¬p))→(p→(¬q→p))) by detachment of [L15] and [L16] [L18] ((p→(¬q→¬p))→(p→q)) by detachment of [L14] and [L17] [L19] (¬p→((p→(¬q→¬p))→(p→q))) by detachment of [L2] and [L18] [L20] ((¬p→(p→(¬q→¬p)))→(¬p→(p→q))) by detachment of [L1] and [L19] [L21] ((¬p→((¬q→¬p)→(p→(¬q→¬p))))→((¬p→(¬q→¬p))→(¬p→(p→(¬q→¬p))))) by substitution of [A2] with p↦¬p, q↦(¬q→¬p), r↦(p→(¬q→¬p)) [L22] (((¬q→¬p)→(p→(¬q→¬p)))→(¬p→((¬q→¬p)→(p→(¬q→¬p))))) by substitution of [A1] with p↦((¬q→¬p)→(p→(¬q→¬p))), q↦¬p [L23] ((¬q→¬p)→(p→(¬q→¬p))) by substitution of [A1] with p↦(¬q→¬p), q↦p [L24] (¬p→((¬q→¬p)→(p→(¬q→¬p)))) by detachment of [L22] and [L23] [L25] ((¬p→(¬q→¬p))→(¬p→(p→(¬q→¬p)))) by detachment of [L21] and [L24] [L26] (¬p→(¬q→¬p)) by substitution of [A1] with p↦¬p, q↦¬q [L27] (¬p→(p→(¬q→¬p))) by detachment of [L25] and [L26] [L28] (¬p→(p→q)) by detachment of [L20] and [L27]
Proof by Tableau method is here.