Ant S. (May 19 2026 at 16:05): Ant S. (May 19 2026 at 16:05):There are really two questions here, but I'll write it out as one.
https://isabelle.in.tum.de/dist/library/Pure/Pure-Examples/document.pdf
Here, any embedding of a logic within Pure requires the use of an axiomatization. But I've heard more that axiomatizations are a bad idea since they lead to inconsistency (and that's why people tend to use locales).
Alex Mobius (May 24 2026 at 11:08):Well, you have to use some axioms in any theory :) Axiomatizations are "a bad idea" because you might accidentally become able to prove False, so the more you can construct from a small set of axioms, the better.
Kevin Kappelmann (May 24 2026 at 11:20):Axiomatizations for object logics are so fundamental, that one (or at least I) want them to live globally and not in some locale (of course, one could improve several tools such that it becomes more practical (or even feasible at all -- some axiomatizations are not expressible with locales) and then I wouldn't object).
Ant S. (May 24 2026 at 11:32):What sort of axiomatization wouldn't be feasible in a locale? E.g. typedecls? Since locales don't play nice with monomorphisation iirc
Kevin Kappelmann (May 24 2026 at 11:38):yes, polymorphic constants and type constructors are problematic. Example for the former:
locale test =
fixes id :: "'a ⇒ 'a"
begin
(*Problem: id has type "'a ⇒ 'a" and not "?'a ⇒ ?'a"*)
term "id True"
end
As an aside: has anyone considered improving polymorphism support for locales? And if so, What'd need to be done? I remember reading the Zulip thread talking about that but I don't remember if it went over why
Kevin Kappelmann (May 24 2026 at 12:22):Yes Popescu, Traytel, Buday have some preliminary work on that.
Last updated: Jun 06 2026 at 17:17 UTC