From e7cd189557781eada78ef85a7f09a4ebcbddc633 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 1 Aug 2023 13:17:30 -0600 Subject: [PATCH] Enderton. Draft theorems/exercises on arithmetic section. --- Bookshelf/Enderton/Set.tex | 183 ++++++++++++++++++++++++++++++++++++- 1 file changed, 178 insertions(+), 5 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 893c714..2fc343a 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -22,6 +22,28 @@ \chapter{Reference}% \hyperlabel{chap:reference} +\section{\defined{Addition}}% +\label{ref:addition} + +For each $m \in \omega$, there exists (by the + \nameref{sub:recursion-theorem-natural-numbers}) a unique + \nameref{ref:function} $A_m \colon \omega \rightarrow \omega$ for which + \begin{align*} + A_m(0) & = m, \\ + A_m(n^+) & = A_m(n)^+ & \text{for } n \text{ in } \omega. + \end{align*} +\textbf{Addition} ($+$) is the \nameref{ref:binary-operation} on $\omega$ such + that for any $m$ and $n$ in $\omega$, $$m + n = A_m(n).$$ +Thus when written as a \nameref{ref:relation}, + $$+ = \{\pair{\pair{m, n}, p} \mid + m \in \omega \land n \in \omega \land p = A_m(n)\}.$$ + +\begin{definition} + + \lean*{Init/Prelude}{Add.add} + +\end{definition} + \section{\defined{Axiom of Choice, First Form}}% \hyperlabel{ref:axiom-of-choice-1} @@ -46,6 +68,12 @@ For any set $I$ and any function $H$ with domain $I$, if $H(i) \neq \emptyset$ \end{axiom} +\section{\defined{Binary Operation}}% +\hyperlabel{ref:binary-operation} + +A \textbf{binary operation} on a set $A$ is a \nameref{ref:function} from + $A \times A$ into $A$. + \section{\defined{Cartesian Product}}% \hyperlabel{ref:cartesian-product} @@ -341,6 +369,25 @@ A \textbf{linear ordering} on $A$ (also called a \textbf{total ordering} on $A$) \end{definition} +\section{\defined{Multiplication}}% +\hyperlabel{sec:multiplication} + +For each $m \in \omega$, there exists (by the + \nameref{sub:recursion-theorem-natural-numbers}) a unique + \nameref{ref:function} $M_m \colon \omega \rightarrow \omega$ for which + \begin{align*} + M_m(0) & = 0, \\ + M_m(n^+) = M_m(n) + m. + \end{align*} +\textbf{Multiplication} ($\cdot$) is the \nameref{ref:binary-operation} on + $\omega$ such that for any $m$ and $n$ in $\omega$, $$m \cdot n = M_m(n).$$ + +\begin{definition} + + \lean*{Init/Prelude}{Mul.mul} + +\end{definition} + \section{\defined{Natural Number}}% \hyperlabel{ref:natural-number} @@ -6249,7 +6296,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. $\dom{h} = \omega$, and (iv) $h$ is unique. \paragraph{(i)}% - \label{par:recursion-theorem-natural-numbers-i} + \hyperlabel{par:recursion-theorem-natural-numbers-i} We prove that $h$ is a function. Consider set @@ -6257,7 +6304,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. We show (1) that $0 \in S$ and (2) if $n \in S$ then $n^+ \in S$. \subparagraph{(1)}% - \label{spar:recursion-theorem-natural-numbers-i-1} + \hyperlabel{spar:recursion-theorem-natural-numbers-i-1} Suppose $0 \in \dom{h}$. By construction, there must exist some $y_1 \in A$ and acceptable function @@ -6269,7 +6316,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. Therefore $0 \in S$. \subparagraph{(2)}% - \label{spar:recursion-theorem-natural-numbers-i-2} + \hyperlabel{spar:recursion-theorem-natural-numbers-i-2} Suppose $n$ and $n^+$ are members of $\dom{h}$. By construction, there must exist some $y_1 \in A$ and acceptable function @@ -6294,7 +6341,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. In other words, $h$ is a function. \paragraph{(ii)}% - \label{par:recursion-theorem-natural-numbers-ii} + \hyperlabel{par:recursion-theorem-natural-numbers-ii} We now prove $h \in H$, i.e. $h$ is an acceptable function. It trivially holds that $\dom{h} \subseteq \omega$ and @@ -6321,7 +6368,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. Hence $h \in H$. \paragraph{(iii)}% - \label{par:recursion-theorem-natural-numbers-iii} + \hyperlabel{par:recursion-theorem-natural-numbers-iii} We now prove that $\dom{h} = \omega$. We show that (1) $0 \in \dom{h}$ and (2) if $n \in \dom{h}$ then @@ -6414,6 +6461,74 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} +\section{Arithmetic}% +\hyperlabel{sec:arithmetic} + +\subsection{\sorry{Theorem 4I}} +\hyperlabel{sub:theorem-4i} + +\begin{theorem}[4I] + + For natural numbers $m$ and $n$, + \begin{align*} + m + 0 & = m, \\ + m + n^+ & = (m + n)^+. + \end{align*} + +\end{theorem} + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Theorem 4J}} +\hyperlabel{sub:theorem-4j} + +\begin{theorem}[4J] + + For natural numbers $m$ and $n$, + \begin{align*} + m \cdot 0 & = 0, \\ + m \cdot n^+ & = m \cdot n + m. + \end{align*} + +\end{theorem} + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Theorem 4K}} +\hyperlabel{sub:theorem-4k} + +\begin{theorem}[4K] + + The following identities hold for all natural numbers. + \begin{enumerate} + \item Associative law for addition + $$m + (n + p) = (m + n) + p.$$ + \item Commutative law for addition + $$m + n = n + m.$$ + \item Distributive law + $$m \cdot (n + p) = m \cdot n + m \cdot p.$$ + \item Associative law for multiplication + $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$ + \item Commutative law for multiplication + $$m \cdot n = n \cdot m.$$ + \end{enumerate} + +\end{theorem} + +\begin{proof} + + TODO + +\end{proof} + \section{Exercises 4}% \hyperlabel{sec:exercises-4} @@ -6781,4 +6896,62 @@ Formulate an analogue to Exercise 9 for a function \end{proof} +\subsection{\sorry{Exercise 4.13}}% +\hyperlabel{sub:exercise-4.13} + +Let $m$ and $n$ be natural numbers such that $m \cdot n = 0$. +Show that either $m = 0$ or $n = 0$. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 4.14}}% +\hyperlabel{sub:exercise-4.14} + +Call a natural number \textit{even} if it has the form $2 \cdot m$ for some $m$. +Call it \textit{odd} if it has the form $(2 \cdot p) + 1$ for some $p$. +Show that each natural number is either even or odd, but never both. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 4.15}}% +\hyperlabel{sub:exercise-4.15} + +Complete the proof of part (1) of \nameref{sub:theorem-4k}. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 4.16}}% +\hyperlabel{sub:exercise-4.16} + +Complete the proof of part (5) of \nameref{sub:theorem-4k}. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 4.17}}% +\hyperlabel{sub:exercise-4.17} + +Prove that $m^{n+p} = m^n \cdot m^p$. + +\begin{proof} + + TODO + +\end{proof} + \end{document}