SE calculus

SE Calculus is a modification of regular SKI combinator calculus to make it much more powerful; as powerful as set theory itself. It removes the K and I combinators and added the new E combinator.

On the surface, we wish to define:

Ewxyz = y if x == y, and Ewxyz = z otherwise

However, the true definition is much more sophisticated as the naive definition is paradoxical: what does it mean for combinator equality? And moreover, the way we define equality can arbitrarily add ridiculous strength.

Definition of the Equality combinator

Creating a "Von Neumann" hierarchy of combinators

The way we define combinators is similar to lambda calculus and the Von Neumann hierarchy. Define V₀ as the set containing only the combinator Q_∅, which maps everything to S.

Define Q_I (where I is a set) to be the combinator that maps everything inside I to E, and everything else to S. Note that we care about intrinsic equality when talking about membership. For example, Q_∅ is different from KS in SKI calculus.

Define V_b as the set containing all the combinators Q_I, where I is a subset of the union of all V_c for all c<b.

Finally, define V to be the union of all V_b for ordinal b.

Defining Equality for E

 Ewxyz = y if for all k in V, there exist a sequence of beta reduction that reduces wk to A, xk to also A, where A is some tree of combinators (which may contain S, E, or QI)

Computational Class

Immediately we see

ESSyz = Kyz = y
EESSz = Iz = z

This means we can implement all combinators from SKI calculus, making this Turing-complete. However, we can implement more operators, specifically set membership and universal quantifier. Define E as TRUE and S as FALSE. Some examples:

EEx = CHURCH_TRUE if x==E and CHURCH_FALSE if x==S.
Qxy = E if y∈x and Qxy = S otherwise
E(λx.P(x))E = CHURCH_TRUE if ∀(x∈V).P(x) and E(λx.P(x))E = CHURCH_FALSE otherwise

This means that SE Calculus is as least as powerful as first order set theory.

Paradoxical combinators

It might be possible that the call tree is infinitely deep or we get paradoxical self-expression (a set that contains X if and only if it doesn't contain X). We ignore all of these paradoxical combinators. If anything of such happens or can possibly happen, we destroy the universe.

What model of set theory are we using

See the discussion here.