practical foundation of mathematics



Type theory





In the context of foundations of mathematics the term practical foundations (following a term introduced in (Taylor)) refers to emphasis on conceptually natural formalizations.

In my own education I was fortunate to have two teachers who used the term “foundations” in a common-sense way (rather than in the speculative way of the Bolzano-Frege-Peano-Russell tradition). This way is exemplified by their work in Foundations of Algebraic Topology, published in 1952 by Eilenberg (with Steenrod), and The Mechanical Foundations of Elasticity and Fluid Mechanics, published in the same year by Truesdell. The orientation of these works seemed to be “concentrate the essence of practice and in turn use the result to guide practice”. (Lawvere 2003: 213)

Formal systems of interest here are natural deduction in type theories, which allow natural expressions for central concepts in mathematics, notably via their categorical semantics and the conceptual strength of category theory (see Harper).


  • Paul Taylor, Practical Foundations of Mathematics, Cambridge University Press (web)
  • William Lawvere, Foundations and applications: axiomatization and education, Bulletin of Symbolic Logic 9 (2003), 213-224 (ps)

Under computational trinitarianism this corresponds to a practical foundation in programming, laid out in

A foundation for algebraic topology in this practical spirit is laid out in

Last revised on November 12, 2014 at 23:52:37. See the history of this page for a list of all contributions to it.