natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
further
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).
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 October 18, 2022 at 05:06:33. See the history of this page for a list of all contributions to it.