*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 10 May 2010 09:04:43 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1273484055.2555.16.camel@kirk>*References*: <1273267675.11358.4.camel@kirk> <q2gcc2478ab1005080940yc3652e94r557a2ecea600e821@mail.gmail.com> <1273484055.2555.16.camel@kirk>*Sender*: huffman.brian.c at gmail.com

On Mon, May 10, 2010 at 2:34 AM, Joachim Breitner <mail at joachim-breitner.de> wrote: > This poses a new question: What foundation should I use? As a > mathematician, I’d first say that set theory is the correct base to > formalize pure math on – but does it really matter? Will I have problems > convincing other mathematician to trust a formalized proof on Higher > Logic? > > Are the provable theorems within, say, pure algebra the same in either > systems, just with different proofs? If so, is this fact proven? Or is > it indeed necessary to prove results in either system? There should be no problem for mathematicians to trust Higher Order Logic, since there is a straightforward model of HOL in set theory. In fact, Alexander Krauss and Andreas Schropp have an upcoming paper where they describe an automatic translation from Isabelle/HOL to Isabelle/ZF: http://www4.in.tum.de/~krauss/holzf/ On the other hand, there is no model of ZF in HOL (unless you add a bunch of new axioms to HOL) so there is no translation the other way. In particular, many constructions in set theory using the axiom of replacement are impossible to represent in HOL (the cardinalities just get too big). In practice, using HOL is usually nicer than using ZF, since the automation is better (automatic type checking/type inference, for example). And in Isabelle, the libraries and tools are much more well developed in Isabelle/HOL compared to Isabelle/ZF. > Does the AFP also accept Isabelle/ZF submissions? There aren't any Isabelle/ZF submissions yet, but I'm sure they would be welcome. - Brian

**References**:**[isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Joachim Breitner

**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Brian Huffman

**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Joachim Breitner

- Previous by Date: [isabelle] ITP/FLoC early registration, program
- Next by Date: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Previous by Thread: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Next by Thread: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list