[Om3] A short comment on two of Michael's ideas. Re: Reminder: today 14:00 CET

[Chris Rowley]

This could be something to talk about today.

Michael at some stage suggested extending OM structures with the following:

Records;
Sequences.

Looking at these from a mathematical viewpoint they are both requests for ‘sets in OM’.

—  Records being, I think, equivalent to finite (unordered?, labelled) sets.
—  Sequences add the canonical the minimal (well-ordered) infinite set 
     (together with the whole high-order concept of infinity, which worries 
      me 'beyond measure’).
 
Now sets seem, from a Bourbaki-view of maths to be very natural things to have as first-class objects in a ‘language for maths’, bt there are other ways to develop the subject.

Also, it could be that sets are already present in the OM formalism, but are currently ignored.

As for the existence of infinite sets, this must be an extension of OM but what place does it have in a computer-accessible language?  And it raises the question of why only countable sets are to be added?

chris  


On 2 Jun 2014, at 18:02, Michael Kohlhase <m.kohlhase at jacobs-university.de> wrote:

> Dear all,
> 
> We will talk soon.
> 
> Michael
> 
> -- 
> ----------------------------------------------------------------------
> Prof. Dr. Michael Kohlhase,        Office: Research 1, Room 168
> Professor of Computer Science  Campus Ring 1, 
> Jacobs University Bremen           D-28759 Bremen, Germany
> tel/fax: +49 421 200-3140/-493140  skype: m.kohlhase   
> m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase 
> ----------------------------------------------------------------------
> 
> <m_kohlhase.vcf>_______________________________________________
> Om3 mailing list
> Om3 at openmath.org
> http://openmath.org/mailman/listinfo/om3