*To*: Steven Obua <steven.obua at googlemail.com>*Subject*: Re: [isabelle] Untyped formalized systems are wrong (blog post)*From*: Victor Porton <porton at yandex.ru>*Date*: Fri, 08 Jul 2011 23:43:45 +0400*Cc*: isarmathlib-devel at nongnu.org, isabelle-users at cl.cam.ac.uk*In-reply-to*: <8B1DEAC2-0593-4F73-9B2B-636B4575408A@googlemail.com>*References*: <1319931310144510@web97.yandex.ru> <8B1DEAC2-0593-4F73-9B2B-636B4575408A@googlemail.com>

08.07.2011, 23:05, "Steven Obua" <steven.obua at 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 -- Victor Porton - http://portonvictor.org

**Follow-Ups**:**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

**References**:**[isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

- Previous by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Previous by Thread: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Thread: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Cl-isabelle-users July 2011 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