Axiomatic Proof Of Negation Introduction
These two formulas are present in Whitehead/Russel Principia Mathematica.
Axiomatic proofs follow.
[L1] ((((¬p→¬q)→p)→((¬p→((¬p→¬q)→p))→(¬p→q)))→((((¬p→¬q)→p)→(¬p→((¬p→¬q)→p)))→(((¬p→¬q)→p)→(¬p→q)))) by substitution of [A2] with p↦((¬p→¬q)→p), q↦(¬p→((¬p→¬q)→p)), r↦(¬p→q) [L2] (((¬p→((¬p→¬q)→p))→(¬p→q))→(((¬p→¬q)→p)→((¬p→((¬p→¬q)→p))→(¬p→q)))) by substitution of [A1] with p↦((¬p→((¬p→¬q)→p))→(¬p→q)), q↦((¬p→¬q)→p) [L3] ((¬p→(((¬p→¬q)→p)→q))→((¬p→((¬p→¬q)→p))→(¬p→q))) by substitution of [A2] with p↦¬p, q↦((¬p→¬q)→p), r↦q [L4] ((¬p→(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q)))→((¬p→((¬p→¬q)→¬p))→(¬p→(((¬p→¬q)→p)→q)))) by substitution of [A2] with p↦¬p, q↦((¬p→¬q)→¬p), r↦(((¬p→¬q)→p)→q) [L5] ((((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q))→(¬p→(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q)))) by substitution of [A1] with p↦(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q)), q↦¬p [L6] ((((¬p→¬q)→¬p)→((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q)))→((((¬p→¬q)→¬p)→(((¬p→¬q)→p)→((¬p→¬q)→¬p)))→(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q)))) by substitution of [A2] with p↦((¬p→¬q)→¬p), q↦(((¬p→¬q)→p)→((¬p→¬q)→¬p)), r↦(((¬p→¬q)→p)→q) [L7] (((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q))→(((¬p→¬q)→¬p)→((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q)))) by substitution of [A1] with p↦((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q)), q↦((¬p→¬q)→¬p) [L8] ((((¬p→¬q)→p)→(((¬p→¬q)→¬p)→q))→((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q))) by substitution of [A2] with p↦((¬p→¬q)→p), q↦((¬p→¬q)→¬p), r↦q [L9] ((((¬p→¬q)→p)→((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q)))→((((¬p→¬q)→p)→(((¬p→¬q)→¬p)→¬(¬p→¬q)))→(((¬p→¬q)→p)→(((¬p→¬q)→¬p)→q)))) by substitution of [A2] with p↦((¬p→¬q)→p), q↦(((¬p→¬q)→¬p)→¬(¬p→¬q)), r↦(((¬p→¬q)→¬p)→q) [L10] (((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q))→(((¬p→¬q)→p)→((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q)))) by substitution of [A1] with p↦((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q)), q↦((¬p→¬q)→p) [L11] ((((¬p→¬q)→¬p)→(¬(¬p→¬q)→q))→((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q))) by substitution of [A2] with p↦((¬p→¬q)→¬p), q↦¬(¬p→¬q), r↦q [L12] ((((¬p→¬q)→¬p)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q)))→((((¬p→¬q)→¬p)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(((¬p→¬q)→¬p)→(¬(¬p→¬q)→q)))) by substitution of [A2] with p↦((¬p→¬q)→¬p), q↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)), r↦(¬(¬p→¬q)→q) [L13] (((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q))→(((¬p→¬q)→¬p)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q)))) by substitution of [A1] with p↦((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q)), q↦((¬p→¬q)→¬p) [L14] (((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q)))→(((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q))))→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q)))) by substitution of [A2] with p↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)), q↦(¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q))), r↦(¬(¬p→¬q)→q) [L15] (((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q))→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q)))) by substitution of [A1] with p↦((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q)), q↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)) [L16] ((¬(¬p→¬q)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q))→((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q))) by substitution of [A2] with p↦¬(¬p→¬q), q↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)), r↦q [L17] ((¬(¬p→¬q)→(q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)))→((¬(¬p→¬q)→q)→(¬(¬p→¬q)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)))) by substitution of [A2] with p↦¬(¬p→¬q), q↦q, r↦((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q) [L18] ((q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q))→(¬(¬p→¬q)→(q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)))) by substitution of [A1] with p↦(q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)), q↦¬(¬p→¬q) [L19] (q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)) by substitution of [A1] with p↦q, q↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)) [L20] (¬(¬p→¬q)→(q→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q))) by detachment of [L18] and [L19] [L21] ((¬(¬p→¬q)→q)→(¬(¬p→¬q)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q))) by detachment of [L17] and [L20] [L22] ((¬(¬p→¬q)→((¬q→¬(¬p→¬q))→q))→((¬(¬p→¬q)→(¬q→¬(¬p→¬q)))→(¬(¬p→¬q)→q))) by substitution of [A2] with p↦¬(¬p→¬q), q↦(¬q→¬(¬p→¬q)), r↦q [L23] (((¬q→¬(¬p→¬q))→q)→(¬(¬p→¬q)→((¬q→¬(¬p→¬q))→q))) by substitution of [A1] with p↦((¬q→¬(¬p→¬q))→q), q↦¬(¬p→¬q) [L24] (((¬q→¬(¬p→¬q))→(¬¬q→q))→(((¬q→¬(¬p→¬q))→¬¬q)→((¬q→¬(¬p→¬q))→q))) by substitution of [A2] with p↦(¬q→¬(¬p→¬q)), q↦¬¬q, r↦q [L25] ((¬¬q→q)→((¬q→¬(¬p→¬q))→(¬¬q→q))) by substitution of [A1] with p↦(¬¬q→q), q↦(¬q→¬(¬p→¬q)) [L26] ((¬¬q→((¬q→q)→q))→((¬¬q→(¬q→q))→(¬¬q→q))) by substitution of [A2] with p↦¬¬q, q↦(¬q→q), r↦q [L27] (((¬q→q)→q)→(¬¬q→((¬q→q)→q))) by substitution of [A1] with p↦((¬q→q)→q), q↦¬¬q [L28] (((¬q→q)→((q∨¬q)→q))→(((¬q→q)→(q∨¬q))→((¬q→q)→q))) by substitution of [A2] with p↦(¬q→q), q↦(q∨¬q), r↦q [L29] ((q→q)→((¬q→q)→((q∨¬q)→q))) by substitution of [A8] with p↦q, r↦q, q↦¬q [L30] ((q→((a→q)→q))→((q→(a→q))→(q→q))) by substitution of [A2] with p↦q, q↦(a→q), r↦q [L31] (q→((a→q)→q)) by substitution of [A1] with p↦q, q↦(a→q) [L32] ((q→(a→q))→(q→q)) by detachment of [L30] and [L31] [L33] (q→(a→q)) by substitution of [A1] with p↦q, q↦a [L34] (q→q) by detachment of [L32] and [L33] [L35] ((¬q→q)→((q∨¬q)→q)) by detachment of [L29] and [L34] [L36] (((¬q→q)→(q∨¬q))→((¬q→q)→q)) by detachment of [L28] and [L35] [L37] ((q∨¬q)→((¬q→q)→(q∨¬q))) by substitution of [A1] with p↦(q∨¬q), q↦(¬q→q) [L38] (q∨¬q) by substitution of [A11] with p↦q [L39] ((¬q→q)→(q∨¬q)) by detachment of [L37] and [L38] [L40] ((¬q→q)→q) by detachment of [L36] and [L39] [L41] (¬¬q→((¬q→q)→q)) by detachment of [L27] and [L40] [L42] ((¬¬q→(¬q→q))→(¬¬q→q)) by detachment of [L26] and [L41] [L43] (¬¬q→(¬q→q)) by substitution of [A10] with p↦¬q, q↦q [L44] (¬¬q→q) by detachment of [L42] and [L43] [L45] ((¬q→¬(¬p→¬q))→(¬¬q→q)) by detachment of [L25] and [L44] [L46] (((¬q→¬(¬p→¬q))→¬¬q)→((¬q→¬(¬p→¬q))→q)) by detachment of [L24] and [L45] [L47] ((¬q→(¬p→¬q))→((¬q→¬(¬p→¬q))→¬¬q)) by substitution of [A9] with p↦¬q, q↦(¬p→¬q) [L48] (¬q→(¬p→¬q)) by substitution of [A1] with p↦¬q, q↦¬p [L49] ((¬q→¬(¬p→¬q))→¬¬q) by detachment of [L47] and [L48] [L50] ((¬q→¬(¬p→¬q))→q) by detachment of [L46] and [L49] [L51] (¬(¬p→¬q)→((¬q→¬(¬p→¬q))→q)) by detachment of [L23] and [L50] [L52] ((¬(¬p→¬q)→(¬q→¬(¬p→¬q)))→(¬(¬p→¬q)→q)) by detachment of [L22] and [L51] [L53] (¬(¬p→¬q)→(¬q→¬(¬p→¬q))) by substitution of [A1] with p↦¬(¬p→¬q), q↦¬q [L54] (¬(¬p→¬q)→q) by detachment of [L52] and [L53] [L55] (¬(¬p→¬q)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→q)) by detachment of [L21] and [L54] [L56] ((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q)) by detachment of [L16] and [L55] [L57] ((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→((¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(¬(¬p→¬q)→q))) by detachment of [L15] and [L56] [L58] (((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q))))→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q))) by detachment of [L14] and [L57] [L59] ((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))) by substitution of [A1] with p↦(((¬p→¬q)→¬¬p)→¬(¬p→¬q)), q↦¬(¬p→¬q) [L60] ((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q)) by detachment of [L58] and [L59] [L61] (((¬p→¬q)→¬p)→((((¬p→¬q)→¬¬p)→¬(¬p→¬q))→(¬(¬p→¬q)→q))) by detachment of [L13] and [L60] [L62] ((((¬p→¬q)→¬p)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q)))→(((¬p→¬q)→¬p)→(¬(¬p→¬q)→q))) by detachment of [L12] and [L61] [L63] (((¬p→¬q)→¬p)→(((¬p→¬q)→¬¬p)→¬(¬p→¬q))) by substitution of [A9] with p↦(¬p→¬q), q↦¬p [L64] (((¬p→¬q)→¬p)→(¬(¬p→¬q)→q)) by detachment of [L62] and [L63] [L65] ((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q)) by detachment of [L11] and [L64] [L66] (((¬p→¬q)→p)→((((¬p→¬q)→¬p)→¬(¬p→¬q))→(((¬p→¬q)→¬p)→q))) by detachment of [L10] and [L65] [L67] ((((¬p→¬q)→p)→(((¬p→¬q)→¬p)→¬(¬p→¬q)))→(((¬p→¬q)→p)→(((¬p→¬q)→¬p)→q))) by detachment of [L9] and [L66] [L68] (((¬p→¬q)→p)→(((¬p→¬q)→¬p)→¬(¬p→¬q))) by substitution of [A9] with p↦(¬p→¬q), q↦p [L69] (((¬p→¬q)→p)→(((¬p→¬q)→¬p)→q)) by detachment of [L67] and [L68] [L70] ((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q)) by detachment of [L8] and [L69] [L71] (((¬p→¬q)→¬p)→((((¬p→¬q)→p)→((¬p→¬q)→¬p))→(((¬p→¬q)→p)→q))) by detachment of [L7] and [L70] [L72] ((((¬p→¬q)→¬p)→(((¬p→¬q)→p)→((¬p→¬q)→¬p)))→(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q))) by detachment of [L6] and [L71] [L73] (((¬p→¬q)→¬p)→(((¬p→¬q)→p)→((¬p→¬q)→¬p))) by substitution of [A1] with p↦((¬p→¬q)→¬p), q↦((¬p→¬q)→p) [L74] (((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q)) by detachment of [L72] and [L73] [L75] (¬p→(((¬p→¬q)→¬p)→(((¬p→¬q)→p)→q))) by detachment of [L5] and [L74] [L76] ((¬p→((¬p→¬q)→¬p))→(¬p→(((¬p→¬q)→p)→q))) by detachment of [L4] and [L75] [L77] (¬p→((¬p→¬q)→¬p)) by substitution of [A1] with p↦¬p, q↦(¬p→¬q) [L78] (¬p→(((¬p→¬q)→p)→q)) by detachment of [L76] and [L77] [L79] ((¬p→((¬p→¬q)→p))→(¬p→q)) by detachment of [L3] and [L78] [L80] (((¬p→¬q)→p)→((¬p→((¬p→¬q)→p))→(¬p→q))) by detachment of [L2] and [L79] [L81] ((((¬p→¬q)→p)→(¬p→((¬p→¬q)→p)))→(((¬p→¬q)→p)→(¬p→q))) by detachment of [L1] and [L80] [L82] (((¬p→¬q)→p)→(¬p→((¬p→¬q)→p))) by substitution of [A1] with p↦((¬p→¬q)→p), q↦¬p [L83] (((¬p→¬q)→p)→(¬p→q)) by detachment of [L81] and [L82]
Proof by Tableau method is here.
[L1] (((¬p→q)→(((¬p→¬q)→¬¬p)→((¬p→¬q)→p)))→(((¬p→q)→((¬p→¬q)→¬¬p))→((¬p→q)→((¬p→¬q)→p)))) by substitution of [A2] with p↦(¬p→q), q↦((¬p→¬q)→¬¬p), r↦((¬p→¬q)→p) [L2] ((((¬p→¬q)→¬¬p)→((¬p→¬q)→p))→((¬p→q)→(((¬p→¬q)→¬¬p)→((¬p→¬q)→p)))) by substitution of [A1] with p↦(((¬p→¬q)→¬¬p)→((¬p→¬q)→p)), q↦(¬p→q) [L3] (((¬p→¬q)→(¬¬p→p))→(((¬p→¬q)→¬¬p)→((¬p→¬q)→p))) by substitution of [A2] with p↦(¬p→¬q), q↦¬¬p, r↦p [L4] ((¬¬p→p)→((¬p→¬q)→(¬¬p→p))) by substitution of [A1] with p↦(¬¬p→p), q↦(¬p→¬q) [L5] ((¬¬p→((¬p→p)→p))→((¬¬p→(¬p→p))→(¬¬p→p))) by substitution of [A2] with p↦¬¬p, q↦(¬p→p), r↦p [L6] (((¬p→p)→p)→(¬¬p→((¬p→p)→p))) by substitution of [A1] with p↦((¬p→p)→p), q↦¬¬p [L7] (((¬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 [L8] ((p→p)→((¬p→p)→((p∨¬p)→p))) by substitution of [A8] with p↦p, r↦p, q↦¬p [L9] ((p→((a→p)→p))→((p→(a→p))→(p→p))) by substitution of [A2] with p↦p, q↦(a→p), r↦p [L10] (p→((a→p)→p)) by substitution of [A1] with p↦p, q↦(a→p) [L11] ((p→(a→p))→(p→p)) by detachment of [L9] and [L10] [L12] (p→(a→p)) by substitution of [A1] with p↦p, q↦a [L13] (p→p) by detachment of [L11] and [L12] [L14] ((¬p→p)→((p∨¬p)→p)) by detachment of [L8] and [L13] [L15] (((¬p→p)→(p∨¬p))→((¬p→p)→p)) by detachment of [L7] and [L14] [L16] ((p∨¬p)→((¬p→p)→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦(¬p→p) [L17] ((¬p→p)→(p∨¬p)) by detachment of [L16] and [A11] [L18] ((¬p→p)→p) by detachment of [L15] and [L17] [L19] (¬¬p→((¬p→p)→p)) by detachment of [L6] and [L18] [L20] ((¬¬p→(¬p→p))→(¬¬p→p)) by detachment of [L5] and [L19] [L21] (¬¬p→(¬p→p)) by substitution of [A10] with p↦¬p, q↦p [L22] (¬¬p→p) by detachment of [L20] and [L21] [L23] ((¬p→¬q)→(¬¬p→p)) by detachment of [L4] and [L22] [L24] (((¬p→¬q)→¬¬p)→((¬p→¬q)→p)) by detachment of [L3] and [L23] [L25] ((¬p→q)→(((¬p→¬q)→¬¬p)→((¬p→¬q)→p))) by detachment of [L2] and [L24] [L26] (((¬p→q)→((¬p→¬q)→¬¬p))→((¬p→q)→((¬p→¬q)→p))) by detachment of [L1] and [L25] [L27] ((¬p→q)→((¬p→¬q)→¬¬p)) by substitution of [A9] with p↦¬p, q↦q [L28] ((¬p→q)→((¬p→¬q)→p)) by detachment of [L26] and [L27]
Proof by Tableau method is here.