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

09.07.2011, 16:45, "Steven Obua" <steven.obua at>:
> On 09.07.2011, at 14:30, Victor Porton wrote:
>>  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 -
> You would need HOLZF for that (to get ZF sets within HOL). It might work, depending on what "\cap" does. As I said, the best way to see if it really works and if this is what you want is to just try it out!

I will explain what "\cap" should do:

Before investing my time into learning HOL, I want to ask whether the following is possible at all to implement in HOL:

Let "sets" and "filters" are unique tags.

Let "(sets, X)" denotes a ZF set X understood a plain set.
Let "(filters, F)" denotes a filter whose ZF value is F. Let filters are ordered REVERSE to set-theoretic inclusion, that is I want:
"(filters, F1) \subseteq (filters, F2) <-> F1 \supseteq F2".

Can we define the following with pattern matching (not with enumerating all possible cases, to be extensible without rewriting existing matching code)?

"(sets, X1) \cap (sets, X2)" to be different than "(filters, X1) \cap (filters, X2)" where X1 and X2 are filters (in the sense as filters are defined in ZF).

I want "(sets, X1) \cap (sets, X2) = (sets, X1\cap X2)" and "(filters, X1) \cap (filters, X2)" to mean "(filters, Y)" where Y is the coarsest filter which is finer than both X1 and X2.

Victor Porton -

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