So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm wondering if I really need lambda abstraction to use it. I understand that you can use these lambda operators to construct quantifiers, logical connectives, and the like. But do we need them or can we just use type construction on its own and create quantifiers and operators that work on terms that return a propositional type, using ordinary classical logic?
This seems more straightforward for me coming from my familiarity with logic over lambda calculus, and the logic constructed with lambda calculus seems a bit unnatural, along with it being weaker than classical logic.
Question:
Can I dispense with lambda abstraction in type theory, and what do I lose by doing that?
Unlike set theory, where sets taken as the most fundamental objects, type theory takes functions as the first-class mathematical objects. Then we obviously need something like a function type to work on. But how to construct inhabitants of this type? By $\lambda$-abstraction, which is what we call the function type constructor.
Let $b$ be an inhabitant of a type $B$ under the assumption that $x$ is an inhabitant of $A$, that is
$x : A \vdash b : B$
Then we can construct an inhabitant of the function type $A \to B$ by $\lambda$-abstraction on $b$:
$\vdash \lambda x.b: A\rightarrow B$
You ask what you lose if you remove $\lambda$-abstraction. The straightforward answer is that you can no longer construct elements of the function type. Since there is no such thing as a free lunch, we would have to replace it with something else.
One of the most remarkable alternatives is the notion of a combinator from combinatory logic. It eliminates the need of bound variables by using primitive high-order functions called combinators, some of which are
$$I : A \to A $$ $$K : A \to (B \to A) $$ $$S : (A \to (B \to C)) \to (A \to B) \to (A \to C) $$
for any types $A, B, C$.
Now rather than using lambda-abstraction, functions are constructed out of combinators. But note that the notion of $\lambda$-abstraction is still here under the hood. In particular,
$$I := \lambda x. x$$ $$K := \lambda x.\lambda y. x$$ $$S := \lambda f. \lambda g. \lambda x. (f x) (g x) $$