Javier Diaz (May 26 2024 at 14:50): Javier Diaz (May 26 2024 at 14:50):I'm wondering how typed sets in HOL.Set relate to classical axiomatic set theory, in terms of expressive power, typed vs. untyped, choice of axioms, etc.
James Hanson (May 31 2024 at 17:31):Sets in Isabelle/HOL are always subsets of a given type. In some sense they're really just semantic sugar for Boolean-valued predicates. You can see this in the definition of the set type constructor:
typedecl 'a set
axiomatization Collect :: "('a ⇒ bool) ⇒ 'a set" ― ‹comprehension›
and member :: "'a ⇒ 'a set ⇒ bool" ― ‹membership›
where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
and Collect_mem_eq [simp]: "Collect (λx. member x A) = A"
This is saying that the only way to specify a set of elements of type 'a is to specify a predicate of type 'a ⇒ bool, and the only way to 'probe' a set is to ask what its members are. As such, the axiomatization in HOL/Set.thy isn't going to tell you all that much about the expressiveness of Isabelle/HOL in general.
I'm not sure if I'm really answering your question, but in terms of standard classical mathematical logic terminology, types (especially non-dependent types like those in Isabelle/HOL) are roughly analogous to sorts in something like many-sorted first-order logic. In particular, there is no global quantification; quantifiers are always bound to a given type. Since Isabelle/HOL doesn't have any dependent types and the type forming operations are bounded roughly by the size of a finite number of iterated power sets, the consistency strength and expressive power of Isabelle/HOL should be comparable to bounded Zermelo set theory also known as Mac Lane set theory (i.e., Zermelo set theory with separation only for bounded formulas). This puts it on par with the common theory of elementary toposes. So this means that you shouldn't be able to prove things like Borel determinacy in it without extra assumptions. Since Isabelle/HOL can reason about unspecified types (with type variables like 'a), it should be relatively straightforward to write down assumptions to the effect of ''a encodes a Grothendieck universe,' which would in principle allow you to prove things that need higher consistency strength conditionally, although I could imagine the specifics of something like this being a pain.
Manuel Eberl (Jun 07 2024 at 13:52):Note that back when I started doing Isabelle/HOL (around 2011), 'a set was actually a type synonym for 'a ⇒ bool, but at some point it was changed back to a type of its own. So it really is just a type copy of 'a ⇒ bool, in a sense.
Last updated: Dec 21 2024 at 12:33 UTC