*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] Untyped formalized systems are wrong (blog post)*From*: Steven Obua <steven.obua at googlemail.com>*Date*: Fri, 8 Jul 2011 21:05:27 +0200*Cc*: isarmathlib-devel at nongnu.org, isabelle-users at cl.cam.ac.uk*In-reply-to*: <1319931310144510@web97.yandex.ru>*References*: <1319931310144510@web97.yandex.ru>

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 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 >

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

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

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