Enderton. Peano systems.

finite-set-exercises
Joshua Potter 2023-07-21 13:40:38 -06:00
parent 9b8ddd2b0d
commit f328440797
5 changed files with 105 additions and 8 deletions

View File

@ -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^{+++}$.

View File

@ -1,3 +1,4 @@
import Common.Set.Basic
import Common.Set.Interval
import Common.Set.Partition
import Common.Set.Partition
import Common.Set.Peano

View File

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

View File

@ -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

42
Common/Set/Peano.lean Normal file
View File

@ -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