Email Gateway (Aug 22 2022 at 12:24): Email Gateway (Aug 22 2022 at 12:24):From: dimitri@math.uni-bonn.de
Hello all,
since this is my first post in this mailing list, I will shortly introduce
myself. My name is Ioanna Matilde Dimitriou, and I work with the
mathematical logic group of Bonn, on formalising ZF/NBG-Set Theory in
Isabelle/HOL, in a "natural" style, i.e., as in a standard textbook.
We do this to understand the interplay between Isabelle's, ZF's, and NBG's
logics, to be able to use Sledgehammer (which to our knowledge is only
written for HOL), and to explore the controlled natural language parsing
possibilities in such a setting. For the first goal we chose to revisit
Lawrence Paulson's "/ZF/Constructible/AC_in_L.thy", which is a large and
challenging metamathematical formal proof, and which states that the Axiom
of Choice (AC) is true in L, the universe of constructible sets.
We quickly realised that AC holds in Isabelle/HOL, in fact it is a lemma
in "A Proof Assistant for Higher Order Logic" by Nikpow, Paulson, and
Wenzel (page 87 of the 2015 version).
Is there any way to completely "turn off" AC in Isabelle/HOL? If not,
could you please give me some pointers to the direction of writing a
Sledgehammer for Isabelle/Pure, Isabelle/FOL, or Isabelle/ZF?
Thank you in advance,
Ioanna
Email Gateway (Aug 22 2022 at 12:35):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle/HOL introduces the axiom of choice fairly late in the development (contrast with other HOL implementations, which include it as part of the basic axiomatic set up), but from that point onwards, it gets intertwined with everything. It would be better if you chose a development involving AC, something to do with cardinals perhaps, or simply some of the more obscure consequences of AC.
Larry Paulson
Email Gateway (Aug 22 2022 at 12:37):From: Christian Sternagel <c.sternagel@gmail.com>
Correct me if I am wrong, but my impression is that sledgehammer (via
metis) has (at least a variant of) the "Axiom of Choice" built-in. And I
think the same holds true for any tool that employs Skolemization.
E.g.
lemma "ALL x. EX y. P x y ==> EX f. ALL x. P x (f x)" by metis
cheers
chris
Email Gateway (Aug 22 2022 at 12:38):From: Buday Gergely <gbuday@karolyrobert.hu>
Larry Paulson wrote:
Her research page tells me that her research goal is especially discovering how far one can get without the axiom of choice.
Might it be that Isabelle/ZF is better for her aim?
Email Gateway (Aug 22 2022 at 12:40):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Chris,
This is true, but only if you have loaded "Hilbert_Choice". Before that, "metis" will fail to prove the above, because it has to rely on a weaker skolemizer. And Sledgehammer is simply not available.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 12:41):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle/ZF is surely best for developments in axiomatic set theory. But there is no sledgehammer there.
Larry
Email Gateway (Aug 22 2022 at 12:43):From: Ioanna Dimitriou <dimitri@math.uni-bonn.de>
Thank you all for your answers.
Correct me if I am wrong, but my impression is that sledgehammer (via
metis) has (at least a variant of) the "Axiom of Choice" built-in. And I
think the same holds true for any tool that employs Skolemization.
Isabelle/HOL introduces the axiom of choice fairly late in the development (contrast with other HOL implementations, which include it as part of the basic axiomatic set up), but from that point onwards, it gets intertwined with everything. It would be better if you chose a development involving AC, something to do with cardinals perhaps, or simply some of the more obscure consequences of AC.
I think that if we have a primitive type "Class" of classes with a
subtype "Set" of sets, and some axioms for them, say NBG without choice,
then we can still work in a theory that involves the axiom of choice
without deducing that certain choice functions and Skolem functions
(which exist in HOL) have type "Class". This is similar to constructing
a "model" of (ZF+notAC ) while working in (ZF+AC), which is not
problematic at all.
So, unless I'm mistaken, I don't think that working with HOL is
problematic in itself, though we now have to put some work in defining
FOL-formulas with class parameters in order to get Class Separation in
our theory NGB, and then somehow carefully "connect" these formulas to
formulas in HOL. If we didn't have AC at all, then we could be more
flexible with rules that deduce that certain metafunctions ("Set =>
bool") have representations of type Class.
Her research page tells me that her research goal is especially discovering how far one can get without the axiom of choice.
Might it be that Isabelle/ZF is better for her aim?
Though I personally enjoy working without AC, or between AC and notAC,
the research goal for the project I mentioned in the last post is to
formalise ZF(C) (or NBG(C)) in a way that appears natural to a working
mathematician (like in a textbook). Paulson's proof of AC in L is
particularly interesting because of the metamathematical arguments which
are so commonplace in set theory. In the Bonn logic group we think that
HOL is more suitable for this task, because of the shorter proof steps,
the meta-arguments that become easier when one can talk about classes,
because of the large HOL-libraries we can learn from, and because of
Sledgehammer.
Having said that, I would also like to compare the two logics (HOL vs
ZF) with respect to formalising ZF(C) in a "natural" way. For this, I
would really like to be able to use Sledgehammer. That's why I also
asked for some pointers in the direction of writing a Sledgehammer for
FOL. Perhaps this has been done already, or there is a detailed
explanation of Sledgehammer somewhere? Otherwise, do I just have to
understand the code in Sledgehammer.thy?
Best wishes,
Ioanna
Email Gateway (Aug 22 2022 at 12:44):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm suspicious of this suggestion. Something tells me that AC (which is available for all types) will contaminate the new types that you introduce. This raises the question however of solving your problem using type classes, whether we could allow types that do not assume AC to coexist beside the others.
Larry Paulson
Email Gateway (Aug 22 2022 at 12:45):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey all.
It's nice to be able to avoid the Hilbert_Choice theory, and use only
the definite description operator (The/THE) as opposed to the strong
Hilbert choice operator (Eps/SOME).
I played around with this about a year ago, and discovered that this
doesn't buy you much in modern Isabelle. The lifting and transfer
packages seem to make extensive use of Eps, and pretty much everything
that isn't a natural seems to now use lifting/transfer in the definition
of some primitive functions. Even proofs about naturals seem to depend
on the axiom about Eps because the simprocs about naturals sometimes
coerce to integers, and int/of_nat is defined by lifting/transfer.
At least, that's the impression I got. I might have misunderstood what
was going on.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:46):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
In addition, the BNF (co)datatype package uses "Eps" in a few places. Granted, some of it could be avoided, e.g.
HOLogic.choice_const T $ absdummy T @{term True}
could (and perhaps should) be replaced by
Const (@{const_name undefined}, T)
Jasmin
Last updated: Apr 18 2024 at 12:27 UTC