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

09.07.2011, 00:09, "Steven Obua" <steven.obua at>:
> 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.

I'm not an expert in Isabelle/HOL but it seems for me that it can be written using types with parameters (my sets A and B would be parameters of a type "funcoid").

Victor Porton -

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