Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- From: Christian Sternagel <c.sternagel at gmail.com>
- Date: Tue, 2 Feb 2016 12:31:36 +0100
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.0
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.
lemma "ALL x. EX y. P x y ==> EX f. ALL x. P x (f x)" by metis
On 01/26/2016 09:16 PM, dimitri at math.uni-bonn.de wrote:
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and