First Principles Mathematics

This is a draft outlining original resources that could be made to describe the foundational constructions of mathematics with the following goals:

Literal, well motivated definitions, rather than arbitrary and convenient definitions
Clear distinction between constructive algorithms and non-constructive proofs
Presentation of statements in a way that strengthens intuition rather than confounding it
Only building axiomatic/structural theories after the individual exemplars have been built and studied
Use of state-of-the-art or original techniques whenever genuinely superior to historical ones, e.g. geometric algebra, rational trigonometry
Explicit argument for how techniques can be generalized, if not a symbolic proof then mechanized, general instructions for how a symbolic proof could be constructed for relevant cases

Logical Foundations

This section is the most esoteric, but does logically come first. The aim of this resource is to demonstrate a philosophically rigorous construction of the mathematics people take for granted, for the benefits of clearer understanding of how mathematical results come to be, and sharper ability to reason in general, that is, as an exercise in logical intuition. In the context of logical intuition, mathematics can be seen as the construction of cognitive and typographic symbols, and valid logical arguments about those symbols or the physical objects those symbols might signify. We can go further and create symbols to represent the phenomenon of argument itself, which can be useful in systematizing and mechanizing the process of verifying argument, but will not be taken as being at all necessary for an argument to be valid, rather logical models and type theories will be taken as their own subject of discussion, described in terms of natural language like anything else.

Since we take the written symbol as the fundamental object of mathematics, as opposed to the set, category, type, or homotopy, it becomes a very interesting question to explore the way that symbols and their referants are identified with each other, that is, the way that symbols and their referants are interpreted as being the same. In many formal approaches to mathematics, objects are identified formally by constructing either a set quotient or a groupoid that makes the identification literal, or identification is taken as merely a quirk of notation, but implicit in all arguments about characterization is the intuition that the things being characterized are somehow the same thing; this does not need to remain implicit, we can bring it to the fore, and treat the set quotients as a self-referential quirk similar to the models and type theories.

Counting and Common Arithmetic

In everyday life counting arises as a technique for coordinating physical objects, and the very beginnings of mathematics arise directly out of increasingly sophisticated methods of coordinating these physical objects. We can understand counting and whole-numbered quantities as a description of properties of physical collections, we can develop techniques of account for objects by manipulating symbols that signify these quantities, and eventually realize the constitutive power of these symbols as a basis for increasingly rich and expressive number systems. It is this last aspect of counting and common numbers that we aim to establish, and so we should describe:

The visually discernible quantities one, two, three, e.g. *, ||, •••
practical phenomenology of small quantities: connectedness, reflective symmetry, bijectivity
incremental counting for reasoning about larger bijections (incrementation is a more practical and pre-numerical version of mathematical induction)
addition as an invariant of counting multiple collections
multiplication as addition of equal sized collections
arithmetic procedures, arithmetic expressions, arithmetic identities
algebraic equations as symbols representing possible identities
subtraction and divisors as possible identities
basic number theory of Euclidean division, greatest common divisors, prime factors

Integers and Rationals

While not all subtractions or divisions have a well defined result, the difference or ratio between pairs of numbers is still an important quantity of those pairs, and by taking those pairs as a new mathematical object, and identifying them based on their difference or ratio, we can construct new number systems. The integers are useful in accounting, and the rationals are useful in measuring physical quantities with arbitrary precision, rather than the fixed precision of any given unit of measurement. Once again we avoid both of these practical concerns and primarily construct and reason about these systems for their use as constituents of even richer objects such as polynomials, quadratic extensions, the rational number line, geometric manifolds, rational functions, and even Cauchy sequences and Dedekind cuts.

High level topics

With the full rational number line in place many aspects of mathematics become possible to explore:

Rational functions, metric analysis, cut continuity, Cauchy continuity, uniform continuity
manifolds, topology, standard topological continuity
limits, completion, (real numbers) uncountability
basic differential geometry, tangent vectors
countable/topological measure theory
polynomials and simplifying algebraic expressions, field extensions
linear algebra, vector spaces
geometric algebra, rotors and spinors
type systems, type checking, univalence
formal construction of graphs, connected components, communicating classes