[FOM] Defining Cargo Cult Science in Mathematics

[José Manuel Rodriguez Caballero]

>
> MK wrote:
> One discerns distinct profiles among such
> critics:
> (1) people opposed to Robinson's framework because they feel it
> conflicts with a legitimate mathematical framework they favor on
> philosophical grounds;
> (2) people involved in a Cargo Cult Science (CCS) of their own without
> necessarily any intrinsic or scholarly value, and hate Robinson's
> theory because they perceive it as a valid competitor that
> disqualifies their CCS.


In experimental science, CCS can be defined as a fail in the use of the
scientific method. In pure mathematics the situation is more subtle. I
would like to propose that a candidate mathematical-like theory is CCS if
it cannot be developed in a proof assistant. Otherwise, it is a genuine
mathematical theory.

In some cases, like elementary topos, I think that they cannot be developed
in traditional proofs assistants, because, in general, they lack a natural
number object. Nevertheless, such a proof assistant without natural number
object can be developed in the future. So, non-standard analysis is not
CCS, but genuine mathematics, because it was implemented in Isabelle/HOL.
Reference:
https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/fleuriot-princip-CADE.pdf

MK wrote:
> Here Bishop would clearly fall under category (1), even though he may
> have been factually wrong in thinking that there is actually a
> conflict, as argued by Sam Sanders.


Indeed, Bishop's intuitionistic approach is genuine mathematics, because it
can be formalized in a proof assistant, e.g, Isabelle/CTT (does not confuse
with Isabelle/HOL), Coq.  Reference:
http://www.cse.chalmers.se/research/group/logic/book/book.pdf

MK wrote:
> As far as Connes is concerned, he clearly has a system of his own
> including a rudimentary notion of infinitesimal (viewed as compact
> operators with a specific rate of decay of eigenvalues).  On the other
> hand, some of the claims he makes, particularly about his so-called
> "primordial mathematical reality" tend to place him into category (2).


If a system like Connes' primordial mathematical reality can be formalized
in a proof assistant, then Connes' criticism to Robinson's approach will be
fair inside Connes' system, although this will not affect the fact that
Robinson's approach is genuine mathematics as explained above. It is like
the law of excluded middle, which is not a theorem in Coq, but it is a
theorem in Isabelle/HOL. Nevertheless, there is the tu quoque problem: Can
Connes' creative mathematical work, e.g., his program to solve to the
Riemann Hypothesis as a limit case of Weil's conjectures, be formalized in
a proof assistant according to the so-called primordial mathematical
reality? Well, the first step is to formalize this primordial mathematical
reality in a proof assistant. If this is possible, then we can take it as
more than an inspiration.

There is a new mysticism in mathematics which comes from Grothendieck's
book: The key of dreams or dialogue with God (LA CLEF DES SONGES : OU
DIALOGUE AVEC LE BON DIEU, PAR ALEXANDRE GROTHENDIECK. 1987.)

It will be interesting to discover how much of Connes' criticism of
Nonstandard Analysis was influenced by Grothendieck's ideas. Indeed, in
this video Connes reads some parts of Grothendieck's book:
https://www.youtube.com/watch?v=FkBtSRyv6l4

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180908/288a3090/attachment.html>