Paweł Balawender (Apr 22 2025 at 15:48): Paweł Balawender (Apr 22 2025 at 15:48):Hey, I want to formalize a particular logic in Isabelle, and to study it I need to be able to adjust the power of its formulas. One thing I need is expressing that a logical formula (in a standard language with and, or, etc.) contains no universal quantifiers. I.e. it is of the form Exists a . Exists b . phi(a, b)... Or to express that a formula may or may not have a free variable. I really don't want to deal with name binding on my own - do you think I could use Isabelle's machinery somehow to reason about the logical formulas themselves? I attach a screenshot of the definition of what I'm actually going after, this is definition 4.14 from https://www.karlin.mff.cuni.cz/~krajicek/cook-nguyen.pdf
image.png
Last updated: May 09 2025 at 08:28 UTC