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