While this axiom has great intuitive appeal, it is not true in all logic systems.
This axiom is often called "I", since it corresponds to Curry and Fey's "I" combinator. [Hindley and Meredith, 1990, pg 91]
In terms of combinators "I" is:
I x => x
(It is part of almost all the usual systems...)
© Copyright 2004 by John Halleck, All Rights Reserved. This page is http://www.cc.utah.edu/~nahaj/logic/structures/axioms/Cpp.html This page was last modified on October 11th, 2005.