[FOM] Defining Cargo Cult Science in Mathematics (Sam Sanders
José Manuel Rodriguez Caballero
josephcmac at gmail.com
Mon Sep 10 20:16:07 EDT 2018
> 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.
> 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).
> 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
> 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
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:
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM