foundations (Rev #8, changes)

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


  • 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


  • 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

Revision on August 9, 2012 at 23:56:03 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.