Variables are finicky. I've been looking at algebraizations of first-order logic recently to figure things out in more detail. Mostly I've been looking at Tarski's Cylindrical algebra but lately I have been looking at modal boolean logic/interior algebra which are simpler versions of the same idea.
Is there any work on constructive interpretations/variations?
I've been playing around a bit myself in PLT Redex getting a feeling for what a constructive look at it might appear like.
The base of these logics consists of Boolean algebras. So a constructive rework could straightforwardly use Cartesian Closed categories and the simply typed lambda calculus as a foundation.
STLC doesn't really seem in the "spirit" of cylindrical logic though but I'm not really sure how you would "cylindrify" lambda binders.
I'm also having trouble understanding the existential as a kind of dependent sum. As well constructively you have to axiomize universal quantification separately instead of encoding via negation which gets confusing.
You would think some variation on System F would be a constructive interpretation of Cylindrical Algebra but I'm having trouble seeing any connection.
It also seems obvious to think of things in terms of locally Cartesian (maybe closed?) categories and subobjects and over categories but unfortunately I'm not really familiar with the language of the topology side of things. To tell the truth most of this category theory stuff goes over my head too.