Paweł Balawender (May 05 2025 at 11:14): Paweł Balawender (May 05 2025 at 11:14):Hey, can we somehow limit the logical formulas (like in Isabelle/Pure) from having a quantifier in them? I want to use Isabelle's unification to reason about variable names in formulas etc., but I see that even in Isabelle/Pure, universal and existential quantification is 'on' by default. I want to reason about weaker formulas! I.e. only allow the user to add quantifiers in a particular way and not however they want to. Do you think we can do that in Isabelle? Perhaps I shouldn't even import Pure? :) Thanks!
Fabian Huch (May 05 2025 at 11:21):Pure doesn't have an existential quantifier, but in any case, what do you even want to achieve? You could check whether Pure.all, HOL.All, and HOL.Ex appear in your term, but that doesn't stop anyone from defining another constant that is a quantifier
Mathias Fleury (May 05 2025 at 11:30):Depending on what you are trying to achieve, embedding your terms into HOL might be easier, like in https://www.isa-afp.org/sessions/implicational_logic/#Implicational_Logic
Fabian Huch (May 05 2025 at 11:30):Especially if you want to prove meta-theorems about your formulas
Paweł Balawender (May 05 2025 at 12:13):Hey thank you for the pointers! Embedding into HOL is something I haven't considered, but sounds useful indeed. @Fabian Huch I need to formalize proofs in the area of bounded arithmetics and, more generally, of reverse mathematics. What they do there is to limit the expressiveness of a proof system by restricting the Induction scheme (for every proposition P, if P(0) and P(x)->P(x+1), then forall x, P(x)) to only some smaller class of propositions. For example, you can consider a proof system consisting of classical natural deduction, some constants and axioms (constants 0, 1, +, *, axiom 0+x=x etc.) + an axiom scheme of induction limited to open formulas - that is, having no quantifiers at all, but possibly having free variables. I attach the relevant part of Wikipedia's article on Arithmetical hierarchy for the specific definition of how to they cluster the formulas. All this is very cool and I think formalizing some of these results would help us "convert" a lot of logicians onto our side :) But it seems that implementing these weak systems will require more work than I thought
image.png
Last updated: May 09 2025 at 08:28 UTC