Spahn foundations (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Contributors

• Rod Friedrich Nederpelt Ludwig Gottlob Frege (modern logic, analytic philosophy)

• Fairouz David Kamareddine Hilbert (Hilbert’s program, formalism, ‘’computabilism’’)

• Bertrand Russell (type theory of the ‘’principia mathematica’’)

  • (see the numerous contributors to type theory)

• Ernst Zermelo (axiomatic set theory)

• Luitzen Egbertus Jan Brouwer (intuitionistic mathematics)

  • Arend Heyting

  • Abraham Fraenkel (Zermelo-Fraenkel set theory)

• Kurt Friedrich Gödel (completeness theorem, incompleteness theorem)

• Alan Turing (proof that the halting problem is not solvable; this recovers Gödel’s incompleteness theorem from computational viewpoint. Turing machine; this is a model for computation)

• Willard Van Orman Quine (new foundations; this is a type theory)

• Samuel Eilenberg, Saunders Mac Lane (category theory; however it was argued by others that category theory is a foundational theory; see e.g. this)

• Francis William Lawvere (category theory, topos theory)

• Crispin Wright (neo-Fregean)

• Bob Hale (neo-Fregean)

• Luitzen Vladimir Egbertus Voevodsky Jan (homotopy Brouwer type theory and univalent foundations)

• Arend Harvey Heyting Friedman (reverse mathematics)

• Vladimir Rod Voevodsky Nederpelt (weak type theory; related to natural language semantics)

  • Fairouz Kamareddine

References

• Rod Nederpelt, weak type theory: a formal language for mathematics, pdf

• EPSRC project- Theoretical and Implementation advantages of a new lambda notation, (on Automath), web

• Coq

• Freek Wiedijk, the QED manifesto revisited, Nijmegen, 2007, pdf

• A foundation for metareasoning part II: the model theory, pdf

• homotopy type theory and univalent foundations, web

• type theory

• Steward Shapiro: Foundations without Foundationalism: A Case for Second-order Logic, 2000