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 <[email protected]>
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
> [email protected] http://kwarc.info/kohlhase
> ----------------------------------------------------------------------
>
> <m_kohlhase.vcf>_______________________________________________
> Om3 mailing list
> [email protected]
> http://openmath.org/mailman/listinfo/om3
_______________________________________________
Om3 mailing list
[email protected]
http://openmath.org/mailman/listinfo/om3
