Axiomatic Proof Of Double Negation Law

Law of Double Negation has 2 parts. The first part shows that from any statement follows that same statement, double negated.

Axiomatic proof:

[L1] ((p→((¬p→p)→¬¬p))→((p→(¬p→p))→(p→¬¬p))) by substitution of [A2] with p↦p, q↦(¬p→p), r↦¬¬p
[L2] (((¬p→p)→¬¬p)→(p→((¬p→p)→¬¬p))) by substitution of [A1] with p↦((¬p→p)→¬¬p), q↦p
[L3] (((¬p→p)→((¬p→¬p)→¬¬p))→(((¬p→p)→(¬p→¬p))→((¬p→p)→¬¬p))) by substitution of [A2] with p↦(¬p→p), q↦(¬p→¬p), r↦¬¬p
[L4] ((¬p→p)→((¬p→¬p)→¬¬p)) by substitution of [A9] with p↦¬p, q↦p
[L5] (((¬p→p)→(¬p→¬p))→((¬p→p)→¬¬p)) by detachment of [L3] and [L4]
[L6] ((¬p→(p→¬p))→((¬p→p)→(¬p→¬p))) by substitution of [A2] with p↦¬p, q↦p, r↦¬p
[L7] (¬p→(p→¬p)) by substitution of [A1] with p↦¬p, q↦p
[L8] ((¬p→p)→(¬p→¬p)) by detachment of [L6] and [L7]
[L9] ((¬p→p)→¬¬p) by detachment of [L5] and [L8]
[L10] (p→((¬p→p)→¬¬p)) by detachment of [L2] and [L9]
[L11] ((p→(¬p→p))→(p→¬¬p)) by detachment of [L1] and [L10]
[L12] (p→(¬p→p)) by substitution of [A1] with p↦p, q↦¬p
[L13] (p→¬¬p) by detachment of [L11] and [L12]

Proof by Tableau method is here.

The second part shows the inverse relation, that is: given double negated statement, the same direct statement follows. Proof:

[L1] ((¬¬p→((p∨¬p)→p))→((¬¬p→(p∨¬p))→(¬¬p→p))) by substitution of [A2] with p↦¬¬p, q↦(p∨¬p), r↦p
[L2] ((¬¬p→((¬p→p)→((p∨¬p)→p)))→((¬¬p→(¬p→p))→(¬¬p→((p∨¬p)→p)))) by substitution of [A2] with p↦¬¬p, q↦(¬p→p), r↦((p∨¬p)→p)
[L3] (((¬p→p)→((p∨¬p)→p))→(¬¬p→((¬p→p)→((p∨¬p)→p)))) by substitution of [A1] with p↦((¬p→p)→((p∨¬p)→p)), q↦¬¬p
[L4] ((p→p)→((¬p→p)→((p∨¬p)→p))) by substitution of [A8] with p↦p, r↦p, q↦¬p
[L5] ((p→((q→p)→p))→((p→(q→p))→(p→p))) by substitution of [A2] with p↦p, q↦(q→p), r↦p
[L6] (p→((q→p)→p)) by substitution of [A1] with p↦p, q↦(q→p)
[L7] ((p→(q→p))→(p→p)) by detachment of [L5] and [L6]
[L8] (p→p) by detachment of [L7] and [A1]
[L9] ((¬p→p)→((p∨¬p)→p)) by detachment of [L4] and [L8]
[L10] (¬¬p→((¬p→p)→((p∨¬p)→p))) by detachment of [L3] and [L9]
[L11] ((¬¬p→(¬p→p))→(¬¬p→((p∨¬p)→p))) by detachment of [L2] and [L10]
[L12] (¬¬p→(¬p→p)) by substitution of [A10] with p↦¬p, q↦p
[L13] (¬¬p→((p∨¬p)→p)) by detachment of [L11] and [L12]
[L14] ((¬¬p→(p∨¬p))→(¬¬p→p)) by detachment of [L1] and [L13]
[L15] ((p∨¬p)→(¬¬p→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦¬¬p
[L16] (¬¬p→(p∨¬p)) by detachment of [L15] and [A11]
[L17] (¬¬p→p) by detachment of [L14] and [L16]

Proof by Tableau method is here.