Axioms of Mathematics
All structures studied in mathematics should be effectively contained within some universal, total formal system through which we may construct arbitrary mathematical structures.
Mathematics is a field of the most formal and sure nature, so naturally we hope to define mathematics itself formally (that is, by some formal language). The subfield of mathematics concerned with such basic, underlying commonalities between all mathematical structures is termed foundational mathematics, and the modern landscape of the field is divided into several different camps with different foundational structures (and strengths).
For the most part, these foundational considerations are nearly inconsequential for working mathematicians and completely irrelevant for those working in applied math (such as engineering). However, certain frameworks
Structuralism
The viewpoint that mathematics is the study of well-defined structures is a school of thought termed structuralism. This point of view allows us to consider all relevant mathematical objects to be contained within some universal structure. The form of this universal structure is essentially the topic at hand in this article, with three modern approaches covered here (in very brief detail). These include the historical favorite of ZFC set theory (and most uninterested mathematician's default answer); the relatively new, but seemingly powerful homotopy type theory (which is perhaps vaguely familiar to a computer scientist); and the more top-down approach of category theory applied to foundations (as in Lawvere's category of categories).
But first, we should consider what pure logical languages look like.
Underlying Logic
Formal logic consists of a formal language with a set of rules of deduction. These allow us to make statements about the truth value of formal statements about mathematical structures. Hence, most all foundational mathematical theories rely on some form of elementary logic, the most common being classical first order logic, which is discussed briefly below.
First-Order Logic
First order logic adds to the basic constructions of zero-th order logic the additional quantifiers.
Set Theory
Set theory was originally developed by Georg Cantor in the late 19th century as a means to investigate the nature of infinity, or more specifically, infinitely large sets. This formal setting was later taken by some mathematicians, in the simplest way possible, to be the underlying language of all mathematics. These mathematicians essentially asserted that all mathematical structures were definable as a set satisfying some logical or mathematical property. Furthermore, they took any set definable by such means to be well-defined and contained within mathematics. Some time later, however, this naive set theory ran into a seemingly simple problem: some logically defined sets led to apparent contradictions.
History: Set Theory's Origin
For a good, brief introduction to this history and some background justifying a more thoroughly defined set theory (as well as a wonderful discussion of the history leading up to Kurt Godel's famous incompleteness theorems) see the Veritasium video below.
Over time then, this naive set theory was developed again and again into more and more rigorous and complete systems of set theory.
Zermelo-Frankel Set Theory
The standard answer to the question of a foundational language of mathematics is generally set theory with a first order deductive apparatus and the Zermelo-Frankel axioms (ZF), also often with the additional axiom of choice (ZFC).
First order logic and set theory generally lend themselves well to the
The ZFC axioms essentially do one thing: they define the concept of membership of sets such that all relevant logical discourse is only about sets, while avoiding any admittance of self-referential objects, such as those found in the Liar's paradox and Russel's paradox.
Interlude: Intuitionism vs. Constructivism & the Law of the Excluded Middle
An often used proof technique in ZFC set theory is the proof of non-existence by contradiction, and consequently, the existence of things via contradictions derivable from their non-existence.
Constructivist's tend to deny the law of the excluded middle. They say that to prove something exists isn't sufficient; and that, in fact, to prove an object exists is to construct it as some well-defined structure from the foundational structure.
'Univalent foundations' is the phrase used to refer to a new approach to the formal foundations of mathematics that seeks to avoid invoking first-order logic and hence doesn't use sets built on top of this formal apparatus (or sets at all for that matter).
Type Theory
Typically a more constructive approach, intuitionistic type theory, is another, set-independant approach to a formal axiomatization of mathematical foundations.
Martin-Lof type theory was a set of deductive apparatus developed by the Swedish mathematician
homotopy type theory discussion
Homotopy Type Theory
Vovoedsky Univalent axiom
Interlude: Programming Languages & Proof Checkers
Agda and Coq
Curry Howard
Category Theory
Category theory is generally a more top-down approach in it's use as an axiomatic system.
Lawvere's Category of Categories
The Elementary Theory of the Category of Sets (ETCS) is an axiomatic formulation of set theory in the language of category-theory, developed by William Lawvere.
Further Resources
