general formulation issues by Chris

[kohlhase]

see https://github.com/OpenMath/OM3/issues/75

[kohlhase]

I think that Chris should propose better formulations or call for help. @car222222 I have added him to the repos as a collaborator, when he accepts, I can assign this to him.

[kohlhase]

closed accidentally.

[car222222]

Chris is formulating suggestions about cds, symbols and signatures. These mainly affect what we say about them rather than more formal changes. In particular, around these questions: — ‘types of cd’ such as “mathematical” “directives”., etc., other suggestions welcome; — ‘definitions’ in maths cds, and building a coherent collection of cds that, for the example, in some sense represents ‘the Bourbaki approach to basic ZF-maths’: Includes a possible need for an addition to the standard to support formally labelling some FMPs in cds as DefiningMPs, to distinguish them from results that need proof (I know that it is not as simple as this as many maths definitions include logically complex statements regarding existence, uniqueness and equivalence); — ‘signatures’ I understand that the ‘computational signature’ may need to vary (use-cases?) but the FMPs need/use at least a fixed ‘mathematical signature’ and any coherent collection with DMPs will imply such a fixed signature.

[kohlhase]

Assigning to James and Chris to make a proposal (and ultimately a pull request for the standard).

[car222222]

Do we want to continue this discussion under this issue? Or, at some stage, open it out on on a mailing list?

[kohlhase]

I personally like the targetted discussions on issues better. One could (if you find it appropriate) tell the mailing list that this is going on here.

[car222222]

Stayed here for now is fine with me.