[FOM] Defining Cargo Cult Science in Mathematics (Sam Sanders

[José Manuel Rodriguez Caballero]

>
> Sam wrote:
> What about the following problem: choosing the right definitions is
> extremely important when doing constructive math, and even more so when
> formalising math
> in proof assistants. For instance, Larry Paulson has formalised Godel?s
> incompleteness theorems in Isabelle using the notion of ?hereditarily
> finite set?.  He used
> this particular notion because other notions did not (seem to) yield a
> formal proof (I am citing from memory about a talk he gave at TU Munich).
> IIRC, he even wrote
> (or rewrote?) a version of Sledgehammer to accommodate this notion.
> Are we therefore to conclude that this particular formulation (using
> hereditarily finite sets) of Godel?s incompleteness theorems is genuine and
> the others are not?


If a version of Goedel's incompleteness theorem can not be formalized in a
proof assistant, it should be renamed as heuristic.argument for the
Goedel's incompleteness theorem.

Sam wrote:
> Moreover, what if different parts of math require different (but
> equivalent, say in ZFC) definitions to successfully obtain formal proofs?


Each one is genuine, because it can be formalized. Cargo Cult Science is
what cannot be formalized in a consistent way, e.g., the golden ration is
magic (this cannot be formalized in a consistent way).

Sam wrote:
> Finally, it seems your notion of ?genuine vs CCS? includes some kind of
> implicit strict finitism (and temporal/physical dimension): for a given
> theorem to be implemented in a
> proof assistant, there have to be ?good? definitions that result in a
> proof that can be run on a physical machine (in the here and now).


Yes, a so-called theorem with an infinitely large proof is Cargo Cult
Science.

Sam wrote:
> The previous does present a nice  ?incompleteness? challenge: find a
> natural theorem that cannot be implemented in proof assistants,
> in that any choice of definitions for that theorem results in infeasible
> computation at the level of implemented proofs.


As far as I know, many results in elementary topos cannot be formalized in
current proof assistants, because of a problem with the natural number
object. Nevertheless, proofs assistants in the future will be able to
perform such a talk. A nice natural theorem which cannot be formalized in
any proof assistant is a perfect example of a result belonging to Cargo
Cult Science.

Goedel's proof of the existence of God via ultrafilters satisfies the
criteria for genuine mathematics, because it can be formalized in a proof
assistant in a consistent way, indepently of the fact that the reader may
disagree with the axioms:
http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180910/4444161b/attachment-0001.html>