# What is the corresponding lambda-calculus / proof terms of intuitionistic first order logic? (looking for references)

It is an oft-repeated result that lambda calculi correspond to logics. In particular, recall the following (approximate) relationships

• intuitionistic propositional logic ⇄ simply typed lambda calculus
• intuitionistic second order logic (without first order quantification) ⇄ System F

My general question is: what is the corresponding lambda calculus to intuitionistic first order logic?

The key missing feature is terms for the quantification over objects from a universe of individuals. Thus we can solve the general question by just taking the STLC and adding terms that introduce and eliminate such quantifiers.

However, what I'm really after is papers/results developing this calculus and its theory. I feel like I've seen such a paper in the past, but I can't find it now.

Thus, my specific questions are the following: what is the lambda calculus corresponding to IFOL? Is there any interesting theory about it? Are there any papers about it? How does it interact with the lambda cube?

P.S. I also note that this question has been asked before in the question What order logic does a system correspond to under Curry–Howard correspondence?, but I find the answer unsatisfying, as it's just speculation.

• From what I could find there's this. Commented Aug 1 at 7:50

Intuitionistic first-order logic corresponds to dependent types: propositions quantify over elements ∀(x : A), P where x may occur in P (in other words, "the type P depends on x"). This is the system called λP in the lambda cube.