Analytic combinatory calculi and the elimination of transitivity (Q1879319)

The author of this paper develops a system of combinatory equality, which is equivalent to standard systems, but does not require the transitivity rule. The new system allows a very simple proof of the Church-Rosser property and a simpler proof of the leftmost reduction theorem. When extensionality is added to the new equational system however, transitivity is no longer provable, although it still is for some weaker systems such as BCK combinatory-equality.