I am aware of the lambda cube which gives an ordering to several variants of the lambda calculus. My intuition says that this ordering should have the following property:

For logics $A,B\in\lambda\textrm{-cube}$, $A\le B$ iff there is a mapping $f$ such that formula $x$ can be inferred in $A$ iff formula $f(x)$ can be inferred in $B$. Specifically, $f(x)=x$ for languages in the $\lambda\textrm{-cube}$, but could be non-trivial in an extended ordering.

Is this correct? And is there an extended version of this ordering that applies to a larger set of logical systems?

Then, if such an ordering exists, does it have a greatest element? And what logical system could we use to prove all of this, as (I think) we are operating at a metalogical level?

  • $\begingroup$ This mostly doesn't make sense. There are no "formulas" in the typed lambda calculi of the lambda cube. It's also unclear what you mean by "inferred". I assume something like "proven". Perhaps, via a CH lens, you want to talk about types and a mapping between types and whether they are inhabited or not. Still, you'd need some constraints on $f$ or else it's basically meaningless. What stops me from choosing $f$ as mapping every thing to just two types, one inhabited the other not, as appropriate? $\endgroup$ – Derek Elkins Apr 1 at 9:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.