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.
Can I dispense with lambda abstraction in type theory, and what do I lose by doing that?