Re: [isabelle] Untyped formalized systems are wrong (blog post)
09.07.2011, 00:53, "Steven Obua" <steven.obua at googlemail.com>:
> On 08.07.2011, at 22:38, Victor Porton wrote:
>> 09.07.2011, 00:09, "Steven Obua" <steven.obua at googlemail.com>;:
>>> On 08.07.2011, at 21:43, Victor Porton wrote:
>>>> 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.
>>> 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 - http://portonvictor.org
> That wouldn't work, because in order for A and B to be parameters, they would have to be modeled as types, too. Now, two types in HOL are either identical (A = B), or they are disjoint. That's probably not what you would for your construction. It's probably best you try to formalize a small part of your theory in Isabelle/HOL. Then you will pretty soon notice what works and what doesn't.
Oh, sorry for my stupid dilettante consideration. Steven, I just want to finish my conversation with hope that you'll create a new proof assistant which deals smoothly over the trouble described in my blog. I suppose this could be done by allowing type parameters to be arbitrary values not just types.
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and