Comment by barryjay

Tree calculus is more expressive, can define more functions, than lambda calculus or traditional combinatory logic. This theorem is so startling, so outrageous, that mere proof, even a formal proof, is not enough to get the message across. This is no one’s fault. To help, I am currently writing a series of conversations, where the characters come at these ideas from many points of view, letting it all hang out. It doesn’t help that the current formal proof of the theorem is indirect. So here is a challenge for you all. Find a direct proof that the node operator of tree calculus is not definable in traditional combinatory logic. That is, no SK-combinator satisfies the equations of tree calculus. Conversely, trying to find such a combinator may give you a better feel for intensionality.