# Iota combinator and implicational propositional calculus

There is are two esoteric languages with minimally functionally complete operators, iota and jot, that are closely related to SK combinators. I'm attempting to understand the relationship between these languages and propositional calculus.

We know $K := P → (Q → P)$ and $S := (P → (Q → R)) → ((P → Q) → (P → R))$

My question is this: Is there a relation between iota $λx.xSK$, jot, or iota prime $λx.xKSK$ with Łukasiewicz's axiom system?

$((P → Q) → R) → (R → P) → (S → P)$

## 1 Answer

The axiom scheme you reference represents a classical logic, i.e. one with excluded middle. The computational interpretation of Peirce's law (implicitly embodied in Łukasiewicz's system) is call/cc. Neither iota nor jot support first-class continuations (or continuations of any sort), so they do not encode or imply Peirce's law.

Added much later:

I think I just now realized that the minimally functionally complete is talking about completeness of logical connectives and had originally thought it had been referring to the completeness of the SK basis. This realization doesn't invalidate my answer but makes it so that there is more to say.

The first thing to say is that functional completeness in the context of propositional logic is (usually) talking about Boolean functions and thus we usually talk about collections of connectives (like $$\to$$ and $$\land$$) being or not being functionally complete. It doesn't really make sense to use it to refer to programming languages which we usually want to be Turing-complete which is a very different notion.

Nevertheless, taking a logical view of the SK combinatory logic, as the question does, the only connective is $$\to$$ which is not functionally complete. This is mentioned on the referenced page on Łukasiewicz's system. That page also strongly implies that Axiom 3 is not derivable from Axiom 1 and Axiom 2 which correspond to $$K$$ and $$S$$ respectively. If true (which it, of course, is), that would mean that the single axiom can't be derived from Axiom 1 and 2 either, since you would then be able to derive Axiom 3. My original paragraph was a high-level argument of why this is the case. A more direct argument would be to provide a counter-model by using a non-classical model of intuitionistic logic which will validate Axioms 1 and 2 but not Axiom 3 and therefore not the single axiom.

As a final note, in the above I've been assuming a typed version of iota and jot which are untyped languages. This is necessary for the logical reading to be meaningful. It is worth noting that a type version of iota and jot would not be Turing-complete.

• "Neither iota nor jot support first-class continuations (or continuations of any sort)" -- counter-intuitive, but interesting. So, one could calculate anything using iota only, but continuations are impossible? – vak Sep 14 '19 at 10:24
• I think I didn't click on the "minimially functionally complete" link before and assumed it referred to completeness of the SK combinators. That makes the question more confused than I originally thought. Either way, Turing-completeness only cares that you have some implementation of every computable function. It doesn't care how you do it. Continuations are just a tool for organizing implementations. – Derek Elkins left SE Sep 14 '19 at 18:58