Ant S. (Apr 22 2026 at 23:39): Ant S. (Apr 22 2026 at 23:39):Kevin Kappelmann said:
Meta-level forall and implication are typically nicer to work with in Isar (Isabelle's structured proof language) and most proof methods. Rule of thumb: use them in theorem statements whenever you can.
So meta forall is the way to go in theorem statements.
Consider this contrived example (that I wish to prove using the well-ordering property)
theorem induction: "⟦ P(0::nat); (∀ n :: nat. P(n) ⟶ P(n + 1)) ⟧ ⟹ (∀n. P(n))"
why is it better to use metalogical forall than that of the object logic? in fact, why make the distinction? if the metalogic is HOL, is the object logic Pure?
Mathias Fleury (Apr 23 2026 at 04:21):Use the metalogical forall as much as possible
Mathias Fleury (Apr 23 2026 at 04:22):Basically, the only exception are definitions of invariants and properties, because using type bool makes those properties easier to compose
Kevin Kappelmann (Apr 23 2026 at 09:50):Ant S. said:
why is it better to use metalogical forall than that of the object logic? in fact, why make the distinction? if the metalogic is HOL, is the object logic Pure?
(1) Because many tools work with meta level quantifiers and implications and not HOL's object logic quantifiers and implications.
(2) Because there is a meta logic (Isabelle/Pure) which has quantifiers and implications and there are several object logics (Isabelle/HOL, Isabelle/FOL, etc.) with their own logical operators separate from the meta logic ones (e.g. the quantifiers in Isabelle/FOL only quantify first-order entities).
(3) Pure is the meta logic, HOL is one of the object logics.
Ant S. (Apr 23 2026 at 09:52):yeah I flipped (3) by mistake
Last updated: May 05 2026 at 02:56 UTC