Prop, but with universal quantifiers only, or none?

Stream: Is there code for X?

[Paweł Balawender]

Hey, I want to formalize results from reverse mathematics and I have been stuck at the problem of controlling what quantifiers can a logical formula have. Of course I could just define a deep embedding of the logic I am formalizing, so using String for variable names and writing code for binding quantifiers to variables etc., but I still hope I could use Lean's (or other prover's) mechanisms to reason about variable names etc. But Lean's prop doesn't allow us to narrow our reasoning to only logical formulas which have no quantifiers (open formulas), or have only universal quantifiers, or they only have a block of existential quantifiers, then a block of universal quantifiers and then no further quantifiers etc.

One idea I had was to define a type ExistentialFormula (String varname) (OpenFormula formula) := Exists varname such that formula(varname). But it requires me to formalize 'OpenFormula' and I just can't get around it. Do you have any idea how to take a subset of Prop, which doesn't allow quantification? Thanks! :)

[Luigi Massacci]

Depending on what exactly you want to formalize, you can take a look at docs#FirstOrder.Language.BoundedFormula.IsQF (the deep embedding you talk about has already been done in some sense)

[Luigi Massacci]

Otherwise, I'm fairly confindent you will not be able to state any meta-theore about Prop of the kind you'd need.

[Paweł Balawender]

Wow! it even accepts Language as an argument, which is what I need. This look really promising, thank you!