Axiom: PL1: p>(q>p) [CpCqp]

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))

[Zeman, 1973, page 8]

Go to ...

© Copyright 2004 by John Halleck, All Rights Reserved.
This page is
This page was last modified on August 18th, 2006.