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



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
> 






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