\chapter{Axiomatic systems}

\section{Introduction to axiomatic systems}

Here are some common axiomatic set theories
\begin{itemize}
\item ZFC
\item NBG 
\item MK
\end{itemize}

Here are some common axiomatic systems for synthetic geometry
\begin{itemize}
\item Euclidean geometry (Hilbert's axioms)
\item Euclidean geometry (Tarski's axioms)
\end{itemize}

Peano arithmetic is the common axiomatic system used for arithmetic and much of elementary number theory.




\section{Peano arithmetic}

Set theories are useful extensions upon mathematical logic, but mathematicians have discovered axiomatic systems for specific fields of mathematics that avoid set theories.

It's worth noting that a model of Peano arithmetic can be created within various set theories and type theories
A system of axioms that creates arithmetic and number theory. It doesn't require 
Establishes number theory

compatible with ZFC

We will form the axioms under the assumption that we are following ZFC.

$0\in \mathbb{N}$
$x=x$
$x=y \implies y=x$
$x=y \land y=z \implies x=z$
$a\in \mathbb{N} \land a=b \implies b\in \mathbb{N}$
$n \in \mathbb{N} \implies s(n) \in \mathbb{N}$
$s \text{ is injective}$
$\nexists n ( s(n)=0 )$
$0 \in K \land [ k \in K \implies s(k) \in K]  \implies K =\mathbb{N}$


This essentially forms the field on number theory, and one can derive definitions for more complex classes of numbers (integers, rational numbers, real numbers, complex numbers, quaternions, etc.) based on the natural numbers; forming fields such as real and complex analysis.

Note that axiom 9 can be reformulated in second order logic rather than ZFC

Our successor function would ideally be $s(n)=n+1$ so that we can inductively define all the natural numbers. Unfortunately, we haven't defined what $1$ or $+$ means. This means that we're going to have to form the conditions on $s$ using ideas from mathematical logic and set theory rather than arithmetic, since artihmetic doesn't 'exist' yet.

\chapter{Euclidean geometry}


Establishes geometry

Euclid's axioms
Hilbert's axioms
Tarski's axioms