FMP type=defining

[jbs1]

migrated from Trac, where originally posted by jhd on 26-Oct-2007 7:26am

Allow specifiers on FMP, equivalent to the old DefMP proposal of Cohen et al.
See suggestions from JHD.

[jbs1]

migrated from Trac, where originally posted by jhd on 26-Oct-2007 7:26am

JHD's slides at MKM2007

[jbs1]

migrated from Trac, where originally posted by kohlhase on 25-Feb-2011 12:25pm

rescheduling

[jbs1]

migrated from Trac, where originally posted by lars_h on 31-May-2014 8:37pm

Writing down the following example so that I don't forget it.

In (single variable) complex analysis, the term analytic (function) may be defined as:

• Satisfies the Cauchy–Riemann equations on the whole of C.
• The Maclaurin series converges to the function on the whole of C.
• … and I'm pretty sure there are a bunch more of them (satisfying the Cauchy integral formula seems likely).
  But it was a long time since I did that course, and I may be getting some details wrong.

The point is, that whereas any particular development of complex analysis must choose one of these as the definition of analytic (and then prove the rest as theorems), there is not in the mathematics as such anything which says that one of them is the "proper" definition and the others just logical curiosities. Rather, they are all equivalent. Hence there is no need to single out one of them for a symbol that seeks to denote the concept in general.

One image I'm thinking about is that maybe the graph of all definitions need not be a forest, but rather that it should be given with an edge-colouring where each colour class is acyclic. Colours then correspond to particular developments of mathematics.

[jbs1]

migrated from Trac, where originally posted by jhd on 1-Jun-2014 10:45pm

A good discussion. Is the world ready for this?
However, I suspect that whatever we decide ought NOT to preclude this, which will make for an interesting debate.
Another example might be elementary transcendental functions, where one colouring (tree/forest) would be complex, rooted in exp/log, and the other real, rooted, say, in exp/tan/log/atan (as for Pascal)
Thanks

[kohlhase]

moved to OpenMath/OMSTD#38