*Formalizing Mathematics In Simple Type Theory* Lawrence C. Paulson (Submitted on 20 Apr 2018) https://arxiv.org/abs/1804.07860
Despite the considerable interest in new dependent type theories, simple type theory (which dates from 1940) is sufficient to formalize serious topics in mathematics. This point is seen by examining formal proofs of a theorem about stereographic projections. A formalization using the *HOL Light** proof assistant is contrasted with one using Isabelle/HOL. Harrison's technique for formalizing Euclidean spaces is contrasted with an approach using Isabelle/HOL's axiomatic type classes. However, every formal system can be outgrown, and mathematics should be formalized with a view that it will eventually migrate to a new formalism. *Thus we are led to conclude that, although everything mathematical is formalizable, it is nevertheless impossible to formalise all of mathematics in a single formal system, a fact that intuitionism has asserted all along.* K. Godel * https://www.cl.cam.ac.uk/~jrh13/hol-light/ @philipthrift -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/332089ae-fb18-4ecb-ae8a-11a19886f074%40googlegroups.com.
