Hi, thanks! I can't access it but I have read some papers from Jonathan Seldin on Curry's illative approach, which seems to be the key here, e.g. https://people.uleth.ca/~jonathan.seldin/CCL.pdf However, I think he explains this approach has failed and type theory is kind of simpler approach to functionality.

My idea is different than introducing a new special combinator operator. Instead I want to formalize what a "question" is. In type theory, we can formalize any(?) mathematical question as a question of finding a term of a certain type. I want to replace that with a combinator equation Ax=B, where A and B are given lambda terms and x is an unknown. However, with x being any normalizable lambda term this wouldn't work, so I add additional condition that x must be what I call a "primitive term" (I haven't seen it defined anywhere sorry), expressible as a lambda term where only a given number of lambda abstractions occur in the front of the term and no other abstractions in its body, only applications. These are terms expressible in normal form as applications of only arguments, so many of the commonly used combinators are primitive (they don't compose though, for example, Y combinators are not primitive).

By choice of A, we can control the "combinator base" that x accepts inside the equation, so we can restrict the "type" of x that are solutions to the equation. So we can represent the question of y being of type T as a question of there being a primitive term x for an equation Ax=B (i.e. Ax and B both normalize to identical expression), where A and B is chosen based on T and y corresponds to x taking a chosen combinator base (the logic we work with) as arguments.

I was interested in formalizing what a question is, because I think that formalizing mathematics using type theory requires quite large meta-logical apparatus. However, using only untyped lambda calculus (and notion of beta-normalized equation with a primitive unknown) as a replacement for type theory is easy to embed into untyped lambda calculus itself using self-interpretation. The correspondence between the embedded language and the untyped lambda calculus (i.e. description how untyped lambda calculus manifests within the self-interpreter, and how questions are translated) could then be the only metalogical axiom required.

Try Anna's Archive, matey.

Bunder's papers are hard to find. It's been a while, but I think that "illiative" approach is precisely what Bunder tried to articulate. I recall one paper where he proved you could do set their with Combinator Logic and an "element of" operator. I think.