# nLab practical foundation of mathematics

foundations

## Foundational axioms

foundational axiom

## Removing axioms

#### Mathematics

Could not include mathematicscontents

# Contents

## Idea

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).

## References

• 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

Revised on November 12, 2014 23:52:37 by Urs Schreiber (82.224.164.72)