If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend that to second order logic by allowing quantification of predicate variables and function variables. Beyond that I can extend quantification to functions that have higher order types as arguments, such as a third order predicate that takes a second order function or predicate.
This, as I understand it, is equivalent to the simply typed lambda calculus. We can further extend this logic to include some sort of notion of type quantification to obtain a polymorphic lambda calculus, which seems quite powerful to me. Looking it up takes me to the entry on the 'lambda cube' which has 8 strongly normalizing lambda calculi, with the simply typed lambda calculus on the bottom and the calculus of constructions on the top.
I don't quite understand this; What does it mean to be at the 'top' of the cube? Reading about the calculus of constructions, it's presented as a constructive calculus which I thought to be strictly weaker than simply typed lambda calculus or the polymorphic second order lambda calculus. I would have thought that adding capacity to represent terms and types would make a system stronger rather than weaker.
I'm primarily interested in lambda calculi that can be used to construct unifiable propositions (and handling the propositional calculus outside of the lambda expressions rather than using the lambda calculus itself to represent propositional calculus.) Is there anything more general/powerful than the polymorphic second order lambda calculus? Are there lambda calculi outside of the lambda cube that can be used for further abstraction?