Re: [isabelle] Formalizations of Free Groups and Matrix Groups?



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.