Email Gateway (Aug 18 2022 at 18:02): Email Gateway (Aug 18 2022 at 18:02):From: Victor Porton <porton@narod.ru>
Please read and discuss my blog post "Untyped formalized systems are wrong" at
http://portonmath.wordpress.com/2011/07/08/untyped-or-typed/
where I advocate using typed systems like HOL.
I really hope to start a discussion thread in blogs and/or mailing lists.
Email Gateway (Aug 18 2022 at 18:02):From: Steven Obua <steven.obua@googlemail.com>
Having read your blog post, I can understand why you come to your conclusion, but I think you come to the wrong conclusion.
For example, if you have two different lattices, with two different lattice operations, you will need two different names for it, there is just no way around it.
What you would usually do in informal mathematics is to introduce a context where you have abbreviations for those two operations, and then argue with these abbreviations. Locales in Isabelle are a step in the right direction, but (IMHO) not lightweight and integrated enough.
HOLZF is not really a solution for this problem (once upon a time I thought it might be), but might be a useful tool in order to enhance the logical strength of a proper solution.
My current idea for a system would be "lightweight contexts" + L, where L is some kind of logic that relates to Babel-17 in a similar way as HOL relates to Standard ML.
I think the problem you are addressing is one of the more important problems that are in the way of an adoption of theorem proving assistants by mainstream mathematicians. Unfortunately, many many computer scientists (which currently seem to be the majority of people interested in theorem proving assistants) live in a typed world anyway and don't see the problem or think dependent types solve it.
Cheers,
Steven
Email Gateway (Aug 18 2022 at 18:02):From: Steven Obua <steven.obua@googlemail.com>
On 08.07.2011, at 21:43, Victor Porton wrote:
08.07.2011, 23:05, "Steven Obua" <steven.obua@googlemail.com>:
Having read your blog post, I can understand why you come to your conclusion, but I think you come to the wrong conclusion.
For example, if you have two different lattices, with two different lattice operations, you will need two different names for it, there is just no way around it.
What you would usually do in informal mathematics is to introduce a context where you have abbreviations for those two operations, and then argue with these abbreviations. Locales in Isabelle are a step in the right direction, but (IMHO) not lightweight and integrated enough.In the very example I provided in the blog, the lattices are essentially types WITH ARGUMENTS (or are they called "parameters"?). This can't be modeled by introducing abbreviations for those two operations. It is the reason I want a typed system and resign from ZF.
In your blog you complain that you have to annotate the operations with lengthy descriptions. Well, this is because they are different operations with possibly different carrier sets, right? How would you write your example in HOL ? My guess is you can't.
HOLZF is not really a solution for this problem (once upon a time I thought it might be), but might be a useful tool in order to enhance the logical strength of a proper solution.
My current idea for a system would be "lightweight contexts" + L, where L is some kind of logic that relates to Babel-17 in a similar way as HOL relates to Standard ML.
Could you clarify? I don't really know what is Babel-17.
Is it worth to study Babel-17 for me? I'm an amateur mathematician specializing in General Topology and has not yet decided whether to invest my time into rewriting my results in a formal system like Isabelle/ISAR.
Babel-17 is a programming language I am currently developing (www.babel-17.com). Yep, it is worth studying it (but then again, I might be biased in that respect :-D), especially if you are a mathematician. But it won't currently help you with theorem proving. I have brought it up because it has a type system which allows for encapsulation and abstraction, but is dynamically typed. I would like one day to build a theorem proving system on top of it, just like HOL systems like HOL4, Isabelle and HOL-Light are built on top of Standard ML / OCaml. Note that the type system of HOL is basically that of Standard ML.
PS: It's Friday night, I guess the Isabelle mailing list can take the hit...
Email Gateway (Aug 18 2022 at 18:02):From: Steven Obua <steven.obua@googlemail.com>
That wouldn't work, because in order for A and B to be parameters, they would have to be modeled as types, too. Now, two types in HOL are either identical (A = B), or they are disjoint. That's probably not what you would for your construction. It's probably best you try to formalize a small part of your theory in Isabelle/HOL. Then you will pretty soon notice what works and what doesn't.
Email Gateway (Aug 18 2022 at 18:03):From: Victor Porton <porton@yandex.ru>
08.07.2011, 23:05, "Steven Obua" <steven.obua@googlemail.com>:
Having read your blog post, I can understand why you come to your conclusion, but I think you come to the wrong conclusion.
For example, if you have two different lattices, with two different lattice operations, you will need two different names for it, there is just no way around it.
What you would usually do in informal mathematics is to introduce a context where you have abbreviations for those two operations, and then argue with these abbreviations. Locales in Isabelle are a step in the right direction, but (IMHO) not lightweight and integrated enough.
In the very example I provided in the blog, the lattices are essentially types WITH ARGUMENTS (or are they called "parameters"?). This can't be modeled by introducing abbreviations for those two operations. It is the reason I want a typed system and resign from ZF.
HOLZF is not really a solution for this problem (once upon a time I thought it might be), but might be a useful tool in order to enhance the logical strength of a proper solution.
My current idea for a system would be "lightweight contexts" + L, where L is some kind of logic that relates to Babel-17 in a similar way as HOL relates to Standard ML.
Could you clarify? I don't really know what is Babel-17.
Is it worth to study Babel-17 for me? I'm an amateur mathematician specializing in General Topology and has not yet decided whether to invest my time into rewriting my results in a formal system like Isabelle/ISAR.
(You may probably answer these my questions in a personal email, not mailing lists, as for the rest public these may be irrelevant.)
I think the problem you are addressing is one of the more important problems that are in the way of an adoption of theorem proving assistants by mainstream mathematicians. Unfortunately, many many computer scientists (which currently seem to be the majority of people interested in theorem proving assistants) live in a typed world anyway and don't see the problem or think dependent types solve it.
Cheers,
Steven
On 08.07.2011, at 19:01, Victor Porton wrote:
Please read and discuss my blog post "Untyped formalized systems are wrong" at
http://portonmath.wordpress.com/2011/07/08/untyped-or-typed/
where I advocate using typed systems like HOL.
I really hope to start a discussion thread in blogs and/or mailing lists.
--
Victor Porton - http://portonvictor.org
Email Gateway (Aug 18 2022 at 18:03):From: Victor Porton <porton@yandex.ru>
I'm not an expert in Isabelle/HOL but it seems for me that it can be written using types with parameters (my sets A and B would be parameters of a type "funcoid").
Email Gateway (Aug 18 2022 at 18:03):From: Victor Porton <porton@yandex.ru>
Oh, sorry for my stupid dilettante consideration. Steven, I just want to finish my conversation with hope that you'll create a new proof assistant which deals smoothly over the trouble described in my blog. I suppose this could be done by allowing type parameters to be arbitrary values not just types.
Email Gateway (Aug 18 2022 at 18:03):From: Steven Obua <steven.obua@googlemail.com>
You would need HOLZF for that (to get ZF sets within HOL). It might work, depending on what "\cap" does. As I said, the best way to see if it really works and if this is what you want is to just try it out!
Email Gateway (Aug 18 2022 at 18:03):From: Steven Obua <steven.obua@googlemail.com>
Instead of using tags/tuples you would probably rather use something like
datatype myuniverse = Sets of ZF | Filters of ZF
you can then define your operation "\cap", but you would need to also say what Sets (A) \cap Filters (B) should mean (for example, "arbitrary", if there is no good definition for this)
If you don't want both to live in the same universe, then also
datatype sets = Sets of ZF
datatype filters = Filters of ZF
could work. Due to overloading, you could still define "\cap" to operate on sets*filters if you should need that.
I think you should definitely go for it and try to formalize your stuff using HOLZF to see if that works. I think it is definitely worth the time anyway as you will learn more about both HOL and your stuff.
Email Gateway (Aug 18 2022 at 18:04):From: Victor Porton <porton@yandex.ru>
Sorry for a possibly stupid question, but can't it be done with tuples consisting of a unique tag and sets A, B (with patter matching) together with the actual value (which is a ZF set)?
"(funcoid, A, B, v)" (where "funcoid" is a unique tag) would mean a funcoid from A to B whose set-theoretic value is v.
"(funcoid, A, B, v1) \cap (funcoid, A, B, v2)" would be well defined.
Note that this can't be done in pure ZFC as in ZFC there are no concept of unique tags.
Email Gateway (Aug 18 2022 at 18:05):From: Victor Porton <porton@yandex.ru>
I will explain what "\cap" should do:
Before investing my time into learning HOL, I want to ask whether the following is possible at all to implement in HOL:
Let "sets" and "filters" are unique tags.
Let "(sets, X)" denotes a ZF set X understood a plain set.
Let "(filters, F)" denotes a filter whose ZF value is F. Let filters are ordered REVERSE to set-theoretic inclusion, that is I want:
"(filters, F1) \subseteq (filters, F2) <-> F1 \supseteq F2".
Can we define the following with pattern matching (not with enumerating all possible cases, to be extensible without rewriting existing matching code)?
"(sets, X1) \cap (sets, X2)" to be different than "(filters, X1) \cap (filters, X2)" where X1 and X2 are filters (in the sense as filters are defined in ZF).
I want "(sets, X1) \cap (sets, X2) = (sets, X1\cap X2)" and "(filters, X1) \cap (filters, X2)" to mean "(filters, Y)" where Y is the coarsest filter which is finer than both X1 and X2.
Email Gateway (Aug 18 2022 at 18:05):From: Victor Porton <porton@narod.ru>
My idea was completely wrong. The source of my trouble was that I had overlapping sets. The solution is to use bijective copies of the sets to make them non-overlapping and this works in ZF (no need for a typed system for this).
Last updated: Apr 19 2024 at 20:15 UTC