This is a popular axiom called PL1 by Hilbert, R1 by Russel and Whitehead, C2 by Zeman, and HA1 by Heyting.
This axiom is also called "K", since it corresponds to Curry and Fey's "K" combinator. [Hindley and Meredith, 1990] In terms of combinators it is:
K x y => x
In English it says roughly that if something is true, anything implies it.
ICI = p>(q>p) + (p>(q>r))>((p>q)>(p>r))
© Copyright 2004 by John Halleck, All Rights Reserved. This page is http://www.cc.utah.edu/~nahaj/logic/structures/axioms/CpCqp.html This page was last modified on August 18th, 2006.