Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Suggestions for new formalizations on mathemat...


view this post on Zulip Email Gateway (Jan 14 2023 at 21:07):

From: Javier Diaz <cl-isabelle-users@lists.cam.ac.uk>
Dear mailing list,

I've been an Isabelle user for several years now and am passionate about
mathematical logic. I'm aware that there are lots of formalized results
regarding mathematical logic in Isabelle; however, I'd like to contribute
with a new formaization on this field. Is there some specific topic you
would suggest?

Thanks a lot in advance.
Kindest regards,
Javier

view this post on Zulip Email Gateway (Jan 15 2023 at 15:40):

From: Javier Diaz Manzi <javier.diaz.manzi@gmail.com>
Dear Isabelle users,

I'm passionate about mathematical logic and Isabelle. I'm aware that there
are lots of formalized results regarding mathematical logic in Isabelle;
however, I'd like to contribute with a new formaization on this field. Is
there some specific topic you would suggest?

Thanks a lot in advance.
Kindest regards,
Javier

view this post on Zulip Email Gateway (Jan 15 2023 at 20:09):

From: Ken Kubota <mail@kenkubota.de>
Quantification over types would allow for the natural expression of many mathematical fields such as abstract algebra (e.g., group theory).
Two logics are Peter B. Andrews’ logic Q (not to be confused with Q0) and Tom Melham’s Extended HOL, see p. 1 box 3.1. here: https://owlofminerva.net/files/fom_2018.pdf
R0 uses lambda for type abstraction, as suggested by Mike Gordon (but implemented independently of his idea): https://owlofminerva.net/the-mathematical-logic-r0/

Kind regards,

Ken Kubota


Ken Kubota
https://doi.org/10.4444/100

view this post on Zulip Email Gateway (Jan 16 2023 at 12:39):

From: Makarius <makarius@sketis.net>
How is this relevant to formalizations in Isabelle/HOL at all?

Makarius

view this post on Zulip Email Gateway (Jan 16 2023 at 16:41):

From: Ken Kubota <mail@kenkubota.de>
It would be an extension of Isabelle/HOL or an alternative to Isabelle/HOL with greater expressive power.

Isabelle/HOL is, if I’m not mistaken, Isabelle’s implementation of Mike Gordon’s HOL,
which is basically a polymorphic variant of Church’s simple type theory, i.e., Church’s logic extended by free (unquantified) type variables.

So the suggestion is not to add new formalizations of particular theories _within_ Isabelle/HOL,
but to to formalize a _new object-logic_ like Isabelle/HOL within Isabelle’s meta-logic
(using the terminology from https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf),
which would be, for example, called Isabelle/ExtendedHOL (Tom Melham’s logic) or Isabelle/Q (Peter B. Andrews’ logic),
and much more powerful than Isabelle/HOL, and hence overcome some of the known limitations of HOL.

Mike Gordon himself had announced explicit quantification over types for HOL in 2000 ("future versions of HOL [...] terms of the
form ∀α.t (where α is a type variable)"), and proposed lambda abstraction for HOL in 2001 ("λ-terms like λα. λx:α. x"),
but unfortunately this never materalized.

Kind regards,

Ken Kubota


Ken Kubota
https://doi.org/10.4444/100

view this post on Zulip Email Gateway (Jan 16 2023 at 17:47):

From: Makarius <makarius@sketis.net>

Am 16.01.2023 um 13:38 schrieb Makarius <makarius@sketis.net>:

How is this relevant to formalizations in Isabelle/HOL at all?

The short answer: this is irrelevant to formalizations in Isabelle/HOL.

Makarius

view this post on Zulip Email Gateway (Jan 16 2023 at 17:53):

From: Ken Kubota <mail@kenkubota.de>
Dear Javier,

Concerning Tom Melham’s Extended HOL, I believe he will be able to give some hints on implementation directly if you contact him: https://www.cs.ox.ac.uk/tom.melham/
He had sent me his article after I presented my idea on the HOL-info mailing list, so I believe he will help in some way.

Tom Melham’s paper heavily draws on Peter B. Andrews’ logic Q, so although Peter is retired, I'd make an attempt and ask him for hints, not only concerning implementing Q, but also how to implement a natural deduction variant: https://gtps.math.cmu.edu/andrews.html

Both his logics Q0 and Q are Hilbert-style systems, which means that for a practical implementation a natural deduction variant must be formulated.
Cris Perdue successfully created a natural deduction software implementation of Peter B. Andrews’ logic Q0: https://prooftoys.org/about/
So in practical terms he might a person to collaborate with for a concrete implementation.
You might have a look at his websites prooftoys.org and mathtoys.org.
The interactive example was quite impressive when I had a look at it, but it seems broken at the moment: https://mathtoys.org/simplify.html
He is also active in the Metamath project: https://groups.google.com/g/metamath

Thierry Arnoux implemented Q0 in Metamath: https://github.com/tirix/q0.mm
Maybe he might be interested in a formalization of Q (or Tom Melham’s Extended HOL) in Isabelle.

I could make my paper on R0 available online, but being neither an Isabelle expert nor too familiar with natural deduction systems, and due to constraints imposed by other projects I cannot make a promise for any enduring commitment besides answering questions from time to time.

Best regards,

Ken Kubota


Ken Kubota
https://doi.org/10.4444/100

view this post on Zulip Email Gateway (Jan 16 2023 at 19:28):

From: Ken Kubota <mail@kenkubota.de>
Technically speaking, yes, but the question's implication itself is very problematic.

Why should somebody confine oneself to the obsolete and obviously impoverished type system of HOL (Church's logic, slightly modified)?
Why should the scientific community blatantly ignore the obviously correct hints from Mike Gordon, the founder of HOL, on future developments?

The limitations of HOL are well known, criticized by many people (Freek Wiedijk: "The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra." / John Harrison et al.: "Another limitation of the simple HOL type system is that there is no explicit quantifier over polymorphic type variables, which can make many standard results like completeness theorems and universal properties awkward to express").

For example, with lambda abstraction over types the fact that (Z, +) is a group can be expressed naturally as
Grp Z +
which is what a mathematician wants. But this is not possible in HOL.

My example was formally proving the theorem
Grp o XOR
expressing the fact that (o, XOR) is a group: https://www.owlofminerva.net/files/formulae.pdf#page=420 (wff 6955 = XorGroup)

For the group definition see https://www.owlofminerva.net/files/formulae.pdf#page=362 (wff 266 = Grp)
and for some explanation https://sympa.inria.fr/sympa/arc/coq-club/2022-06/msg00025.html

Of course, from an engineering perspective (for practical purposes like smart card applications), formalizing/automating HOL theorems or theorems of first-order logic still has its legitimacy.

But from a scientific perspective, formalizing/automating 1940 type theory has its limits.


Ken Kubota
https://doi.org/10.4444/100

view this post on Zulip Email Gateway (Jan 16 2023 at 20:08):

From: Rob Arthan <rda@lemma-one.com>
Dear All,

A couple of points in this connection:

1) Maybe it has already been mentioned in this thread, but if not, people should be aware of Peter Homeier’s HOL Omega, which attempts to address the issue under debate (and I think was in part inspired by Mike Gordon’s observations about lambda-abstraction over types).

2) With the existing polymorphism, you can define classes of structures such as “all groups”, because that doesn’t require anything more than an outermost universal quantifier over type variables, which is what HOL as is gives you. (E.g., see my paper on group theory in ProofPower-HOL: http://www.lemma-one.com/ProofPower/examples/wrk068.pdf.) However, I agree that there are many useful properties that are best specified using more general quantification over types.

Regards,

Rob.

view this post on Zulip Email Gateway (Jan 18 2023 at 16:37):

From: Javier Diaz Manzi <javier.diaz.manzi@gmail.com>
Dear Ken,

Thanks a lot for your response. The logics that you referred to look very
interesting and I'd certainly love to collaborate in their Isabelle
formalizations. Is there any ongoing project that I could join or any other
way to collaborate?

Looking forward to your kind response.
Best regards,
Javier

El dom, 15 ene 2023 a la(s) 17:09, Ken Kubota (mail@kenkubota.de) escribió:


Last updated: Mar 29 2024 at 08:18 UTC