[FOM] Defining Cargo Cult Science in Mathematics

[Lawrence Paulson]

> On 9 Sep 2018, at 13:15, Sam Sanders <sasander at me.com> wrote:
> 
> 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.  

Let me clarify some points here.

I formalised Gödel's theorems following a preprint by Swierczkowski because it was, by far, the most careful presentation of Gödel's proof I have ever seen. Most published presentations merely sketch out the ideas.

Swierczkowski prefers the hereditarily finite sets for the following reason:

"HF is much better suited for the purpose of describing its own meta-theory. The reason lies in the great expressive power of set theory. A set-theoretical description of the language of HF (and then of the whole meta-theory) presents itself in a wholly natural fashion, once it has been decided how to code (represent) by constant terms the 7 basic (primitive) symbols and the variables of the first-order language of HF. It is at hand to code the variables x1, x2, ... simply by the ordinals 1, 2, ... The constant 0 can be coded as 0, and the remaining 6 symbols as n-tuples of 0s, say ∈ as ⟨0, 0⟩, etc. And here ends the arbitrariness of coding, which is so unpleasant when languages are arithmetized."

Personally I have no concern with arbitrariness. The big advantage of HF is that it provides a notion of ordered pairing almost trivially. Using arithmetic one must either prove the Chinese remainder theorem or develop arguments involving prime numbers. One might argue that these are elementary, but remember that in order to prove the second incompleteness theorem, all of this theory must be worked out formally within an embedded calculus. It can be done but would involve unending tedium.

I don't recall any need to modify Isabelle itself during the course of this project.

Larry Paulson