mathlogic.lv Mathematics, Logic, Algorithms

Axiomatic Proof Of Implication's Reflexivity Law

Law of Reflexivity Of Implication is the easiest to understand the proof building mechanics by example.

I provide its axiomatic proof here.

[L1] ((p→((q→p)→p))→((p→(q→p))→(p→p))) by substitution of [A2] with p↦p, q↦(q→p), r↦p
[L2] (p→((q→p)→p)) by substitution of [A1] with p↦p, q↦(q→p)
[L3] ((p→(q→p))→(p→p)) by detachment of [L1] and [L2]
[L4] (p→p) by detachment of [L3] and [A1]

Proof by Tableau method is here.