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

09.07.2011, 00:53, "Steven Obua" <steven.obua at>:
> On 08.07.2011, at 22:38, Victor Porton wrote:
>>  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 -
> 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.

Sorry for a possibly stupid question, but can't it be done with tuples consisting of a unique tag and sets A, B (with patter matching) together with the actual value (which is a ZF set)?

"(funcoid, A, B, v)" (where "funcoid" is a unique tag) would mean a funcoid from A to B whose set-theoretic value is v.

"(funcoid, A, B, v1) \cap (funcoid, A, B, v2)" would be well defined.

Note that this can't be done in pure ZFC as in ZFC there are no concept of unique tags.

Victor Porton -

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