(p>q)>((r>p)>(r>q)) [CCpqCCrpCrq]

Bibliography: ???

• [Hindley and Meredith, 1990]
• [Chidgey, 1973]

This axiom is also called B, since it corresponds to Curry and Fey's "B" combinator. [Hindley and Meredith, 1990, pg 91] In terms of combinators, B is:
B x y z => X (Y Z)

This axiom is also called "T pre", and like its relative (p>q) > ((q>r)>(p>r)) ("T suf") in the presence of Uniform Substitution and detachment (for >) they yield the rule if |- p>q and |- q>r infer |- p>r . [Chidgey, 1973, page 273]

In the presence of either of the rules:

• From |- p > (q>r) infer |- q > (p>r)
• From |- p > ((q>r)>s) infer |- (q>r) > (r>s)

Or the axiom:

• p > ((p>q) > q)

then T pre and T suf are equivalent. (And not in a whole of other cases -JH) [Chidgey, 1973, page 273]

Go to ...

• Axioms page
• Structures page
• Logic Page
• John Halleck's Home Page

© Copyright 2007 by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/axioms/CCpqCCrpCrq.html
This page was last modified on January 22nd, 2007.