Let’s go skiing
Can’t be enacted with only one vote… — Quirck
Adminned at 23 Jun 2013 14:11:19 UTC
Axioms:
* S, K, I, B, C, K, and W are Expors.
* For all Expors x and y, x y is an Expor.
* For all x, $(x) is an Expor, and $’($(x)) = x.
* For all Expors x and y, if [for all Expors z, (x z) = (y z)], then x = y.
* For all Expors x, y and z, ((S x) y) z = (x z) (y z).
* For all Expors x and y, (K x) y = x.
* For all Expors x, I x = x.
* For all Expors x, y and z, ((B x) y) z = x (y z).
* For all Expors x, y and z, ((C x) y) z = (x z) y.
* For all Expors x and y, (W x) y = (x y) y.
See http://en.wikipedia.org/wiki/SKI_combinator_calculus and http://en.wikipedia.org/wiki/B,C,K,W_system. Irreducible Expors, like ((S I) I) ((S I) I), aren’t a problem; they are simply undefined. The only way you could prove a paradox from these axioms is by proving that $(x) = $(y) where x ≠y, and I’m pretty sure you can’t do that, because it’s impossible for two combinator calculus terms to have substantively different reductions,
Skju:
Why have both systems?