<![CDATA[
\input utility.ldf
\input common.ldf
\input indnum.ldf
\documentclass{article}
\begin{document}
\title{Elementary Induction Proof}
\section{The Successor}
\label{successor}
The following proofs, 4.2 through 4.9, can be checked.
Using the renum program changes the numbers of references to these
numbers (such as those in the preceding sentence) as well as the numbers
themselves. To protect numeration not intended for such changes
enclose the dots in TeX braces. I.e. the notation 4{.}2 will not renumber.
\lineb
\noindent{}
Definition
\prop 4.1 $( \scsr x \ident (x \cup \{x\})) $ \By D
\lineb
\noindent{}
Elementary Properties
\prop 4.2 $(\ex \scsr x \Iff x \in \U)$
\lineb Proof:
\note 1 $(\ex \scsr x \Iff \ex (x \cup \{x\}) $ \By 4.1
\lined $ \Iff \ex x \And \ex \{x\} $ \By 015.2
\lined $ \Iff \ex x \And x \in \U $ \By 019.6
\lined $ \Iff x \in \U) $ \By 06.1
\lineb \Bye .1
\prop 4.3 $(\scsr x \in \U \Iff x \in \U)$
\lineb Proof:
\note 1 $(\scsr x \in \U \Iff x \cup \{x\} \in \U $ \By 4.1
\lined $ \Iff x \in \U \And \{x\} \in \U $ \By 015.3
\lined $ \Iff x \in \U)$ \By 019.13
\lineb \Bye .1
\prop 4.4 $(x \in \scsr x \Iff x \in \U)$
\lineb Proof: Given
\note 1 $(x \in \U) $ \By G
\linea We have that
\note 2 $ (\true \c x \in \{x\} $ \By 019.3;.1
\lineb $ \c x \in x \cup \{x\} $ \By 015.13;(06.1;.1)
\lineb $ \c x \in \scsr x)$ \By 4.1
\linea Hence
\note 3 $(x \in \U \c x \in \scsr x)$ \By .2 H .1
\lineb \Bye 09.20,.3
\prop 4.5 $(x \subset \scsr x \Iff x \in \U)$
\lineb Proof: On the one hand
\note 1 $(x \in \U\c \ex \scsr x$ \By 4.2
\linec $\c \ex (x \cup \{x\})$ \By 4.1
\linec $\c x \subset x \cup \{x\}$ \By 015.21
\linec $\c x \subset \scsr x)$ \By 4.1
\linea On the other hand
\note 2 $(x \subset \scsr x\c \ex \scsr x$ \By 011.2
\lined $\c x \in \U)$ \By 4.2
\lineb \Bye .1,.2
\prop 4.6 $\Not (\scsr x = \e)$
\lineb Proof:
\note 1 $(\scsr x = \e\c x \in \scsr x$ \By 01.27-4.2-4.4
\lined $\c \Not(\scsr x = \e))$ \By 09.2-06.21
\lineb \Bye .1
\prop 4.7 $(t \in \scsr x \c t \in x \Or t = x)$
\lineb Proof:
\note 1 $(t \in \scsr x\c t \in x \cup \{x\}$ \By 4.1
\lined $\c t \in x \Or t \in \{x\}$ \By 015.8
\lined $\c t \in x \Or t = x)$ \By 019.18
\lineb \Bye .1
\prop 4.8 $(\scsr x = \scsr y \c x = y \Or x\in y\in x)$
\lineb Proof:
\note 1 $(\scsr x = \scsr y\c \scsr x = \scsr y \And \ex \scsr x$\By 01.27
\linee $\c \scsr x = \scsr y \And x \in \U$\By 4.2
\linee $\c x \in \scsr x = \scsr y $\By 4.4
\linee $\c x \in \scsr y $
\linee $\c x \in y \Or x = y)$ \By 4.7
\linea Hence we take as given
\note 2 $\Not(x = y)$ \By G
\note 3 $(\scsr x = \scsr y\c \scsr x = \scsr y \And \scsr y = \scsr x$ \By 01.19
\linee $\c (x \in y \Or x = y) \And \scsr y = \scsr x$ \By .1
\linee $\c x \in y \And \scsr y = \scsr x$ \By .2
\linee $\c x \in y \And (y \in x \Or y = x)$ \By .1
\linee $\c x \in y \And y \in x)$ \By 01.19;.2
\lineb \Bye .3 H .2
\prop 4.9 $(\SI x \subset x \in \U \c \SI \scsr x = x)$
\lineb Proof: Given
\note 1 $(\SI x \subset x)$ \By G
\note 2 $(x \in \U)$ \By G
\linea We get that
\note 3 $(\SI \scsr x \ident \SI (x \cup \{x\})$ \By 4.1
\lined $\ident \SI x \cup \SI \{x\}$ \By 023.17
\lined $\ident \SI x \cup x$ \By 019.16;.2
\lined $= x)$ \By 015.28;.1
\lineb \Bye .3 H .1,.2
\lineb
\section{Natural Numbers}
\label{naturals}
\noindent{}
Definition
\prop 5.1 $(\omega \ident \Closure S(\{\e \}\cup \bigcup x \in S\{\scsr x \}))$ \By D
\lineb
\noindent{}
Enabling Lemma
\prop 5.2 $ (\{\e \}\cup \bigcup x \in \U \{\scsr x \}\subset\U)$
\noindent{} First Consequences of the Induction Theorems
\prop 5.3 $ \ex \omega$
\lineb Proof depends on a general existence theorem.
\lineb
\prop 5.4 $(\{\e \}\cup\bigcup x\in \omega\{\scsr x \} = \omega)$
\lineb Proof depends on a fixed set theorem.
\lineb
\prop 5.5 $(\e \in \omega)$
\prop 5.6 $ (x \in \omega \c \scsr x \in \omega)$
\prop 5.7 $(\e \in A \And \Each x \in A
(\scsr x \in A) \c \omega \subset A)$
\lineb Proof depends on a general induction theorem.
\noindent{}
Elementary Properties
\prop 5.8 $(y \in x \in \omega \c y \subset x)$
\lineb Proof: Set
\note 1 $(A \ident \setof x \Each y\in x(y\subset x))$ \By S
\linea We use 5.7 to show that $A$ contains $\omega$. First we unwrap .1.
\note 2 $(t \in A \Iff \Each y \in t (y \subset t) \And t \in \U)$ \By 08.3;.1
\lineb Base Case $(\e \in A )$~.
\note 3 $(\e \in A)$ \By .2;09.19,09.12
\lineb Induction Step $(x \in A \c \scsr x \in A)$~.
\linea Given
\note 4 $(x \in A )$ \By G
\linea We note first that
\note 5 $(x \in \U)$ \By 09.20;.4
\note 6 $\Each y \in x(y \subset x)$\By .2;.4
\linea Then we have
\note 7 $(y \in \scsr x \c y \in x \Or y = x$ \By 4.7
\lined $\c y \subset x \Or y = x$ \By .6
\lined $\c y \subset x $ \By 011.14
\lined $\c y \subset \scsr x )$ \By 011.10;( 4.5;(09.20;.4))
\note 8 $(\scsr x \in A)$ \By .2;(4.3;.5),(.7 U)
\linea Hence
\note 9 $(x \in A \c \scsr x \in A)$ \By .8 H .4
\note 10 $(\omega \subset A)$ \By 5.7;.3,(.9 U)
\linea The induction proof is complete and the conclusion follows directly.
\note 11 $(y \in x \And x \in \omega\c y \in x \And x \in A$ \By 011.7;.10
\linee $\c y \in x \And \Each y \in x(y \subset x)$ \By .2
\linee $\c y \subset x)$
\lineb \Bye .11
\section{Conclusion}
More content here.
\end{document}
]]>