Axiomatic Proof Of Syllogism Rules
I provide axiomatic proofs for 3 variations of syllogism rule.
[L1] (((p→q)→(((q→r)→(p→q))→((q→r)→(p→r))))→(((p→q)→((q→r)→(p→q)))→((p→q)→((q→r)→(p→r))))) by substituton of [A2] with p↦(p→q), q↦((q→r)→(p→q)), r↦((q→r)→(p→r)) [L2] ((((q→r)→(p→q))→((q→r)→(p→r)))→((p→q)→(((q→r)→(p→q))→((q→r)→(p→r))))) by substituton of [A1] with p↦(((q→r)→(p→q))→((q→r)→(p→r))), q↦(p→q) [L3] (((q→r)→((p→q)→(p→r)))→(((q→r)→(p→q))→((q→r)→(p→r)))) by substituton of [A2] with p↦(q→r), q↦(p→q), r↦(p→r) [L4] (((q→r)→((p→(q→r))→((p→q)→(p→r))))→(((q→r)→(p→(q→r)))→((q→r)→((p→q)→(p→r))))) by substituton of [A2] with p↦(q→r), q↦(p→(q→r)), r↦((p→q)→(p→r)) [L5] (((p→(q→r))→((p→q)→(p→r)))→((q→r)→((p→(q→r))→((p→q)→(p→r))))) by substituton of [A1] with p↦((p→(q→r))→((p→q)→(p→r))), q↦(q→r) [L6] ((p→q)→((q→r)→(p→q))) by substituton of [A1] with p↦(p→q), q↦(q→r) [L7] ((p→(q→r))→((p→q)→(p→r))) by substituton of [A2] with p↦p, q↦q, r↦r [L8] ((q→r)→(p→(q→r))) by substituton of [A1] with p↦(q→r), q↦p [L9] ((q→r)→((p→(q→r))→((p→q)→(p→r)))) by detachment of [L5] and [L7] [L10] (((q→r)→(p→(q→r)))→((q→r)→((p→q)→(p→r)))) by detachment of [L4] and [L9] [L11] ((q→r)→((p→q)→(p→r))) by detachment of [L10] and [L8] [L12] (((q→r)→(p→q))→((q→r)→(p→r))) by detachment of [L3] and [L11] [L13] ((p→q)→(((q→r)→(p→q))→((q→r)→(p→r)))) by detachment of [L2] and [L12] [L14] (((p→q)→((q→r)→(p→q)))→((p→q)→((q→r)→(p→r)))) by detachment of [L1] and [L13] [L15] ((p→q)→((q→r)→(p→r))) by detachment of [L14] and [L6]
Proof by Tableau method is here.
[L1] (((q→r)→((p→(q→r))→((p→q)→(p→r))))→(((q→r)→(p→(q→r)))→((q→r)→((p→q)→(p→r))))) by substituton of [A2] with p↦(q→r), q↦(p→(q→r)), r↦((p→q)→(p→r)) [L2] (((p→(q→r))→((p→q)→(p→r)))→((q→r)→((p→(q→r))→((p→q)→(p→r))))) by substituton of [A1] with p↦((p→(q→r))→((p→q)→(p→r))), q↦(q→r) [L3] ((p→(q→r))→((p→q)→(p→r))) by substituton of [A2] with p↦p, q↦q, r↦r [L4] ((q→r)→(p→(q→r))) by substituton of [A1] with p↦(q→r), q↦p [L5] ((q→r)→((p→(q→r))→((p→q)→(p→r)))) by detachment of [L2] and [L3] [L6] (((q→r)→(p→(q→r)))→((q→r)→((p→q)→(p→r)))) by detachment of [L1] and [L5] [L7] ((q→r)→((p→q)→(p→r))) by detachment of [L6] and [L4]
Proof by Tableau method is here.
[L1] (((p→(q→r))→((q→(p→(q→r)))→(q→(p→r))))→(((p→(q→r))→(q→(p→(q→r))))→((p→(q→r))→(q→(p→r))))) by substituton of [A2] with p↦(p→(q→r)), q↦(q→(p→(q→r))), r↦(q→(p→r)) [L2] (((q→(p→(q→r)))→(q→(p→r)))→((p→(q→r))→((q→(p→(q→r)))→(q→(p→r))))) by substituton of [A1] with p↦((q→(p→(q→r)))→(q→(p→r))), q↦(p→(q→r)) [L3] ((q→((p→(q→r))→(p→r)))→((q→(p→(q→r)))→(q→(p→r)))) by substituton of [A2] with p↦q, q↦(p→(q→r)), r↦(p→r) [L4] ((p→(q→r))→(q→(p→(q→r)))) by substituton of [A1] with p↦(p→(q→r)), q↦q [L5] ((q→(((p→(q→r))→(p→q))→((p→(q→r))→(p→r))))→((q→((p→(q→r))→(p→q)))→(q→((p→(q→r))→(p→r))))) by substituton of [A2] with p↦q, q↦((p→(q→r))→(p→q)), r↦((p→(q→r))→(p→r)) [L6] ((((p→(q→r))→(p→q))→((p→(q→r))→(p→r)))→(q→(((p→(q→r))→(p→q))→((p→(q→r))→(p→r))))) by substituton of [A1] with p↦(((p→(q→r))→(p→q))→((p→(q→r))→(p→r))), q↦q [L7] (((p→(q→r))→((p→q)→(p→r)))→(((p→(q→r))→(p→q))→((p→(q→r))→(p→r)))) by substituton of [A2] with p↦(p→(q→r)), q↦(p→q), r↦(p→r) [L8] ((p→(q→r))→((p→q)→(p→r))) by substituton of [A2] with p↦p, q↦q, r↦r [L9] (((p→(q→r))→(p→q))→((p→(q→r))→(p→r))) by detachment of [L7] and [L8] [L10] (q→(((p→(q→r))→(p→q))→((p→(q→r))→(p→r)))) by detachment of [L6] and [L9] [L11] ((q→((p→(q→r))→(p→q)))→(q→((p→(q→r))→(p→r)))) by detachment of [L5] and [L10] [L12] ((q→((p→q)→((p→(q→r))→(p→q))))→((q→(p→q))→(q→((p→(q→r))→(p→q))))) by substituton of [A2] with p↦q, q↦(p→q), r↦((p→(q→r))→(p→q)) [L13] (((p→q)→((p→(q→r))→(p→q)))→(q→((p→q)→((p→(q→r))→(p→q))))) by substituton of [A1] with p↦((p→q)→((p→(q→r))→(p→q))), q↦q [L14] ((p→q)→((p→(q→r))→(p→q))) by substituton of [A1] with p↦(p→q), q↦(p→(q→r)) [L15] (q→(p→q)) by substituton of [A1] with p↦q, q↦p [L16] (q→((p→q)→((p→(q→r))→(p→q)))) by detachment of [L13] and [L14] [L17] ((q→(p→q))→(q→((p→(q→r))→(p→q)))) by detachment of [L12] and [L16] [L18] (q→((p→(q→r))→(p→q))) by detachment of [L17] and [L15] [L19] (q→((p→(q→r))→(p→r))) by detachment of [L11] and [L18] [L20] ((q→(p→(q→r)))→(q→(p→r))) by detachment of [L3] and [L19] [L21] ((p→(q→r))→((q→(p→(q→r)))→(q→(p→r)))) by detachment of [L2] and [L20] [L22] (((p→(q→r))→(q→(p→(q→r))))→((p→(q→r))→(q→(p→r)))) by detachment of [L1] and [L21] [L23] ((p→(q→r))→(q→(p→r))) by detachment of [L22] and [L4]
Proof by Tableau method is here.