From f3284407971feb837189a9f9efb97580020a86c0 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Fri, 21 Jul 2023 13:40:38 -0600
Subject: [PATCH] Enderton. Peano systems.

---
 Bookshelf/Enderton/Set.tex | 62 +++++++++++++++++++++++++++++++++++++-
 Common/Set.lean            |  3 +-
 Common/Set/Interval.lean   |  2 --
 Common/Set/Partition.lean  |  4 ---
 Common/Set/Peano.lean      | 42 ++++++++++++++++++++++++++
 5 files changed, 105 insertions(+), 8 deletions(-)
 create mode 100644 Common/Set/Peano.lean

diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index cb08678..5296c28 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -419,6 +419,25 @@ A \textbf{partition} $\Pi$ of a set $A$ is a set of nonempty subsets of $A$ that
 
 \end{definition}
 
+\section{\defined{Peano System}}%
+\hyperlabel{ref:peano-system}
+
+A \textbf{Peano system} is a triple $\langle N, S, e \rangle$ consisting of a
+  set $N$, a function $S \colon N \rightarrow N$, and a member $e \in N$ such
+  that the following three conditions are met:
+\begin{enumerate}[(i)]
+  \item $e \not\in \ran{S}$.
+  \item $S$ is one-to-one.
+  \item Every subset $A$ of $N$ containing $e$ and closed under $S$ is $N$
+    itself.
+\end{enumerate}
+
+\begin{definition}
+
+  \lean*{Common/Set/Peano}{Peano.System}
+
+\end{definition}
+
 \section{\defined{Power Set}}%
 \hyperlabel{ref:power-set}
 
@@ -6015,11 +6034,52 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
+\section{Peano's Postulates}%
+\hyperlabel{sec:peanos-postulates}
+
+\subsection{\verified{Theorem 4D}}%
+\hyperlabel{sub:theorem-4d}
+
+\begin{theorem}[4D]
+
+  $\langle \omega, \sigma, 0 \rangle$ is a Peano system.
+
+\end{theorem}
+
+\begin{proof}
+
+  \lean{Common/Set/Peano}{Peano.instSystemNatUnivSuccOfNatInstOfNatNat}
+
+  Note $\sigma$ is defined as $\sigma = \{\pair{n, n^+} \mid n \in \omega\}$.
+  To prove $\langle \omega, \sigma, 0 \rangle$ is a \nameref{ref:peano-system},
+    we must show that (i) $0 \not\in \ran{S}$, (ii) $\sigma$ is one-to-one, and
+    (iii) every subset $A$ of $\omega$ containing $0$ and closed under $\sigma$
+    is $\omega$ itself.
+
+  \paragraph{(i)}%
+
+    This follows immediately from \nameref{sub:theorem-4c}.
+
+  \paragraph{(ii)}%
+
+    Let $n^+ \in \ran{\sigma}$.
+    By construction, there exists some $m_1 \in \omega$ such that $m_1 = n^+$.
+    Suppose there exists some $m_2 \in \omega$ such that $m_2 = n^+$.
+    By definition of the \nameref{ref:successor}, $m_1 = n \cup \{n\} = m_2$.
+    By the \nameref{ref:extensionality-axiom}, $m_1 = m_2$.
+    Thus $\sigma$ is one-to-one.
+
+  \paragraph{(iii)}%
+
+    This follows immediately from \nameref{sub:theorem-4b}.
+
+\end{proof}
+
 \section{Exercises 4}%
 \hyperlabel{sec:exercises-4}
 
 \subsection{\verified{Exercise 4.1}}%
-\label{sub:exercise-4.1}
+\hyperlabel{sub:exercise-4.1}
 
 Show that $1 \neq 3$ i.e., that $\emptyset^+ \neq \emptyset^{+++}$.
 
diff --git a/Common/Set.lean b/Common/Set.lean
index ae92e76..4be289c 100644
--- a/Common/Set.lean
+++ b/Common/Set.lean
@@ -1,3 +1,4 @@
 import Common.Set.Basic
 import Common.Set.Interval
-import Common.Set.Partition
\ No newline at end of file
+import Common.Set.Partition
+import Common.Set.Peano
\ No newline at end of file
diff --git a/Common/Set/Interval.lean b/Common/Set/Interval.lean
index 1965c5f..b698cb2 100644
--- a/Common/Set/Interval.lean
+++ b/Common/Set/Interval.lean
@@ -1,8 +1,6 @@
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Intervals.Basic
 
-import Common.List.Basic
-
 /-! # Common.Set.Interval
 
 A representation of a range of values.
diff --git a/Common/Set/Partition.lean b/Common/Set/Partition.lean
index ef27e09..8b2ee8a 100644
--- a/Common/Set/Partition.lean
+++ b/Common/Set/Partition.lean
@@ -1,7 +1,3 @@
-import Mathlib.Data.Finset.Basic
-import Mathlib.Data.List.Sort
-import Mathlib.Data.Set.Intervals.Basic
-
 import Common.List.Basic
 import Common.List.NonEmpty
 import Common.Set.Interval
diff --git a/Common/Set/Peano.lean b/Common/Set/Peano.lean
new file mode 100644
index 0000000..4ebbdc9
--- /dev/null
+++ b/Common/Set/Peano.lean
@@ -0,0 +1,42 @@
+import Mathlib.Data.Rel
+import Mathlib.Data.Set.Basic
+
+/-! # Common.Set.Peano
+
+Data types and theorems used to define Peano systems.
+-/
+
+namespace Peano
+
+/--
+A `Peano system` is a triple `⟨N, S, e⟩` consisting of a set `N`, a function
+`S : N → N`, and a member `e ∈ N` such that the following three conditions are
+met:
+
+1. `e ∉ ran S`.
+2. `S` is one-to-one.
+3. Every subset `A` of `N` containing `e` and closed under `S` is `N` itself.
+-/
+class System (N : Set α) (S : α → α) (e : α) where
+  zero_range : e ∉ Set.range S
+  injective : Function.Injective S
+  induction : ∀ A, A ⊆ N ∧ e ∈ A ∧ (∀ a ∈ A, S a ∈ A) → A = N
+
+instance : System (N := @Set.univ ℕ) (S := Nat.succ) (e := 0) where
+  zero_range := by
+    simp
+  injective := by
+    intro x₁ x₂ h
+    injection h
+  induction := by
+    intro A h
+    suffices Set.univ ⊆ A from Set.Subset.antisymm h.left this
+    show ∀ n, n ∈ Set.univ → n ∈ A
+    intro n hn
+    induction n with
+    | zero => exact h.right.left
+    | succ n ih =>
+      refine h.right.right n (ih ?_)
+      simp
+
+end Peano
\ No newline at end of file