Elementary Functional ArithmeticElementaryFunctionalArithmetic2002-08-17 22:47:152002-08-17 23:35:02Definition% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands here
%\PMlinkescapeword{theory}\emph{Elementary Functional Arithmetic}, or EFA, is a weak theory of arithmetic created by removing induction from Peano Arithmetic. Because it lacks induction, axioms defining exponentiation must be added.
\begin{itemize}
\item $\forall x (x'\neq 0)$ ($0$ is the first number)
\item $\forall x,y (x'=y'\rightarrow x=y)$ (the successor function is one-to-one)
\item $\forall x (x+0=x)$ ($0$ is the additive identity)
\item $\forall x,y(x+y'=(x+y)')$ (addition is the repeated application of the successor function)
\item $\forall x(x\cdot 0=0)$
\item $\forall x,y(x\cdot(y')=x\cdot y+x$ (multiplication is repeated addition)
\item $\forall x(\neg (x<0))$ ($0$ is the smallest number)
\item $\forall x,y(x<y'\leftrightarrow x<y\vee x=y)$
\item $\forall x(x^0=1)$
\item $\forall x(x^{y'}=x^y\cdot x)$
\end{itemize}