Email Gateway (Jan 27 2025 at 11:30): Email Gateway (Jan 27 2025 at 11:30):From: Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk>
Hello,
In short: Is it possible to make a program using Isabelle so that you give it a mathematical statement in ZFC and FOL and it creates a proof of it and tells you which axioms are used?
I am a Master of Science in statistics. I consider Helmut Strasser's book "Mathematical theory of statistics: Statistical experiments and asymptotic decision theory" as a good background for statistical experiments. I asked Strasser personally and he said that the book is based on ZFC axioms and First order logic. I would then be interested in understanding ZFC axioms so well that from every statement in the book I could say that which specific axioms are needed in the statement in hand. Is this possible to achieve by using Isabelle and have someone already made this?
I was bedazzled by Isabelle when reading this "Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant" (https://link.springer.com/article/10.1007/s10817-021-09599-8). It was fascinating to see how Isabelle could be used to prove Gödel's theorem. I think proof assistants like Isabelle are crucial in understanding mathematics better.
Kind regards,
Lauri Tarpila
Email Gateway (Jan 27 2025 at 11:59):From: Manuel Eberl <manuel@pruvisto.org>
I am perhaps not the perfect person to answer this, but I'll give it a
shot anyway. Perhaps others who are more knowledgeable than me can weigh
in as well.
I would say probably not. I suppose it depends on the complexity of the
proof of the given statement. But first of all, you have to remember
that Isabelle is an interactive proof assistant, not an automated one.
You don't just give it a statement and then it runs for a bit and will
give you a proof (or not). You have to guide the system in small steps.
From a user perspective, I would say that there are two main aspects
where the proof assistant actually "assist" you: one, by telling you, in
any given situation, what you still have to show and what facts you have
available; two, by providing automation to "close the gap" from one step
to the next.
So yes, there is some automation that you could use for that, I imagine
it would be fairly easy to use that to build a tool like you envision
inside Isabelle, by adding or dropping axioms or assumptions, running
the automation (e.g. one of the built-in proof methods or sledgehammer
or whatever) and checking whether a proof comes out. But the big problem
that I see here is that just because the system doesn't find a proof
(within a reasonable amount of time) does of course not mean that there
is no proof. For simple propositional statements, this will probably
work, but already for first-order logic I think it is probably not too
hard to find not-too-complex examples that are provable but take the
automation forever to find a proof. So if you're hoping to apply this to
"real" maths and not just toy examples, I don't think that is realistic.
And you might be better of using an automated theorem prover anyway
(although I think they have similar limitations).
What is more realistic is the following process, which is something that
I think many people who work with ITPs can attest (I suspect that's
what's happening in that Gödel paper you mentioned, too): you formalise
some theorem, either from scratch or based on a paper proof. When you're
done, you start playing around with the assumptions of the theorem;
tighten some of the inequalities, drop some assumptions, generalise the
statement, etc. And then you have a look where the existing proof
breaks. Sometimes it doesn't break at all. Sometimes it breaks in a few
places but with some inspection and/or the automation those places are
easily fixed. It is not rare to find that the paper proofs contain
assumptions that are completely unnecessary, i.e. not just such that the
proof is easily repaired when you remove them, but really not used
anywhere in the proof. Similarly, ITPs allow you to refactor proofs much
more painlessly, because you immediately see what breaks and where.
Dually, you also occasionally find missing assumptions, i.e.
assumptions that you have to add for the paper proof to work, or even
for the theorem to hold in the first place. But that's another story…
Cheers,
Manuel
On 27/01/2025 12:30, Lauri Olli Tarpila (via cl-isabelle-users Mailing
List) wrote:
Hello,
In short: Is it possible to make a program using Isabelle so that you
give it a mathematical statement in ZFC and FOL and it creates a proof
of it and tells you which axioms are used?I am a Master of Science in statistics. I considerHelmut Strasser's
book "Mathematical theory of statistics: Statistical experiments and
asymptotic decision theory" as a good background for statistical
experiments. I asked Strasser personally and he said that the book is
based on ZFC axioms and First order logic. I would then be interested
in understanding ZFC axioms so well that from every statement in the
book I could say that which specific axioms are needed in the
statement in hand. Is this possible to achieve by using Isabelle and
have someone already made this?I was bedazzled by Isabelle when reading this "Distilling the
Requirements of Gödel’s Incompleteness Theorems with a Proof
Assistant"
(https://link.springer.com/article/10.1007/s10817-021-09599-8). It was
fascinating to see how Isabelle could be used to prove Gödel's
theorem. I think proof assistants like Isabelle are crucial in
understanding mathematics better.Kind regards,
Lauri Tarpila
Email Gateway (Jan 27 2025 at 12:51):From: Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Thank you for your answer!
Yes I did not take that into account that indeed even if the statements are in a book which every sentence is provable that the system cannot prove in a reasonable time.
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
But so it seems that this has not been attempted or do the automated theorem provers do this kind of things?
Best regards,
Lauri Tarpila
On Monday, January 27th, 2025 at 1:53 PM, Manuel Eberl <manuel@pruvisto.org> wrote:
I am perhaps not the perfect person to answer this, but I'll give it a shot anyway. Perhaps others who are more knowledgeable than me can weigh in as well.
I would say probably not. I suppose it depends on the complexity of the proof of the given statement. But first of all, you have to remember that Isabelle is an interactive proof assistant, not an automated one. You don't just give it a statement and then it runs for a bit and will give you a proof (or not). You have to guide the system in small steps. From a user perspective, I would say that there are two main aspects where the proof assistant actually "assist" you: one, by telling you, in any given situation, what you still have to show and what facts you have available; two, by providing automation to "close the gap" from one step to the next.
So yes, there is some automation that you could use for that, I imagine it would be fairly easy to use that to build a tool like you envision inside Isabelle, by adding or dropping axioms or assumptions, running the automation (e.g. one of the built-in proof methods or sledgehammer or whatever) and checking whether a proof comes out. But the big problem that I see here is that just because the system doesn't find a proof (within a reasonable amount of time) does of course not mean that there is no proof. For simple propositional statements, this will probably work, but already for first-order logic I think it is probably not too hard to find not-too-complex examples that are provable but take the automation forever to find a proof. So if you're hoping to apply this to "real" maths and not just toy examples, I don't think that is realistic. And you might be better of using an automated theorem prover anyway (although I think they have similar limitations).
What is more realistic is the following process, which is something that I think many people who work with ITPs can attest (I suspect that's what's happening in that Gödel paper you mentioned, too): you formalise some theorem, either from scratch or based on a paper proof. When you're done, you start playing around with the assumptions of the theorem; tighten some of the inequalities, drop some assumptions, generalise the statement, etc. And then you have a look where the existing proof breaks. Sometimes it doesn't break at all. Sometimes it breaks in a few places but with some inspection and/or the automation those places are easily fixed. It is not rare to find that the paper proofs contain assumptions that are completely unnecessary, i.e. not just such that the proof is easily repaired when you remove them, but really not used anywhere in the proof. Similarly, ITPs allow you to refactor proofs much more painlessly, because you immediately see what breaks and where.
Dually, you also occasionally find missing assumptions, i.e. assumptions that you have to add for the paper proof to work, or even for the theorem to hold in the first place. But that's another story…
Cheers,
Manuel
On 27/01/2025 12:30, Lauri Olli Tarpila (via cl-isabelle-users Mailing List) wrote:
Hello,
In short: Is it possible to make a program using Isabelle so that you give it a mathematical statement in ZFC and FOL and it creates a proof of it and tells you which axioms are used?
I am a Master of Science in statistics. I consider Helmut Strasser's book "Mathematical theory of statistics: Statistical experiments and asymptotic decision theory" as a good background for statistical experiments. I asked Strasser personally and he said that the book is based on ZFC axioms and First order logic. I would then be interested in understanding ZFC axioms so well that from every statement in the book I could say that which specific axioms are needed in the statement in hand. Is this possible to achieve by using Isabelle and have someone already made this?
I was bedazzled by Isabelle when reading this "Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant" (https://link.springer.com/article/10.1007/s10817-021-09599-8). It was fascinating to see how Isabelle could be used to prove Gödel's theorem. I think proof assistants like Isabelle are crucial in understanding mathematics better.
Kind regards,
Lauri Tarpila
Email Gateway (Jan 27 2025 at 13:22):From: Joe Wells <cl-isabelle-users@lists.cam.ac.uk>
dear lauri,
i think your question should instead be: “can this piece of mathematics be proven with substantially less powerful axioms than zfc and fol? how much weaker can we make the axioms and still prove this?”
for example, much of mathematics doesn't need the axiom of replacement.
a bigger issue that you will face is that much of current work with interactive provers does not start from the axioms of zfc but instead is based on systems like, for example, the calculus of inductive constructions. of the major interactive provers, isabelle/hol seems to me to be the closest to typical mathematics yet most work in isabelle/hol is not founded on the axioms of zfc.
i hope this perspective is somehow useful.
best wishes,
joe
On 1/27/25 12:51, Lauri Olli Tarpila (via cl-isabelle-users Mailing List) wrote:
Hi,
Thank you for your answer!
Yes I did not take that into account that indeed even if the statements are in a book which every sentence is provable that the system cannot prove in a reasonable time.
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
But so it seems that this has not been attempted or do the automated theorem provers do this kind of things?
Best regards,
Lauri Tarpila
On Monday, January 27th, 2025 at 1:53 PM, Manuel Eberl <manuel@pruvisto.org><mailto:manuel@pruvisto.org> wrote:
I am perhaps not the perfect person to answer this, but I'll give it a shot anyway. Perhaps others who are more knowledgeable than me can weigh in as well.
I would say probably not. I suppose it depends on the complexity of the proof of the given statement. But first of all, you have to remember that Isabelle is an interactive proof assistant, not an automated one. You don't just give it a statement and then it runs for a bit and will give you a proof (or not). You have to guide the system in small steps. From a user perspective, I would say that there are two main aspects where the proof assistant actually "assist" you: one, by telling you, in any given situation, what you still have to show and what facts you have available; two, by providing automation to "close the gap" from one step to the next.
So yes, there is some automation that you could use for that, I imagine it would be fairly easy to use that to build a tool like you envision inside Isabelle, by adding or dropping axioms or assumptions, running the automation (e.g. one of the built-in proof methods or sledgehammer or whatever) and checking whether a proof comes out. But the big problem that I see here is that just because the system doesn't find a proof (within a reasonable amount of time) does of course not mean that there is no proof. For simple propositional statements, this will probably work, but already for first-order logic I think it is probably not too hard to find not-too-complex examples that are provable but take the automation forever to find a proof. So if you're hoping to apply this to "real" maths and not just toy examples, I don't think that is realistic. And you might be better of using an automated theorem prover anyway (although I think they have similar limitations).
What is more realistic is the following process, which is something that I think many people who work with ITPs can attest (I suspect that's what's happening in that Gödel paper you mentioned, too): you formalise some theorem, either from scratch or based on a paper proof. When you're done, you start playing around with the assumptions of the theorem; tighten some of the inequalities, drop some assumptions, generalise the statement, etc. And then you have a look where the existing proof breaks. Sometimes it doesn't break at all. Sometimes it breaks in a few places but with some inspection and/or the automation those places are easily fixed. It is not rare to find that the paper proofs contain assumptions that are completely unnecessary, i.e. not just such that the proof is easily repaired when you remove them, but really not used anywhere in the proof. Similarly, ITPs allow you to refactor proofs much more painlessly, because you immediately see what breaks and where.
Dually, you also occasionally find missing assumptions, i.e. assumptions that you have to add for the paper proof to work, or even for the theorem to hold in the first place. But that's another story…
Cheers,
Manuel
On 27/01/2025 12:30, Lauri Olli Tarpila (via cl-isabelle-users Mailing List) wrote:
Hello,
In short: Is it possible to make a program using Isabelle so that you give it a mathematical statement in ZFC and FOL and it creates a proof of it and tells you which axioms are used?
I am a Master of Science in statistics. I consider Helmut Strasser's book "Mathematical theory of statistics: Statistical experiments and asymptotic decision theory" as a good background for statistical experiments. I asked Strasser personally and he said that the book is based on ZFC axioms and First order logic. I would then be interested in understanding ZFC axioms so well that from every statement in the book I could say that which specific axioms are needed in the statement in hand. Is this possible to achieve by using Isabelle and have someone already made this?
I was bedazzled by Isabelle when reading this "Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant" (https://link.springer.com/article/10.1007/s10817-021-09599-8). It was fascinating to see how Isabelle could be used to prove Gödel's theorem. I think proof assistants like Isabelle are crucial in understanding mathematics better.
Kind regards,
Lauri Tarpila
Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:
1. Heriot-Watt University, a Scottish charity registered under number SC000278
2. Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.
The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.
Email Gateway (Jan 27 2025 at 14:05):From: Moritz Roos <cl-isabelle-users@lists.cam.ac.uk>
Hello,
i want to add to the reply from Joe Wells.
You should certainly read a tiny bit of "elementary" set theory based on
ZFC to get a feel for why basically all the Axioms of ZFC are needed
to found typical mathematics
(okay one can maybe make a case against foundation, replacement and
(atleast strong versions of) choice for some areas, but the rest are
very much needed).
So i fear the answer to most "what do i need" questions will be
"basically all of them" most of the time and this is why Joe already
pointed you at the refined question of "How could we weaken (not fully
delete) the axioms to still prove one singled-out theorem?".
But before you can make sense of any answer to that refined question,
you should consider reading a bit into the axioms of ZFC:
I can wholeheartedly recommend Derek Goldrei's "Classic Set Theory : A
guide to independent study".
He will develop very basic mathematics (construction of what a function
is etc.) and some ordinal number theory showing where which axioms are
used, introducing them step by step as needed.
I have never read a more nicely written book on mathematics before!
Moreover i want to mention the Metamath proof system. It has been
designed with this back-traceability of axioms in mind and is based on
ZFC + FOL.
You can click on any of the already proved theorems, and which axioms
were used (notice however, that this might still be different from
"which axioms are really needed") via recursive unravelling of all
definitions and needed theorems for the proof.
See for example this result about matrices and their adjuncts:
https://us.metamath.org/mpeuni/madurid.html and scroll to the bottom to
"This theorem was proved from axioms:".
If you also want to dive into what reasoning in FOL can look like, i
will recommend the "forall x" book, availible at
https://www.fecundity.com/logic/ (it is free of charge).
best wishes,
Moritz
Am 27.01.2025 um 12:30 schrieb Lauri Olli Tarpila (via cl-isabelle-users
Mailing List):
Hello,
In short: Is it possible to make a program using Isabelle so that you
give it a mathematical statement in ZFC and FOL and it creates a proof
of it and tells you which axioms are used?I am a Master of Science in statistics. I considerHelmut Strasser's
book "Mathematical theory of statistics: Statistical experiments and
asymptotic decision theory" as a good background for statistical
experiments. I asked Strasser personally and he said that the book is
based on ZFC axioms and First order logic. I would then be interested
in understanding ZFC axioms so well that from every statement in the
book I could say that which specific axioms are needed in the
statement in hand. Is this possible to achieve by using Isabelle and
have someone already made this?I was bedazzled by Isabelle when reading this "Distilling the
Requirements of Gödel’s Incompleteness Theorems with a Proof
Assistant"
(https://link.springer.com/article/10.1007/s10817-021-09599-8). It was
fascinating to see how Isabelle could be used to prove Gödel's
theorem. I think proof assistants like Isabelle are crucial in
understanding mathematics better.Kind regards,
Lauri Tarpila
Email Gateway (Jan 28 2025 at 10:49):From: Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk>
Hi!
I highly appreciate your answers! I am very happy that the this mailing list provides a way to contact people who can help.
This way of saying "“can this piece of mathematics be proven with substantially less powerful axioms than zfc and fol? how much weaker can we make the axioms and still prove this?" is something I would be interested, but this could result in a situation where the weaker axiom is not part of ZFC or FOL but would be a different system. Maybe like "how many assumptions we can take away from ZFC & FOL and still prove this?"
It is true that the answer might usually be that "we need all of the assumptions" but I would like to be able to say that rather than assume that most probably that is the answer all the time. Since indeed it might not always be the case and that is interesting.
Those book and website recommendations are very welcome. I have studied mathematics for 5 years in the form of statistics and ZFC axioms have become familiar when thinking about mathematics, but that book might indeed explain things in a very clear way.
Metamath might be something that I am looking for and yes that is a issue that things can be proven in many different ways, but right now one way would suffice even if it is not the one that has least axioms in use.
Kind regards,
Lauri Tarpila
PS: Is it enough to just choose "reply" when answering or should I choose "reply all" and add everyone as recipients so that everyone sees my response?
On Monday, January 27th, 2025 at 3:59 PM, Moritz Roos <cl-isabelle-users@lists.cam.ac.uk> wrote:
Hello,
i want to add to the reply from Joe Wells.
You should certainly read a tiny bit of "elementary" set theory based on ZFC to get a feel for why basically all the Axioms of ZFC are needed to found typical mathematics
(okay one can maybe make a case against foundation, replacement and (atleast strong versions of) choice for some areas, but the rest are very much needed).
So i fear the answer to most "what do i need" questions will be "basically all of them" most of the time and this is why Joe already pointed you at the refined question of "How could we weaken (not fully delete) the axioms to still prove one singled-out theorem?".But before you can make sense of any answer to that refined question, you should consider reading a bit into the axioms of ZFC:
I can wholeheartedly recommend Derek Goldrei's "Classic Set Theory : A guide to independent study".
He will develop very basic mathematics (construction of what a function is etc.) and some ordinal number theory showing where which axioms are used, introducing them step by step as needed.
I have never read a more nicely written book on mathematics before!Moreover i want to mention the Metamath proof system. It has been designed with this back-traceability of axioms in mind and is based on ZFC + FOL.
You can click on any of the already proved theorems, and which axioms were used (notice however, that this might still be different from "which axioms are really needed") via recursive unravelling of all definitions and needed theorems for the proof.
See for example this result about matrices and their adjuncts: https://us.metamath.org/mpeuni/madurid.html and scroll to the bottom to "This theorem was proved from axioms:".If you also want to dive into what reasoning in FOL can look like, i will recommend the "forall x" book, availible at https://www.fecundity.com/logic/ (it is free of charge).
best wishes,
MoritzAm 27.01.2025 um 12:30 schrieb Lauri Olli Tarpila (via cl-isabelle-users Mailing List):
Hello,
In short: Is it possible to make a program using Isabelle so that you give it a mathematical statement in ZFC and FOL and it creates a proof of it and tells you which axioms are used?
I am a Master of Science in statistics. I consider Helmut Strasser's book "Mathematical theory of statistics: Statistical experiments and asymptotic decision theory" as a good background for statistical experiments. I asked Strasser personally and he said that the book is based on ZFC axioms and First order logic. I would then be interested in understanding ZFC axioms so well that from every statement in the book I could say that which specific axioms are needed in the statement in hand. Is this possible to achieve by using Isabelle and have someone already made this?
I was bedazzled by Isabelle when reading this "Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant" (https://link.springer.com/article/10.1007/s10817-021-09599-8). It was fascinating to see how Isabelle could be used to prove Gödel's theorem. I think proof assistants like Isabelle are crucial in understanding mathematics better.
Kind regards,
Lauri Tarpila
Email Gateway (Jan 28 2025 at 18:02):From: Lawrence Paulson <lp15@cam.ac.uk>
I suspect the author was being a bit careless when he said "the book is based on ZFC axioms and First order logic”. I’d be surprised if he refers to any ZF axioms by name. But it’s generally assumed that all mathematics can be developed in ZFC, ergo, so is his book on the theory of statistics. But HOL (as in Isabelle/HOL) is probably a much better formal basis for his book.
If on the other hand you are reading a book about ordinals, cardinals, the Mostowski collapse, Aronszajn trees and such like, then it really is based on the ZFC axioms.
Larry
On 27 Jan 2025, at 12:51, Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk> wrote:
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
Email Gateway (Jan 28 2025 at 20:54):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Just to add to this: HOL has essentially the same expressive power as
Zermelo set theory, i.e., ZFC without the Replacement axiom, but with
the Separation (Restricted Comprehension) -- indeed, likely to be
sufficient for the foundations of probabilities and statistics.
As for Lauri Olli Tarpila's point: "I think proof assistants like
Isabelle are crucial in understanding mathematics better." Overall I
wholeheartedly agree with this. Manuel described the possibilities and
limitations very well, but I want to add that certain theorems such as
Gödel's second (first mechanized by Larry in Isabelle
https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/abs/machineassisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets)
are especially in need of mechanization.
Best wishes,
Andrei
On Tue, Jan 28, 2025 at 6:02 PM Lawrence Paulson <lp15@cam.ac.uk> wrote:
I suspect the author was being a bit careless when he said "the book is based on ZFC axioms and First order logic”. I’d be surprised if he refers to any ZF axioms by name. But it’s generally assumed that all mathematics can be developed in ZFC, ergo, so is his book on the theory of statistics. But HOL (as in Isabelle/HOL) is probably a much better formal basis for his book.
If on the other hand you are reading a book about ordinals, cardinals, the Mostowski collapse, Aronszajn trees and such like, then it really is based on the ZFC axioms.
Larry
On 27 Jan 2025, at 12:51, Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk> wrote:
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
Email Gateway (Jan 28 2025 at 20:56):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Sorry for the broken link -- this is the correct one: :-)
On Tue, Jan 28, 2025 at 8:53 PM Andrei Popescu
<andrei.h.popescu@gmail.com> wrote:
Just to add to this: HOL has essentially the same expressive power as
Zermelo set theory, i.e., ZFC without the Replacement axiom, but with
the Separation (Restricted Comprehension) -- indeed, likely to be
sufficient for the foundations of probabilities and statistics.As for Lauri Olli Tarpila's point: "I think proof assistants like
Isabelle are crucial in understanding mathematics better." Overall I
wholeheartedly agree with this. Manuel described the possibilities and
limitations very well, but I want to add that certain theorems such as
Gödel's second (first mechanized by Larry in Isabelle
https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/abs/machineassisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets)
are especially in need of mechanization.Best wishes,
AndreiOn Tue, Jan 28, 2025 at 6:02 PM Lawrence Paulson <lp15@cam.ac.uk> wrote:
I suspect the author was being a bit careless when he said "the book is based on ZFC axioms and First order logic”. I’d be surprised if he refers to any ZF axioms by name. But it’s generally assumed that all mathematics can be developed in ZFC, ergo, so is his book on the theory of statistics. But HOL (as in Isabelle/HOL) is probably a much better formal basis for his book.
If on the other hand you are reading a book about ordinals, cardinals, the Mostowski collapse, Aronszajn trees and such like, then it really is based on the ZFC axioms.
Larry
On 27 Jan 2025, at 12:51, Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk> wrote:
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
Email Gateway (Jan 29 2025 at 18:33):From: Lauri Olli Tarpila <cl-isabelle-users@lists.cam.ac.uk>
Hi!
Yes in the book "Mathematical Theory of Statistics" (if I remember) the ZFC axioms are not listed or referred. But it seemed that Strasser does know ZFC axioms well and probably could list which axioms are used where (with some thinking).
I checked Mostowski collapse (did not yet fully understand it) and I see that there ZFC is more closely referred.
It would be cool to help in the mechanization of Gödel's second theorem! Anyone in need of a research assistant? Though I am not fluent in Isabelle, but unemployed and smart :).
Kind regards,
Lauri Tarpila
On Tuesday, January 28th, 2025 at 10:55 PM, Andrei Popescu <andrei.h.popescu@gmail.com> wrote:
Sorry for the broken link -- this is the correct one: :-)
On Tue, Jan 28, 2025 at 8:53 PM Andrei Popescu
andrei.h.popescu@gmail.com wrote:Just to add to this: HOL has essentially the same expressive power as
Zermelo set theory, i.e., ZFC without the Replacement axiom, but with
the Separation (Restricted Comprehension) -- indeed, likely to be
sufficient for the foundations of probabilities and statistics.As for Lauri Olli Tarpila's point: "I think proof assistants like
Isabelle are crucial in understanding mathematics better." Overall I
wholeheartedly agree with this. Manuel described the possibilities and
limitations very well, but I want to add that certain theorems such as
Gödel's second (first mechanized by Larry in Isabelle
https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/abs/machineassisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets)
are especially in need of mechanization.Best wishes,
AndreiOn Tue, Jan 28, 2025 at 6:02 PM Lawrence Paulson lp15@cam.ac.uk wrote:
I suspect the author was being a bit careless when he said "the book is based on ZFC axioms and First order logic”. I’d be surprised if he refers to any ZF axioms by name. But it’s generally assumed that all mathematics can be developed in ZFC, ergo, so is his book on the theory of statistics. But HOL (as in Isabelle/HOL) is probably a much better formal basis for his book.
If on the other hand you are reading a book about ordinals, cardinals, the Mostowski collapse, Aronszajn trees and such like, then it really is based on the ZFC axioms.
Larry
On 27 Jan 2025, at 12:51, Lauri Olli Tarpila cl-isabelle-users@lists.cam.ac.uk wrote:
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
Email Gateway (Jan 30 2025 at 00:10):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Hi Lauri,
On Wed, Jan 29, 2025 at 6:33 PM Lauri Olli Tarpila
<lauri.tarpila@protonmail.com> wrote:
Hi!
Yes in the book "Mathematical Theory of Statistics" (if I remember) the ZFC axioms are not listed or referred. But it seemed that Strasser does know ZFC axioms well and probably could list which axioms are used where (with some thinking).
I checked Mostowski collapse (did not yet fully understand it) and I see that there ZFC is more closely referred.
It would be cool to help in the mechanization of Gödel's second theorem! Anyone in need of a research assistant? Though I am not fluent in Isabelle, but unemployed and smart :).
That was already done, as reported in the referenced paper. Sorry for
my confusing formulation, I meant to say that Gödel's second has
been formalized (mechanized) for the first time there.
Best wishes,
Andrei
Kind regards,
Lauri TarpilaOn Tuesday, January 28th, 2025 at 10:55 PM, Andrei Popescu <andrei.h.popescu@gmail.com> wrote:
Sorry for the broken link -- this is the correct one: :-)
On Tue, Jan 28, 2025 at 8:53 PM Andrei Popescu
andrei.h.popescu@gmail.com wrote:Just to add to this: HOL has essentially the same expressive power as
Zermelo set theory, i.e., ZFC without the Replacement axiom, but with
the Separation (Restricted Comprehension) -- indeed, likely to be
sufficient for the foundations of probabilities and statistics.As for Lauri Olli Tarpila's point: "I think proof assistants like
Isabelle are crucial in understanding mathematics better." Overall I
wholeheartedly agree with this. Manuel described the possibilities and
limitations very well, but I want to add that certain theorems such as
Gödel's second (first mechanized by Larry in Isabelle
https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/abs/machineassisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets)
are especially in need of mechanization.Best wishes,
AndreiOn Tue, Jan 28, 2025 at 6:02 PM Lawrence Paulson lp15@cam.ac.uk wrote:
I suspect the author was being a bit careless when he said "the book is based on ZFC axioms and First order logic”. I’d be surprised if he refers to any ZF axioms by name. But it’s generally assumed that all mathematics can be developed in ZFC, ergo, so is his book on the theory of statistics. But HOL (as in Isabelle/HOL) is probably a much better formal basis for his book.
If on the other hand you are reading a book about ordinals, cardinals, the Mostowski collapse, Aronszajn trees and such like, then it really is based on the ZFC axioms.
Larry
On 27 Jan 2025, at 12:51, Lauri Olli Tarpila cl-isabelle-users@lists.cam.ac.uk wrote:
Yea I understand that if I can formalise a theorem then I can study its behavior with Isabelle. But yeah I guess I was looking for a more general system that would quickly show me that "This statement X uses these and these axioms of ZFC and FOL" can be pretty difficult. Maybe if I formalise the books general ideas then it could work like you mention.
Last updated: Jan 30 2025 at 04:21 UTC