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

On 08.07.2011, at 21:43, Victor Porton wrote:

> 08.07.2011, 23:05, "Steven Obua" <steven.obua at>:
>> 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 ( 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.

- Steven

PS: It's Friday night, I guess the Isabelle mailing list can take the hit...

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