\input utility.ldf
\input common.ldf
\input template.ldf 


\documentclass{article} 





\begin{document}
\title{LaTex Article Template}
\author{P.F. Check}



\begin{abstract}

Proofs in this article can be checked using the
program available at www.proofcheck.org.


\end{abstract}

\maketitle


\section{Introduction}


    
 Put text with mathematical expressions $(x + y)$ here as usual.\footnote{Footnotes work.} 

\section {Foundations}
\label{Foundations}

\subsection {Formal Language}

We use a formal inferential language very close to that of 
Morse \cite{thesets2}.  The language includes 
\begin {itemize}
\item object variables, such as `$x$', `$y$', and `$z$'.
\item sentence variables, such as `$\pvar$', `$\qvar$', and `$\rvar$'.
\item second-order predicates such as `$\pbar x$', `$\qbar x$', and `$\pbarp xy$'.
\item second-order functions  such as `$\ubar x$', `$\vbar x$', `$\ubarp xy$'.
	\end {itemize}
Only object variables are subject to quantification. 

\subsection {Logic}

We use a standard form of sentence logic that includes the 
two Boolean constants `$\true$' (True) and `$\false$' (False). Our predicate 
logic, Alps and Neveln \cite{an},
 is based on indefinite description and two notions of identity. 
It is free of ontological presumptions and, as such, permits expressions which 
denote no object. In the terminology of Shapiro it is a free-variable second-order 
logic.\footnote{See p. 123 of Shapiro \cite{fowofo}.}
The notations of the logic include the following.

	\begin {itemize}
	\item `$\ex x$' means $x$ exists, i.e. `$x$' denotes an object.
Only objects lie in the range of quantification.

	\item `$\an x \pbar x$' represents an object $x$ such that the predicate $\pbar x$
    is true. In the event that $\pbar x$ is false for each object $x$, $\an x \pbar x$
    does not exist.

	\item  `$(x \ident y)$' means $x$ is 
identical to $y$, i.e. `$x$' and `$y$' may be substituted for
    one another without affecting the resulting truth values.
Identity does not imply existence.

	\item `$(x = y)$' means $x$ equals $y$, i.e. `$x$' and `$y$' denote the same object.
Equality does imply existence.

	\item  `$\Some x \pbar x$' means for at least one object $x$, $\pbar x$ is true.
	
	\item  `$\Each x \pbar x$' means for all objects $x$, $\pbar x$ is true.
	
	\item  `$(\pvar \cond x)$' is identical to $x$ if $\pvar$ is true and does 
    not exist otherwise.  It exists if and only if $\pvar$ is true and $x$ exists.
	
	\end {itemize}

All definitions of terms take the form `$(x \ident y)$'.  All definitions of formulas 
take the form
`$(\pvar \Iff \qvar)$'.

\subsection {Proof Syntax}

	Proof steps are justified using dotted numerical references.  References beginning
with a dot refer to some note of the current proof.  Those beginning with
a zero refer to some result ordinarily too obvious for reference but 
listed in an on-line common notions file.   A reference which is followed by
a semi-colon refers to a major premise of the justification; minor premises
follow.  A dash is used to indicate the use of the transitivity of
logical implication.

	Letters used in justifications include:
	\begin {itemize}
	\item G -  for given, which initiates a block of lines 
in which the justified statement is accepted as a hypothesis.
	\item S - for set, which justifies a line which assigns a value to a temporary variable.
	The scope of the variable assignment
terminates with that of the most recent given statement which is still
in effect. 
	\item H - for hence, which terminates the scope of a previously given hypothetical.
It is often used to justify a statement of the
form $(\pvar \c \qvar)$ where $\pvar$ was given earlier as a hypothetical.
	\item U - for universalization, which indicates the universalization
of some referenced statement.
	\end {itemize}

Lines of a proof which begin with the implication sign or some other 
transitive operator break a note into lines which are checked individually.
Later references to such a note refer only to the telescoped note formed
by deleting the intermediate steps.   When `$\true$' is used
to begin a multi-line note
only the last line is accessed by a later reference.  
 
    Adherence to this proof syntax enables proofs to
   be checked for correctness using ProofCheck.\footnote{This program is 
	described in \cite{proofchecking}} 


\subsection {Set Theory}


Our set-class theory is essentially that of Morse-Kelley. The theory admits
a universal class, $\U$, and makes no distinction between set and
class variables. Basic to the theory is a classifier, $\setof
x \pbar x$, with the property that
\begin{quote}

   $(x \in \setof x \pbar x \Iff \pbar x \And x \in \U)$.

\end{quote}
As in Morse's set theory but not as in Kelley's this 
property is a theorem and not an axiom  
scheme (or a theorem scheme).\footnote{Compare Theorem 2{.}35 of \cite{thesets2} with the
axiom scheme on p. 253 of \cite{kelley}.}  Other features of the set theory include:
	\begin {itemize}
	\item Standard axioms such as the axiom of replacement and the power set 
axiom.  The axiom of choice follows immediately from the predicate logic.  Axioms of 
infinity and regularity are included in the theory
but no use of either of these axioms is made before section \ref{univ}. 
	\item Existence preconditions on most defined forms.\footnote{These 
conditions
modify the mathematical substance of the theory less than
modifications resulting from allowances such as letting $(x/y = 0)$ when
$(y = 0)$ as suggested by Suppes.  See p. 18 of  \cite{suppes} for
his discussion of the elimination of existence preconditions.  Indeed the
purpose of imposing explicit existence preconditions is to protect mathematics
from such ad hoc modifications. In effect the logic formalizes the
notion of ``undefined.''  It may be that this logic also plays a role in keeping the length of
complete proofs under control.} 
$(A \cap B)$ exists, for example, only if both $A$ and $B$ exist,  where
to exist just means to be a class.
Similarly $\bigcap x ;\pbar x \ubar x$ exists only if $\ubar x$
exists for all $x$ such that $\pbar x$.  Stronger preconditions
are sometimes imposed:  $\{x\}$ exists, for example, only if $(x \in \U)$.
	\end {itemize}
Notations used include:
	\begin {itemize}
	\item `$\sb A$' represents the set of all subsets of $A$.
We note that 
\lineb $(x \in \sb A \Iff x \subset A \And x \in \U)$.
	\item `$\PI A$' represents the intersection of all the elements of $A$.
	\item `$\bigcap x ; \pbar x \ubar x$' represents the intersection of all 
classes $\ubar x$ such that $\pbar x$.  It should be noted that
this intersection can be written in the form $\PI A$,
where $A$ is the class of all sets $\ubar x$
such that $\pbar x$, only if none of these sets $\ubar x$ are actually proper classes.
	\item `$\SI A$' represents the union of all elements of $A$.
	\item `$\bigcup x ; \pbar x \ubar x$' represents the union of all 
classes $\ubar x$ such that $\pbar x$.  
	\end {itemize}

\section{Content}
\label{content}

Content goes here.



\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}


This section is included primarily to show how standard induction looks
in the context of the results of section \ref{induction}.
The Peano postulates appear as
5.5, 5.6, 4.6, 5.12, and 5.7.  
The only subsequent references to this section
are in the proofs of 6.21, 6.22, and 6.23. 

In 5.1 below the class of natural numbers\footnote{In the common notions file referred
to in these proofs, the designation ``natural number'' is reserved
to structure carrying objects as exemplified by the groups 
of section~\ref{ordinary}.   For consistency sake we should use
the designation ``finite ordinal.''} $\omega$ is defined inductively by
the properties 
\begin{itemize}
\item $(\e \in S)$
\item $(x \in S \c \scsr x \in S)$.
\end{itemize} 

\noindent{}This gives rise to classic induction proofs with a base case and an
induction step.  
If we use $\ubar S$ to stand for the operation 
$(\{\e \}\cup  \bigcup x \in S\{\scsr x \})$ used in 5.1 to define the natural numbers,
we note from 3.26 that it is constricting.
We can then abbreviate theorems 5.2 and 5.4 as follows:

\linea 5.2 $(\ubar \U \subset \U)$

\linea 5.4 $(\ubar \omega = \omega)$ 

Theorem 5.2 shows that
the existence condition in 3.6 is satisfied by the universe $\U$ and results in
the existence of the natural numbers stated in 5.3.  The conclusion 
of the fixed set theorem 3.29 we obtain in 5.4.
Theorems 5.5 and 5.6 merely spell out the inclusion $(\ubar \omega \subset \omega)$.
Theorem 5.7 instantiates the standard induction theorem 3.10. 


\lineb

\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)$
\lineb Proof: 
	\note 1 $(x \in \U \c \{\scsr x\} \subset \U)$ \By 4.3-019.30
	\note 2 $(\bigcup x \in \U \{\scsr x\} \subset \U)$ \By 021.12;(.1 U),09.18
\lineb \Bye 015.33;(019.30;09.19),.2

\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)$
\lineb Proof: 
	\note 1$(\true\c \e \in \{\e\}$ \By 019.3;09.19
    \lineb $\c \e \in (\{\e\}\cup \bigcup x \in \omega\{\scsr x\}))$\By 015.14;(01.27;5.4) 
\lineb     \Bye 5.4,.1

\prop 5.6 $ (x \in \omega \c \scsr x \in \omega)$
\lineb Proof: First we need to note that
	\note 1 $(x \in \omega\c \ex \{\scsr x\})$ \By 09.20-4.3-019.6
\linea Then it follows that 
\note 2 $(x \in \omega\c \{\scsr x \} \subset \bigcup x \in \omega \{\scsr x\}$ \By 021.43;(.1 U)
\linee $\subset \omega$ \By 015.38;5.4
\linec $\c \scsr x \in \omega)$ \By 019.30
\lineb \Bye .2

\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 

\prop 5.9 $(x \in \omega \c x \subset \omega)$
    \lineb Proof:  Set
	\note 1 $(A \ident \setof x \in\omega(x\subset\omega))$ \By S 
\linea Unwrapping .1 yields
	\note 2 $(x \in A \Iff x \in \omega \And x \subset \omega)$ \By 08.6;.1
	\lineb Base Case $(\e \in A)$ 
	\note 3 $(\e \in A)$ \By .2;5.5,(011.20;5.3)
    \lineb Induction Step  $(x \in A \c \scsr x \in A)$
	\note 4 $(x \in A \c x \in \omega \And x\subset\omega$ \By .2
    \linec $\c x\in\omega\And\{x\} \subset \omega \And x \subset\omega$ \By 019.35
    \linec $\c \scsr x\in\omega\And\{x\} \subset \omega \And x \subset\omega$\By 5.6
    \linec $\c \scsr x\in\omega\And x \cup \{x\} \subset \omega $\By 015.31
    \linec $\c \scsr x\in\omega\And\scsr x \subset\omega$ \By 4.1 
    \linec $\c \scsr x \in A)$ \By .2
	\note 5 $(\omega \subset A)$ \By 5.7;.3,(.4 U)
\linea The induction proof is complete and the result follows.
	\note 6 $(x \in \omega\c x \in A$ \By 011.7;.5
	\linec $ \c x \subset \omega)$ \By .2
	\lineb \Bye .6  
\lineb


\prop 5.10 $(\SI \omega = \omega)$
\lineb Proof: On the one hand we have
\note 1 $(\SI \omega \subset \omega)$ \By 023.7;(5.9 U),5.3,5.3
\linea On the other hand
    \note 2 $(x \in \omega\c x \in \omega \And \scsr x \in \omega$ \By 5.6
    \linec $\c x \in \scsr x \in \omega$ \By 09.20- 4.4
    \linec $\c x \in \SI \omega)$ \By 023.15
\linea so 
\note 3 $(\omega \subset \SI \omega )$  \By 011.6;5.3,(023.2;5.3),(.2 U)
	\lineb \Bye  011.11; .1,.3



\prop 5.11 $(x\in\omega\c x\notin x)$
    \lineb Proof:  Set 
	\note 1 $(A \ident \setof x \in\omega(x\notin x))$  \By S
\linea Unwrapping .1 gives us
	\note 2 $(x \in A \Iff x \in \omega \And x \notin x)$ \By 08.6;.1
    \lineb Base Case $(\e \in A)$
	\note 3 $(\true\c  \e \notin \e$ \By 06.6;09.1,09.1 ,09.3
    \lineb $\c \e \in A)$ \By .2;5.5
    \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 \omega)$ \By .2;.4
	\note 6 $(\scsr x \in \omega)$ \By 5.6;.5
\linea Then we have
	\note 7 $(\Not(\scsr x \in A)$
    \linec $ \c \Not(\scsr x \notin \scsr x)$ \By .2;.6
    \linec $ \c \scsr x \in \scsr x$  \By 06.9;(06.1;.6),(06.1;.6)
    \linec $\c \scsr x \in x\Or \scsr x = x$ \By 4.7
    \linec $\c \scsr x \subset x \Or \scsr x = x$ \By 5.8;.5
    \linec $\c \scsr x \subset x$ \By 011.14
    \linec $\c x\in x$ \By  011.7;(4.4;(09.20;.5))
    \linec $\c \Not(x \notin x)$ \By 06.9;(06.1;.5),(06.1;.5)
    \linec $\c \Not(x\in A)$ \By .2;.5
    \linec $\c \false)$ \By .4
    \linea  This is a contradiction.   Hence
	\note 8 $(x \in A \c \scsr x \in A)$ \By .7 H .4
	\note 9 $(\omega \subset A)$ \By 5.7;(.8 U),.3
\linea The induction is finished and the result follows
 \note 10 $(x \in \omega\c x \in A$ \By 011.7;.9
    \linec $\c x \notin x)$ \By .2
    \lineb \Bye .10

The late appearance in 5.12 of the one-to-one
property of the successor operation is due to the fact that the
axiom of regularity is not used.  Otherwise it would follow directly
from 4.8.  

\prop 5.12 $(x\in\omega \And \scsr x = \scsr y 
\c x = y)$.
    \lineb Proof: Given
	\note 1 $(x\in\omega)$\By G
\linea We have
	\note 2 $(x \in y \in x\c x \in y \And y \subset x $ \By 5.8;.1
	\lined $\c x \in x$ \By 011.7
	\lined $\c \false)$  \By 06.5 ;(5.11;.1)
\linea So
	\note 3 $(\scsr x = \scsr y\c x = y \Or x \in y \in x$ \By 4.8
	\linee $\c x = y)$ \By  .2
	\linec \Bye .3 H .1


\section{Conclusion}

More content here.

\bibliographystyle{jflnat}
\bibliography{bibdata}
\end{document}
