Re: [isabelle] Untyped formalized systems are wrong (blog post)



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.