Is there an ordering of logical systems defined by reductions?

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?

• 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? – Derek Elkins Apr 1 at 9:06