0 \wedge e_0 \in \mbox{\em CN} ) \}$. A {\em constant-variable pair}\index{constant-variable pair} is an expression of length 2 whose first term is a constant and whose second term is a variable. We denote the set of all constant-variable pairs by $\mbox{\em EX}_2 = \{ e \in \mbox{\em EX}_C | ( |e| = 2 \wedge e_1 \in \mbox{\em VR} ) \}$. {\footnotesize\begin{quotation} {\em Relationship to Metamath.} In general, the set $\mbox{\em SM}$ corresponds to the set of declared math symbols in a Metamath database, the set $\mbox{\em CN}$ to those declared with \texttt{\$c} statements, and the set $\mbox{\em VR}$ to those declared with \texttt{\$v} statements. Of course a Metamath database can only have a finite number of math symbols, whereas formal systems in general can have an infinite number, although the number of Metamath math symbols available is in principle unlimited. The set $\mbox{\em EX}_C$ corresponds to the set of permissible expressions for \texttt{\$e}, \texttt{\$a}, and \texttt{\$p} statements. The set $\mbox{\em EX}_2$ corresponds to the set of permissible expressions for \texttt{\$f} statements. \end{quotation}} We denote by ${\cal V}(e)$ the set of all variables in an expression $e \in \mbox{\em EX}$, i.e.\ the set of all $\alpha \in \mbox{\em VR}$ such that $\alpha = e_n$ for some $n < |e|$. We also denote (with abuse of notation) by ${\cal V}(E)$ the set of all variables in a collection of expressions $E \subseteq \mbox{\em EX}$, i.e.\ $\bigcup _{e \in E} {\cal V}(e)$. \subsection{Substitution} Given a function $F$ from $\mbox{\em VR}$ to $\mbox{\em EX}$, we denote by $\sigma_{F}$ or just $\sigma$ the function from $\mbox{\em EX}$ to $\mbox{\em EX}$ defined recursively for nonempty sequences by \begin{eqnarray*} & \sigma(<\alpha>) = F(\alpha) & \mbox{for\ } \alpha \in \mbox{\em VR}; \\ & \sigma(<\alpha>) = <\alpha> & \mbox{for\ } \alpha \not\in \mbox{\em VR}; \\ & \sigma(g \frown h) = \sigma(g) \frown \sigma(h) & \mbox{for\ } g,h \in \mbox{\em EX}. \end{eqnarray*} We also define $\sigma(\varnothing)=\varnothing$. We call $\sigma$ a {\em simultaneous substitution}\index{substitution!variable}\index{variable substitution} (or just {\em substitution}) with {\em substitution map}\index{substitution map} $F$. We also denote (with abuse of notation) by $\sigma(E)$ a substitution on a collection of expressions $E \subseteq \mbox{\em EX}$, i.e.\ the set $\{ \sigma(e) | e \in E \}$. The collection $\sigma(E)$ may of course contain fewer expressions than $E$ because duplicate expressions could result from the substitution. \subsection{Statements} We denote by $\mbox{\em DV}$ the set of all unordered pairs $\{\alpha, \beta \} \subseteq \mbox{\em VR}$ such that $\alpha \neq \beta$. $\mbox{\em DV}$ stands for ``distinct variables.'' A {\em pre-statement}\index{pre-statement!in a formal system} is a quadruple $\langle D,T,H,A \rangle$ such that $D\subseteq \mbox{\em DV}$, $T\subseteq \mbox{\em EX}_2$, $H\subseteq \mbox{\em EX}_C$ and $H$ is finite, $A\in \mbox{\em EX}_C$, ${\cal V}(H\cup\{A\}) \subseteq {\cal V}(T)$, and $\forall e,f\in T {\ } {\cal V}(e) \neq {\cal V}(f)$ (or equivalently, $e_1 \ne f_1$) whenever $e \neq f$. The terms of the quadruple are called {\em distinct-variable restrictions},\index{disjoint-variable restriction!in a formal system} {\em variable-type hypotheses},\index{variable-type hypothesis!in a formal system} {\em logical hypotheses},\index{logical hypothesis!in a formal system} and the {\em assertion}\index{assertion!in a formal system} respectively. We denote by $T_M$ ({\em mandatory variable-type hypotheses}\index{mandatory variable-type hypothesis!in a formal system}) the subset of $T$ such that ${\cal V}(T_M) ={\cal V}(H \cup \{A\})$. We denote by $D_M=\{\{\alpha,\beta\}\in D|\{\alpha,\beta\}\subseteq {\cal V}(T_M)\}$ the {\em mandatory distinct-variable restrictions}\index{mandatory disjoint-variable restriction!in a formal system} of the pre-statement. The set of {\em mandatory hypotheses}\index{mandatory hypothesis!in a formal system} is $T_M\cup H$. We call the quadruple $\langle D_M,T_M,H,A \rangle$ the {\em reduct}\index{reduct!in a formal system} of the pre-statement $\langle D,T,H,A \rangle$. A {\em statement} is the reduct of some pre-statement\index{statement!in a formal system}. A statement is therefore a special kind of pre-statement; in particular, a statement is the reduct of itself. {\footnotesize\begin{quotation} {\em Comment.} $T$ is a set of expressions, each of length 2, that associate a set of constants (``variable types'') with a set of variables. The condition ${\cal V}(H\cup\{A\}) \subseteq {\cal V}(T) $ means that each variable occurring in a statement's logical hypotheses or assertion must have an associated variable-type hypothesis or ``type declaration,'' in analogy to a computer programming language, where a variable must be declared to be say, a string or an integer. The requirement that $\forall e,f\in T \, e_1 \ne f_1$ for $e\neq f$ means that each variable must be associated with a unique constant designating its variable type; e.g., a variable might be a ``wff'' or a ``set'' but not both. Distinct-variable restrictions are used to specify what variable substitutions are permissible to make for the statement to remain valid. For example, in the theorem scheme of set theory $\lnot\forall x\,x=y$ we may not substitute the same variable for both $x$ and $y$. On the other hand, the theorem scheme $x=y\to y=x$ does not require that $x$ and $y$ be distinct, so we do not require a distinct-variable restriction, although having one would cause no harm other than making the scheme less general. A mandatory variable-type hypothesis is one whose variable exists in a logical hypothesis or the assertion. A provable pre-statement (defined below) may require non-mandatory variable-type hypotheses that effectively introduce ``dummy'' variables for use in its proof. Any number of dummy variables might be required by a specific proof; indeed, it has been shown by H.\ Andr\'{e}ka\index{Andr{\'{e}}ka, H.} \cite{Nemeti} that there is no finite upper bound to the number of dummy variables needed to prove an arbitrary theorem in first-order logic (with equality) having a fixed number $n>2$ of individual variables. (See also the Comment on p.~\pageref{nodd}.) For this reason we do not set a finite size bound on the collections $D$ and $T$, although in an actual application (Metamath database) these will of course be finite, increased to whatever size is necessary as more proofs are added. \end{quotation}} {\footnotesize\begin{quotation} {\em Relationship to Metamath.} A pre-statement of a formal system corresponds to an extended frame in a Metamath database (Section~\ref{frames}). The collections $D$, $T$, and $H$ correspond respectively to the \texttt{\$d}, \texttt{\$f}, and \texttt{\$e} statement collections in an extended frame. The expression $A$ corresponds to the \texttt{\$a} (or \texttt{\$p}) statement in an extended frame. A statement of a formal system corresponds to a frame in a Metamath database. \end{quotation}} \subsection{Formal Systems} A {\em formal system}\index{formal system} is a triple $\langle \mbox{\em CN},\mbox{\em VR},\Gamma\rangle$ where $\Gamma$ is a set of statements. The members of $\Gamma$ are called {\em axiomatic statements}.\index{axiomatic statement!in a formal system} Sometimes we will refer to a formal system by just $\Gamma$ when $\mbox{\em CN}$ and $\mbox{\em VR}$ are understood. Given a formal system $\Gamma$, the {\em closure}\index{closure}\footnote{This definition of closure incorporates a simplification due to Josh Purinton.\index{Purinton, Josh}} of a pre-statement $\langle D,T,H,A \rangle$ is the smallest set $C$ of expressions such that: %\begin{enumerate} % \item $T\cup H\subseteq C$; and % \item If for some axiomatic statement % $\langle D_M',T_M',H',A' \rangle \in \Gamma_A$, for % some $E \subseteq C$, some $F \subseteq C-T$ (where ``-'' denotes % set difference), and some substitution % $\sigma$ we have % \begin{enumerate} % \item $\sigma(T_M') = E$ (where, as above, the $M$ denotes the % mandatory variable-type hypotheses of $T^A$); % \item $\sigma(H') = F$; % \item for all $\{\alpha,\beta\}\in D^A$ and $\subseteq % {\cal V}(T_M')$, for all $\gamma\in {\cal V}(\sigma(\langle \alpha % \rangle))$, and for all $\delta\in {\cal V}(\sigma(\langle \beta % \rangle))$, we have $\{\gamma, \delta\} \in D$; % \end{enumerate} % then $\sigma(A') \in C$. %\end{enumerate} \begin{list}{}{\itemsep 0.0pt} \item[1.] $T\cup H\subseteq C$; and \item[2.] If for some axiomatic statement $\langle D_M',T_M',H',A' \rangle \in \Gamma$ and for some substitution $\sigma$ we have \begin{enumerate} \item[a.] $\sigma(T_M' \cup H') \subseteq C$; and \item[b.] for all $\{\alpha,\beta\}\in D_M'$, for all $\gamma\in {\cal V}(\sigma(\langle \alpha \rangle))$, and for all $\delta\in {\cal V}(\sigma(\langle \beta \rangle))$, we have $\{\gamma, \delta\} \in D$; \end{enumerate} then $\sigma(A') \in C$. \end{list} A pre-statement $\langle D,T,H,A \rangle$ is {\em provable}\index{provable statement!in a formal system} if $A\in C$ i.e.\ if its assertion belongs to its closure. A statement is {\em provable} if it is the reduct of a provable pre-statement. The {\em universe}\index{universe of a formal system} of a formal system is the collection of all of its provable statements. Note that the set of axiomatic statements $\Gamma$ in a formal system is a subset of its universe. {\footnotesize\begin{quotation} {\em Comment.} The first condition in the definition of closure simply says that the hypotheses of the pre-statement are in its closure. Condition 2(a) says that a substitution exists that makes the mandatory hypotheses of an axiomatic statement exactly match some members of the closure. This is what we explicitly demonstrate in a Metamath language proof. %Conditions 2(a) and 2(b) say that a substitution exists that makes the %(mandatory) hypotheses of an axiomatic statement exactly match some members of %the closure. This is what we explicitly demonstrate with a Metamath language %proof. % %The set of expressions $F$ in condition 2(b) excludes the variable-type %hypotheses; this is done because non-mandatory variable-type hypotheses are %effectively ``dropped'' as irrelevant whereas logical hypotheses must be %retained to achieve a consistent logical system. Condition 2(b) describes how distinct-variable restrictions in the axiomatic statement must be met. It means that after a substitution for two variables that must be distinct, the resulting two expressions must either contain no variables, or if they do, they may not have variables in common, and each pair of any variables they do have, with one variable from each expression, must be specified as distinct in the original statement. \end{quotation}} {\footnotesize\begin{quotation} {\em Relationship to Metamath.} Axiomatic statements and provable statements in a formal system correspond to the frames for \texttt{\$a} and \texttt{\$p} statements respectively in a Metamath database. The set of axiomatic statements are a subset of the set of provable statements in a formal system, although in a Metamath database a \texttt{\$a} statement is distinguished by not having a proof. A Metamath language proof for a \texttt{\$p} statement tells the computer how to explicitly construct a series of members of the closure ultimately leading to a demonstration that the assertion being proved is in the closure. The actual closure typically contains an infinite number of expressions. A formal system itself does not have an explicit object called a ``proof'' but rather the existence of a proof is implied indirectly by membership of an assertion in a provable statement's closure. We do this to make the formal system easier to describe in the language of set theory. We also note that once established as provable, a statement may be considered to acquire the same status as an axiomatic statement, because if the set of axiomatic statements is extended with a provable statement, the universe of the formal system remains unchanged (provided that $\mbox{\em VR}$ is infinite). In practice, this means we can build a hierarchy of provable statements to more efficiently establish additional provable statements. This is what we do in Metamath when we allow proofs to reference previous \texttt{\$p} statements as well as previous \texttt{\$a} statements. \end{quotation}} \section{Examples of Formal Systems} {\footnotesize\begin{quotation} {\em Relationship to Metamath.} The examples in this section, except Example~2, are for the most part exact equivalents of the development in the set theory database \texttt{set.mm}. You may want to compare Examples~1, 3, and 5 to Section~\ref{metaaxioms}, Example 4 to Sections~\ref{metadefprop} and \ref{metadefpred}, and Example 6 to Section~\ref{setdefinitions}.\label{exampleref} \end{quotation}} \subsection{Example~1---Propositional Calculus}\index{propositional calculus} Classical propositional calculus can be described by the following formal system. We assume the set of variables is infinite. Rather than denoting the constants and variables by $c_0, c_1, \ldots$ and $v_0, v_1, \ldots$, for readability we will instead use more conventional symbols, with the understanding of course that they denote distinct primitive objects. Also for readability we may omit commas between successive terms of a sequence; thus $\langle \mbox{wff\ } \varphi\rangle$ denotes $\langle \mbox{wff}, \varphi\rangle$. Let \begin{itemize} \item[] $\mbox{\em CN}=\{\mbox{wff}, \vdash, \to, \lnot, (,)\}$ \item[] $\mbox{\em VR}=\{\varphi,\psi,\chi,\ldots\}$ \item[] $T = \{\langle \mbox{wff\ } \varphi\rangle, \langle \mbox{wff\ } \psi\rangle, \langle \mbox{wff\ } \chi\rangle,\ldots\}$, i.e.\ those expressions of length 2 whose first member is $\mbox{\rm wff}$ and whose second member belongs to $\mbox{\em VR}$.\footnote{For convenience we let $T$ be an infinite set; the definition of a statement permits this in principle. Since a Metamath source file has a finite size, in practice we must of course use appropriate finite subsets of this $T$, specifically ones containing at least the mandatory variable-type hypotheses. Similarly, in the source file we introduce new variables as required, with the understanding that a potentially infinite number of them are available.} \noindent Then $\Gamma$ consists of the axiomatic statements that are the reducts of following pre-statements: \begin{itemize} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\to\psi)\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }\lnot\varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash(\varphi\to(\psi\to\varphi)) \rangle\rangle$ \item[] $\langle\varnothing,T, \varnothing, \langle \vdash((\varphi\to(\psi\to\chi))\to ((\varphi\to\psi)\to(\varphi\to\chi))) \rangle\rangle$ \item[] $\langle\varnothing,T, \varnothing, \langle \vdash((\lnot\varphi\to\lnot\psi)\to (\psi\to\varphi))\rangle\rangle$ \item[] $\langle\varnothing,T, \{\langle\vdash(\varphi\to\psi)\rangle, \langle\vdash\varphi\rangle\}, \langle\vdash\psi\rangle\rangle$ \end{itemize} \end{itemize} (For example, the reduct of $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\to\psi)\rangle\rangle$ is \begin{itemize} \item[] $\langle\varnothing, \{\langle \mbox{wff\ } \varphi\rangle, \langle \mbox{wff\ } \psi\rangle\}, \varnothing, \langle \mbox{wff\ }(\varphi\to\psi)\rangle\rangle$, \end{itemize} which is the first axiomatic statement.) We call the members of $\mbox{\em VR}$ {\em wff variables} or (in the context of first-order logic which we will describe shortly) {\em wff metavariables}. Note that the symbols $\phi$, $\psi$, etc.\ denote actual specific members of $\mbox{\em VR}$; they are not metavariables of our expository language (which we denote with $\alpha$, $\beta$, etc.) but are instead (meta)constant symbols (members of $\mbox{\em SM}$) from the point of view of our expository language. The equivalent system of propositional calculus described in \cite{Tarski1965} also uses the symbols $\phi$, $\psi$, etc.\ to denote wff metavariables, but in \cite{Tarski1965} unlike here those are metavariables of the expository language and not primitive symbols of the formal system. The first two statements define wffs: if $\varphi$ and $\psi$ are wffs, so is $(\varphi \to \psi)$; if $\varphi$ is a wff, so is $\lnot\varphi$. The next three are the axioms of propositional calculus: if $\varphi$ and $\psi$ are wffs, then $\vdash (\varphi \to (\psi \to \varphi))$ is an (axiomatic) theorem; etc. The last is the rule of modus ponens: if $\varphi$ and $\psi$ are wffs, and $\vdash (\varphi\to\psi)$ and $\vdash \varphi$ are theorems, then $\vdash \psi$ is a theorem. The correspondence to ordinary propositional calculus is as follows. We consider only provable statements of the form $\langle\varnothing, T,\varnothing,A\rangle$ with $T$ defined as above. The first term of the assertion $A$ of any such statement is either ``wff'' or ``$\vdash$''. A statement for which first term is ``wff'' is a {\em wff} of propositional calculus, and one where the first term is ``$\vdash$'' is a {\em theorem (scheme)} of propositional calculus. The universe of this formal system also contains many other provable statements. Those with distinct-variable restrictions are irrelevant because propositional calculus has no constraints on substitutions. Those that have logical hypotheses we call {\em inferences}\index{inference} when the logical hypotheses are of the form $\langle\vdash\rangle\frown w$ where $w$ is a wff (with the leading constant term ``wff'' removed). Inferences (other than the modus ponens rule) are not a proper part of propositional calculus but are convenient to use when building a hierarchy of provable statements. A provable statement with a nonsense hypothesis such as $\langle \to,\vdash,\lnot\rangle$, and this same expression as its assertion, we consider irrelevant; no use can be made of it in proving theorems, since there is no way to eliminate the nonsense hypothesis. {\footnotesize\begin{quotation} {\em Comment.} Our use of parentheses in the definition of a wff illustrates how axiomatic statements should be carefully stated in a way that ties in unambiguously with the substitutions allowed by the formal system. There are many ways we could have defined wffs---for example, Polish prefix notation would have allowed us to omit parentheses entirely, at the expense of readability---but we must define them in a way that is unambiguous. For example, if we had omitted parentheses from the definition of $(\varphi\to \psi)$, the wff $\lnot\varphi\to \psi$ could be interpreted as either $\lnot(\varphi\to\psi)$ or $(\lnot\varphi\to\psi)$ and would have allowed us to prove nonsense. Note that there is no concept of operator binding precedence built into our formal system. \end{quotation}} \subsection{Example~2---Predicate Calculus with Equality}\index{predicate calculus} Here we extend Example~1 to include predicate calculus with equality, illustrating the use of distinct-variable restrictions. This system is the same as Tarski's system $\mathfrak{S}_2$ in \cite{Tarski1965} (except that the axioms of propositional calculus are different but equivalent, and a redundant axiom is omitted). We extend $\mbox{\em CN}$ with the constants $\{\mbox{var},\forall,=\}$. We extend $\mbox{\em VR}$ with an infinite set of {\em individual metavariables}\index{individual metavariable} $\{x,y,z,\ldots\}$ and denote this subset $\mbox{\em Vr}$. We also join to $\mbox{\em CN}$ a possibly infinite set $\mbox{\em Pr}$ of {\em predicates} $\{R,S,\ldots\}$. We associate with $\mbox{\em Pr}$ a function $\mbox{rnk}$ from $\mbox{\em Pr}$ to $\omega$, and for $\alpha\in \mbox{\em Pr}$ we call $\mbox{rnk}(\alpha)$ the {\em rank} of the predicate $\alpha$, which is simply the number of ``arguments'' that the predicate has. (Most applications of predicate calculus will have a finite number of predicates; for example, set theory has the single two-argument or binary predicate $\in$, which is usually written with its arguments surrounding the predicate symbol rather than with the prefix notation we will use for the general case.) As a device to facilitate our discussion, we will let $\mbox{\em Vs}$ be any fixed one-to-one function from $\omega$ to $\mbox{\em Vr}$; thus $\mbox{\em Vs}$ is any simple infinite sequence of individual metavariables with no repeating terms. In this example we will not include the function symbols that are often part of formalizations of predicate calculus. Using metalogical arguments that are beyond the scope of our discussion, it can be shown that our formalization is equivalent when functions are introduced via appropriate definitions. We extend the set $T$ defined in Example~1 with the expressions $\{\langle \mbox{var\ } x\rangle,$ $ \langle \mbox{var\ } y\rangle, \langle \mbox{var\ } z\rangle,\ldots\}$. We extend the $\Gamma$ above with the axiomatic statements that are the reducts of the following pre-statements: \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }\forall x\,\varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }x=y\rangle\rangle$ \item[] $\langle\varnothing,T, \{\langle\vdash\varphi\rangle\}, \langle\vdash\forall x\,\varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash((\forall x(\varphi\to\psi) \to(\forall x\,\varphi\to\forall x\,\psi)) \rangle\rangle$ \item[] $\langle\{\{x,\varphi\}\},T,\varnothing, \langle \vdash(\varphi\to\forall x\,\varphi) \rangle\rangle$ \item[] $\langle\{\{x,y\}\},T,\varnothing, \langle \vdash\lnot\forall x\lnot x=y \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash(x=z \to(x=y\to z=y)) \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash(y=z \to(x=y\to x=z)) \rangle\rangle$ \end{list} These are the axioms not involving predicate symbols. The first two statements extend the definition of a wff. The third is the rule of generalization. The fifth states, in effect, ``For a wff $\varphi$ and variable $x$, $\vdash(\varphi\to\forall x\,\varphi)$, provided that $x$ does not occur in $\varphi$.'' The sixth states ``For a variables $x$ and $y$, $\vdash\lnot\forall x\lnot x = y$, provided that $x$ and $y$ are distinct.'' (This proviso is not necessary but was included by Tarski to weaken the axiom and still show that the system is logically complete.) Finally, for each predicate symbol $\alpha\in \mbox{\em Pr}$, we add to $\Gamma$ the an axiomatic statement, extending the definition of wff, that is the reduct of the following pre-statement: \begin{displaymath} \langle\varnothing,T,\varnothing, \langle \mbox{wff},\alpha\rangle\ \frown \mbox{\em Vs}\restriction\mbox{rnk}(\alpha)\rangle \end{displaymath} and for each $\alpha\in \mbox{\em Pr}$ and each $n < \mbox{rnk}(\alpha)$ we add to $\Gamma$ an equality axiom that is the reduct of the following pre-statement: \begin{eqnarray*} \lefteqn{\langle\varnothing,T,\varnothing, \langle \vdash,(,\mbox{\em Vs}_n,=,\mbox{\em Vs}_{\mbox{rnk}(\alpha)},\to, (,\alpha\rangle\frown \mbox{\em Vs}\restriction\mbox{rnk}(\alpha)} \\ & & \frown \langle\to,\alpha\rangle\frown \mbox{\em Vs}\restriction n\frown \langle \mbox{\em Vs}_{\mbox{rnk}(\alpha)}\rangle \\ & & \frown \mbox{\em Vs}\restriction(\mbox{rnk}(\alpha)\setminus(n+1))\frown \langle),)\rangle\rangle \end{eqnarray*} where $\restriction$ denotes function domain restriction and $\setminus$ denotes set difference. Recall that a subscript on $\mbox{\em Vs}$ denotes one of its terms. (In the above two axiom sets commas are placed between successive terms of sequences to prevent ambiguity, and if you examine them with care you will be able to distinguish those parentheses that denote constant symbols from those of our expository language that delimit function arguments. Although it might have been better to use boldface for our primitive symbols, unfortunately boldface was not available for all characters on the \LaTeX\ system used to typeset this text.) These seemingly forbidding axioms can be understood by analogy to concatenation of substrings in a computer language. They are actually relatively simple for each specific case and will become clearer by looking at the special case of a binary predicate $\alpha = R$ where $\mbox{rnk}(R)=2$. Letting $\mbox{\em Vs}$ be the sequence $\langle x,y,z,\ldots\rangle$, the axioms we would add to $\Gamma$ for this case would be the wff extension and two equality axioms that are the reducts of the pre-statements: \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }R x y\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash(x=z \to(R x y \to R z y)) \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash(y=z \to(R x y \to R x z)) \rangle\rangle$ \end{list} Study these carefully to see how the general axioms above evaluate to them. In practice, typically only a few special cases such as this would be needed, and in any case the Metamath language will only permit us to describe a finite number of predicates, as opposed to the infinite number permitted by the formal system. (If an infinite number should be needed for some reason, we could not define the formal system directly in the Metamath language but could instead define it metalogically under set theory as we do in this appendix, and only the underlying set theory, with its single binary predicate, would be defined directly in the Metamath language.) {\footnotesize\begin{quotation} {\em Comment.} As we noted earlier, the specific variables denoted by the symbols $x,y,z,\ldots\in \mbox{\em Vr}\subseteq \mbox{\em VR}\subseteq \mbox{\em SM}$ in Example~2 are not the actual variables of ordinary predicate calculus but should be thought of as metavariables ranging over them. For example, a distinct-variable restriction would be meaningless for actual variables of ordinary predicate calculus since two different actual variables are by definition distinct. And when we talk about an arbitrary representative $\alpha\in \mbox{\em Vr}$, $\alpha$ is a metavariable (in our expository language) that ranges over metavariables (which are primitives of our formal system) each of which ranges over the actual individual variables of predicate calculus (which are never mentioned in our formal system). The constant called ``var'' above is called \texttt{set} in the \texttt{set.mm} database file, but it means the same thing. I felt that ``var'' is a more meaningful name in the context of predicate calculus, whose use is not limited to set theory. For consistency we stick with the name ``var'' throughout this Appendix, even after set theory is introduced. \end{quotation}} \subsection{Free Variables and Proper Substitution}\index{free variable} \index{proper substitution}\index{substitution!proper} In the system of Example~2, there are no primitive notions of free variable and proper substitution. Tarski \cite{Tarski1965} shows that this system is logically equivalent to the more typical textbook systems that do have these primitive notions, if we introduce these notions with appropriate definitions and metalogic. We could also define axioms for such systems directly, although the recursive definitions of free variable and proper substitution would be messy and awkward to work with. Instead, we mention two devices that can be used in practice to mimic these notions. (1) Instead of introducing special notation to express (as a logical hypothesis) ``where $x$ is not free in $\varphi$'' we can use the logical hypothesis $\vdash(\varphi\to\forall x\,\varphi)$.\label{effectivelybound}\index{effectively not free}\footnote{This is a slightly weaker requirement than ``where $x$ is not free in $\varphi$.'' If we let $\varphi$ be $x=x$, we have the theorem $(x=x\to\forall x\,x=x)$ which satisfies the hypothesis, even though $x$ is free in $x=x$ . In a case like this we say that $x$ is {\em effectively not free}\index{effectively not free} in $x=x$, since $x=x$ is logically equivalent to $\forall x\,x=x$ in which $x$ is bound.} (2) It can be shown that the wff $((x=y\to\varphi)\wedge\exists x(x=y\wedge\varphi))$ (with the usual definitions of $\wedge$ and $\exists$; see Example~4 below) is logically equivalent to ``the wff that results from proper substitution of $y$ for $x$ in $\varphi$.'' This works whether or not $x$ and $y$ are distinct. \subsection{Metalogical Completeness}\index{metalogical completeness} In the system of Example~2, the following are provable pre-statements (and their reducts are provable statements): \begin{eqnarray*} & \langle\{\{x,y\}\},T,\varnothing, \langle \vdash\lnot\forall x\lnot x=y \rangle\rangle & \\ & \langle\varnothing,T,\varnothing, \langle \vdash\lnot\forall x\lnot x=x \rangle\rangle & \end{eqnarray*} whereas the following pre-statement is not to my knowledge provable (but in any case we will pretend it's not for sake of illustration) : \begin{eqnarray*} & \langle\varnothing,T,\varnothing, \langle \vdash\lnot\forall x\lnot x=y \rangle\rangle & \end{eqnarray*} In other words, we can prove ``$\lnot\forall x\lnot x=y$ where $x$ and $y$ are distinct'' and separately prove ``$\lnot\forall x\lnot x=x$'', but we can't prove the combined general case ``$\lnot\forall x\lnot x=y$'' that has no proviso. Now this does not compromise logical completeness, because the variables are really metavariables and the two provable cases together cover all possible cases. The third case can be considered a metatheorem whose direct proof, using the system of Example~2, lies outside the capability of the formal system. Also, in the system of Example~2 the following pre-statement is not to my knowledge provable (again, a conjecture that we will pretend to be the case): \begin{eqnarray*} & \langle\varnothing,T,\varnothing, \langle \vdash(\forall x\, \varphi\to\varphi) \rangle\rangle & \end{eqnarray*} Instead, we can only prove specific cases of $\varphi$ involving individual metavariables, and by induction on formula length, prove as a metatheorem outside of our formal system the general statement above. The details of this proof are found in \cite{Kalish}. There does, however, exist a system of predicate calculus in which all such ``simple metatheorems'' as those above can be proved directly, and we present it in Example~3. A {\em simple metatheorem}\index{simple metatheorem} is any statement of the formal system of Example~2 where all distinct variable restrictions consist of either two individual metavariables or an individual metavariable and a wff metavariable, and which is provable by combining cases outside the system as above. A system is {\em metalogically complete}\index{metalogical completeness} if all of its simple metatheorems are (directly) provable statements. The precise definition of ``simple metatheorem'' and the proof of the ``metalogical completeness'' of Example~3 is found in Remark 9.6 and Theorem 9.7 of \cite{Megill}.\index{Megill, Norman} \subsection{Example~3---Metalogically Complete Predicate Calculus with Equality} For simplicity we will assume there is one binary predicate $R$; this system suffices for set theory, where the $R$ is of course the $\in$ predicate. We label the axioms as they appear in \cite{Megill}. This system is logically equivalent to that of Example~2 (when the latter is restricted to this single binary predicate) but is also metalogically complete.\index{metalogical completeness} Let \begin{itemize} \item[] $\mbox{\em CN}=\{\mbox{wff}, \mbox{var}, \vdash, \to, \lnot, (,),\forall,=,R\}$. \item[] $\mbox{\em VR}=\{\varphi,\psi,\chi,\ldots\}\cup\{x,y,z,\ldots\}$. \item[] $T = \{\langle \mbox{wff\ } \varphi\rangle, \langle \mbox{wff\ } \psi\rangle, \langle \mbox{wff\ } \chi\rangle,\ldots\}\cup \{\langle \mbox{var\ } x\rangle, \langle \mbox{var\ } y\rangle, \langle \mbox{var\ }z\rangle,\ldots\}$. \noindent Then $\Gamma$ consists of the reducts of the following pre-statements: \begin{itemize} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\to\psi)\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }\lnot\varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }\forall x\,\varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }x=y\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }Rxy\rangle\rangle$ \item[(C1$'$)] $\langle\varnothing,T,\varnothing, \langle \vdash(\varphi\to(\psi\to\varphi)) \rangle\rangle$ \item[(C2$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash((\varphi\to(\psi\to\chi))\to ((\varphi\to\psi)\to(\varphi\to\chi))) \rangle\rangle$ \item[(C3$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash((\lnot\varphi\to\lnot\psi)\to (\psi\to\varphi))\rangle\rangle$ \item[(C4$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\forall x(\forall x\,\varphi\to\psi)\to (\forall x\,\varphi\to\forall x\,\psi))\rangle\rangle$ \item[(C5$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\forall x\,\varphi\to\varphi)\rangle\rangle$ \item[(C6$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\forall x\forall y\,\varphi\to \forall y\forall x\,\varphi)\rangle\rangle$ \item[(C7$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\lnot\varphi\to\forall x\lnot\forall x\,\varphi )\rangle\rangle$ \item[(C8$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(x=y\to(x=z\to y=z))\rangle\rangle$ \item[(C9$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\lnot\forall x\, x=y\to(\lnot\forall x\, x=z\to (y=z\to\forall x\, y=z)))\rangle\rangle$ \item[(C10$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\forall x(x=y\to\forall x\,\varphi)\to \varphi))\rangle\rangle$ \item[(C11$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\forall x\, x=y\to(\forall x\,\varphi \to\forall y\,\varphi))\rangle\rangle$ \item[(C12$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(x=y\to(Rxz\to Ryz))\rangle\rangle$ \item[(C13$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(x=y\to(Rzx\to Rzy))\rangle\rangle$ \item[(C15$'$)] $\langle\varnothing,T, \varnothing, \langle \vdash(\lnot\forall x\, x=y\to(x=y\to(\varphi \to\forall x(x=y\to\varphi))))\rangle\rangle$ \item[(C16$'$)] $\langle\{\{x,y\}\},T, \varnothing, \langle \vdash(\forall x\, x=y\to(\varphi\to\forall x\,\varphi) )\rangle\rangle$ \item[(C5)] $\langle\{\{x,\varphi\}\},T,\varnothing, \langle \vdash(\varphi\to\forall x\,\varphi) \rangle\rangle$ \item[(MP)] $\langle\varnothing,T, \{\langle\vdash(\varphi\to\psi)\rangle, \langle\vdash\varphi\rangle\}, \langle\vdash\psi\rangle\rangle$ \item[(Gen)] $\langle\varnothing,T, \{\langle\vdash\varphi\rangle\}, \langle\vdash\forall x\,\varphi\rangle\rangle$ \end{itemize} \end{itemize} While it is known that these axioms are ``metalogically complete,'' it is not known whether they are independent (i.e.\ none is redundant) in the metalogical sense; specifically, whether any axiom (possibly with additional non-mandatory distinct-variable restrictions, for use with any dummy variables in its proof) is provable from the others. Note that metalogical independence is a stronger requirement than independence in the usual logical sense. Not all of the above axioms are logically independent: for example, C9$'$ can be proved as a metatheorem from the others, outside the formal system, by combining the possible cases of distinct variables. \subsection{Example~4---Adding Definitions}\index{definition} There are several ways to add definitions to a formal system. Probably the most proper way is to consider definitions not as part of the formal system at all but rather as abbreviations that are part of the expository metalogic outside the formal system. For convenience, though, we may use the formal system itself to incorporate definitions, adding them as axiomatic extensions to the system. This could be done by adding a constant representing the concept ``is defined as'' along with axioms for it. But there is a nicer way, at least in this writer's opinion, that introduces definitions as direct extensions to the language rather than as extralogical primitive notions. We introduce additional logical connectives and provide axioms for them. For systems of logic such as Examples 1 through 3, the additional axioms must be conservative in the sense that no wff of the original system that was not a theorem (when the initial term ``wff'' is replaced by ``$\vdash$'' of course) becomes a theorem of the extended system. In this example we extend Example~3 (or 2) with standard abbreviations of logic. We extend $\mbox{\em CN}$ of Example~3 with new constants $\{\leftrightarrow, \wedge,\vee,\exists\}$, corresponding to logical equivalence,\index{logical equivalence ($\leftrightarrow$)}\index{biconditional ($\leftrightarrow$)} conjunction,\index{conjunction ($\wedge$)} disjunction,\index{disjunction ($\vee$)} and the existential quantifier.\index{existential quantifier ($\exists$)} We extend $\Gamma$ with the axiomatic statements that are the reducts of the following pre-statements: \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\leftrightarrow\psi)\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\vee\psi)\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }(\varphi\wedge\psi)\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }\exists x\, \varphi\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash ( ( \varphi \leftrightarrow \psi ) \to ( \varphi \to \psi ) )\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash ((\varphi\leftrightarrow\psi)\to (\psi\to\varphi))\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash ((\varphi\to\psi)\to( (\psi\to\varphi)\to(\varphi \leftrightarrow\psi)))\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash (( \varphi \wedge \psi ) \leftrightarrow\neg ( \varphi \to \neg \psi )) \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash (( \varphi \vee \psi ) \leftrightarrow (\neg \varphi \to \psi )) \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle\vdash (\exists x \,\varphi\leftrightarrow \lnot \forall x \lnot \varphi)\rangle\rangle$ \end{list} The first three logical axioms (statements containing ``$\vdash$'') introduce and effectively define logical equivalence, ``$\leftrightarrow$''. The last three use ``$\leftrightarrow$'' to effectively mean ``is defined as.'' \subsection{Example~5---ZFC Set Theory}\index{ZFC set theory} Here we add to the system of Example~4 the axioms of Zermelo-Fraenkel set theory with Choice. For convenience we make use of the definitions in Example~4. In the $\mbox{\em CN}$ of Example~4 (which extends Example~3), we replace the symbol $R$ with the symbol $\in$. We remove from $\Gamma$ of Example~4 the three axiomatic statements containing $R$ and replace them with the reducts of the following: \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }x\in y\rangle\rangle$ \item[] $\langle\varnothing,T, \varnothing, \langle \vdash(x=y\to(x\in z\to y\in z))\rangle\rangle$ \item[] $\langle\varnothing,T, \varnothing, \langle \vdash(x=y\to(z\in x\to z\in y))\rangle\rangle$ \end{list} Letting $D=\{\{\alpha,\beta\}\in \mbox{\em DV}\,|\alpha,\beta\in \mbox{\em Vr}\}$ (in other words all individual variables must be distinct), we extend $\Gamma$ with the ZFC axioms, called \index{Axiom of Extensionality} \index{Axiom of Replacement} \index{Axiom of Union} \index{Axiom of Power Sets} \index{Axiom of Regularity} \index{Axiom of Infinity} \index{Axiom of Choice} Extensionality, Replacement, Union, Power Set, Regularity, Infinity, and Choice, that are the reducts of: \begin{list}{}{\itemsep 0.0pt} \item[Ext] $\langle D,T, \varnothing, \langle\vdash (\forall x(x\in y\leftrightarrow x \in z)\to y =z) \rangle\rangle$ \item[Rep] $\langle D,T, \varnothing, \langle\vdash\exists x ( \exists y \forall z (\varphi \to z = y ) \to \forall z ( z \in x \leftrightarrow \exists x ( x \in y \wedge \forall y\,\varphi ) ) )\rangle\rangle$ \item[Un] $\langle D,T, \varnothing, \langle\vdash \exists x \forall y ( \exists x ( y \in x \wedge x \in z ) \to y \in x ) \rangle\rangle$ \item[Pow] $\langle D,T, \varnothing, \langle\vdash \exists x \forall y ( \forall x ( x \in y \to x \in z ) \to y \in x ) \rangle\rangle$ \item[Reg] $\langle D,T, \varnothing, \langle\vdash ( x \in y \to \exists x ( x \in y \wedge \forall z ( z \in x \to \lnot z \in y ) ) ) \rangle\rangle$ \item[Inf] $\langle D,T, \varnothing, \langle\vdash \exists x(y\in x\wedge\forall y(y\in x\to \exists z(y \in z\wedge z\in x))) \rangle\rangle$ \item[AC] $\langle D,T, \varnothing, \langle\vdash \exists x \forall y \forall z ( ( y \in z \wedge z \in w ) \to \exists w \forall y ( \exists w ( ( y \in z \wedge z \in w ) \wedge ( y \in w \wedge w \in x ) ) \leftrightarrow y = w ) ) \rangle\rangle$ \end{list} \subsection{Example~6---Class Notation in Set Theory}\label{class} A powerful device that makes set theory easier (and that we have been using all along in our informal expository language) is {\em class abstraction notation}.\index{class abstraction}\index{abstraction class} The definitions we introduce are rigorously justified as conservative by Takeuti and Zaring \cite{Takeuti}\index{Takeuti, Gaisi} or Quine \cite{Quine}\index{Quine, Willard Van Orman}. The key idea is to introduce the notation $\{x|\mbox{---}\}$ which means ``the class of all $x$ such that ---'' for abstraction classes and introduce (meta)variables that range over them. An abstraction class may or may not be a set, depending on whether it exists (as a set). A class that does not exist is called a {\em proper class}.\index{proper class}\index{class!proper} To illustrate the use of abstraction classes we will provide some examples of definitions that make use of them: the empty set, class union, and unordered pair. Many other such definitions can be found in the Metamath set theory database, \texttt{set.mm}.\index{set theory database (\texttt{set.mm})} We extend $\mbox{\em CN}$ of Example~5 with new symbols $\{\mbox{class}, \{, |, \}, \varnothing, \cup, , \}$ where the inner braces and last comma are constant symbols. (As before, our dual use of some mathematical symbols for both our expository language and as primitives of the formal system should be clear from context.) We extend $\mbox{\em VR}$ of Example~5 with a set of {\em class variables}\index{class variable} $\{A,B,C,\ldots\}$. We extend the $T$ of Example~5 with $\{\langle \mbox{class\ } A\rangle, \langle \mbox{class\ }B\rangle, \langle \mbox{class\ } C\rangle,\ldots\}$. To introduce our definitions, we add to $\Gamma$ of Example~5 the axiomatic statements that are the reducts of the following pre-statements: \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{class\ }x\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{class\ }\{x|\varphi\}\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }A=B\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{wff\ }A\in B\rangle\rangle$ \item[Ab] $\langle\varnothing,T,\varnothing, \langle \vdash ( y \in \{ x |\varphi\} \leftrightarrow ( ( x = y \to\varphi) \wedge \exists x ( x = y \wedge\varphi) )) \rangle\rangle$ \item[Eq] $\langle\{\{x,A\},\{x,B\}\},T,\varnothing, \langle \vdash ( A = B \leftrightarrow \forall x ( x \in A \leftrightarrow x \in B ) ) \rangle\rangle$ \item[El] $\langle\{\{x,A\},\{x,B\}\},T,\varnothing, \langle \vdash ( A \in B \leftrightarrow \exists x ( x = A \wedge x \in B ) ) \rangle\rangle$ \end{list} Here we say that an individual variable is a class; $\{x|\varphi\}$ is a class; and we extend the definition of a wff to include class equality and membership. Axiom Ab defines membership of a variable in a class abstraction; the right-hand side can be read as ``the wff that results from proper substitution of $y$ for $x$ in $\varphi$.''\footnote{Note that this definition makes unnecessary the introduction of a separate notation similar to $\varphi(x|y)$ for proper substitution, although we may choose to do so to be conventional. Incidentally, $\varphi(x|y)$ as it stands would be ambiguous in the formal systems of our examples, since we wouldn't know whether $\lnot\varphi(x|y)$ meant $\lnot(\varphi(x|y))$ or $(\lnot\varphi)(x|y)$. Instead, we would have to use an unambiguous variant such as $(\varphi\, x|y)$.} Axioms Eq and El extend the meaning of the existing equality and membership connectives. This is potentially dangerous and requires careful justification. For example, from Eq we can derive the Axiom of Extensionality with predicate logic alone; thus in principle we should include the Axiom of Extensionality as a logical hypothesis. However we do not bother to do this since we have already presupposed that axiom earlier. The distinct variable restrictions should be read ``where $x$ does not occur in $A$ or $B$.'' We typically do this when the right-hand side of a definition involves an individual variable not in the expression being defined; it is done so that the right-hand side remains independent of the particular ``dummy'' variable we use. We continue to add to $\Gamma$ the following definitions (i.e. the reducts of the following pre-statements) for empty set,\index{empty set} class union,\index{union} and unordered pair.\index{unordered pair} They should be self-explanatory. Analogous to our use of ``$\leftrightarrow$'' to define new wffs in Example~4, we use ``$=$'' to define new abstraction terms, and both may be read informally as ``is defined as'' in this context. \begin{list}{}{\itemsep 0.0pt} \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{class\ }\varnothing\rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \vdash \varnothing = \{ x | \lnot x = x \} \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{class\ }(A\cup B)\rangle\rangle$ \item[] $\langle\{\{x,A\},\{x,B\}\},T,\varnothing, \langle \vdash ( A \cup B ) = \{ x | ( x \in A \vee x \in B ) \} \rangle\rangle$ \item[] $\langle\varnothing,T,\varnothing, \langle \mbox{class\ }\{A,B\}\rangle\rangle$ \item[] $\langle\{\{x,A\},\{x,B\}\},T,\varnothing, \langle \vdash \{ A , B \} = \{ x | ( x = A \vee x = B ) \} \rangle\rangle$ \end{list} \section{Metamath as a Formal System}\label{theorymm} This section presupposes a familiarity with the Metamath computer language. Our theory describes formal systems and their universes. The Metamath language provides a way of representing these set-theoretical objects to a computer. A Metamath database, being a finite set of {\sc ascii} characters, can usually describe only a subset of a formal system and its universe, which are typically infinite. However the database can contain as large a finite subset of the formal system and its universe as we wish. (Of course a Metamath set theory database can, in principle, indirectly describe an entire infinite formal system by formalizing the expository language in this Appendix.) For purpose of our discussion, we assume the Metamath database is in the simple form described on p.~\pageref{framelist}, consisting of all constant and variable declarations at the beginning, followed by a sequence of extended frames each delimited by \texttt{\$\char`\{} and \texttt{\$\char`\}}. Any Metamath database can be converted to this form, as described on p.~\pageref{frameconvert}. The math symbol tokens of a Metamath source file, which are declared with \texttt{\$c} and \texttt{\$v} statements, are names we assign to representatives of $\mbox{\em CN}$ and $\mbox{\em VR}$. For definiteness we could assume that the first math symbol declared as a variable corresponds to $v_0$, the second to $v_1$, etc., although the exact correspondence we choose is not important. In the Metamath language, each \texttt{\$d}, \texttt{\$f}, and \texttt{\$e} source statement in an extended frame (Section~\ref{frames}) corresponds respectively to a member of the collections $D$, $T$, and $H$ in a formal system statement $\langle D_M,T_M,H,A\rangle$. The math symbol strings following these Metamath keywords correspond to a variable pair (in the case of \texttt{\$d}) or an expression (for the other two keywords). The math symbol string following a \texttt{\$a} source statement corresponds to expression $A$ in an axiomatic statement of the formal system; the one following a \texttt{\$p} source statement corresponds to $A$ in a provable statement that is not axiomatic. In other words, each extended frame in a Metamath database corresponds to a pre-statement of the formal system, and a frame corresponds to a statement of the formal system. (Don't confuse the two meanings of ``statement'' here. A statement of the formal system corresponds to the several statements in a Metamath database that may constitute a frame.) In order for the computer to verify that a formal system statement is provable, each \texttt{\$p} source statement is accompanied by a proof. However, the proof does not correspond to anything in the formal system but is simply a way of communicating to the computer the information needed for its verification. The proof tells the computer {\em how to construct} specific members of closure of the formal system pre-statement corresponding to the extended frame of the \texttt{\$p} statement. The final result of the construction is the member of the closure that matches the \texttt{\$p} statement. The abstract formal system, on the other hand, is concerned only with the {\em existence} of members of the closure. As mentioned on p.~\pageref{exampleref}, Examples 1 and 3--6 in the previous Section parallel the development of logic and set theory in the Metamath database \texttt{set.mm}.\index{set theory database (\texttt{set.mm})} You may find it instructive to compare them. \chapter{The MIU System} \label{MIU} \index{formal system} \index{MIU-system} The following is a listing of the file \texttt{miu.mm}. It is self-explanatory. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{verbatim} $( The MIU-system: A simple formal system $) $( Note: This formal system is unusual in that it allows empty wffs. To work with a proof, you must type SET EMPTY_SUBSTITUTION ON before using the PROVE command. By default, this is OFF in order to reduce the number of ambiguous unification possibilities that have to be selected during the construction of a proof. $) $( Hofstadter's MIU-system is a simple example of a formal system that illustrates some concepts of Metamath. See Douglas R. Hofstadter, _Goedel, Escher, Bach: An Eternal Golden Braid_ (Vintage Books, New York, 1979), pp. 33ff. for a description of the MIU-system. The system has 3 constant symbols, M, I, and U. The sole axiom of the system is MI. There are 4 rules: Rule I: If you possess a string whose last letter is I, you can add on a U at the end. Rule II: Suppose you have Mx. Then you may add Mxx to your collection. Rule III: If III occurs in one of the strings in your collection, you may make a new string with U in place of III. Rule IV: If UU occurs inside one of your strings, you can drop it. Unfortunately, Rules III and IV do not have unique results: strings could have more than one occurrence of III or UU. This requires that we introduce the concept of an "MIU well-formed formula" or wff, which allows us to construct unique symbol sequences to which Rules III and IV can be applied. $) $( First, we declare the constant symbols of the language. Note that we need two symbols to distinguish the assertion that a sequence is a wff from the assertion that it is a theorem; we have arbitrarily chosen "wff" and "|-". $) $c M I U |- wff $. $( Declare constants $) $( Next, we declare some variables. $) $v x y $. $( Throughout our theory, we shall assume that these variables represent wffs. $) wx $f wff x $. wy $f wff y $. $( Define MIU-wffs. We allow the empty sequence to be a wff. $) $( The empty sequence is a wff. $) we $a wff $. $( "M" after any wff is a wff. $) wM $a wff x M $. $( "I" after any wff is a wff. $) wI $a wff x I $. $( "U" after any wff is a wff. $) wU $a wff x U $. $( Assert the axiom. $) ax $a |- M I $. $( Assert the rules. $) ${ Ia $e |- x I $. $( Given any theorem ending with "I", it remains a theorem if "U" is added after it. (We distinguish the label I_ from the math symbol I to conform to the 24-Jun-2006 Metamath spec.) $) I_ $a |- x I U $. $} ${ IIa $e |- M x $. $( Given any theorem starting with "M", it remains a theorem if the part after the "M" is added again after it. $) II $a |- M x x $. $} ${ IIIa $e |- x I I I y $. $( Given any theorem with "III" in the middle, it remains a theorem if the "III" is replaced with "U". $) III $a |- x U y $. $} ${ IVa $e |- x U U y $. $( Given any theorem with "UU" in the middle, it remains a theorem if the "UU" is deleted. $) IV $a |- x y $. $} $( Now we prove the theorem MUIIU. You may be interested in comparing this proof with that of Hofstadter (pp. 35 - 36). $) theorem1 $p |- M U I I U $= we wM wU wI we wI wU we wU wI wU we wM we wI wU we wM wI wI wI we wI wI we wI ax II II I_ III II IV $. \end{verbatim}\index{well-formed formula (wff)} The \texttt{show proof /essential/lemmon/renumber} command yields the following display. It is very similar to the one in \cite[pp.~35--36]{Hofstadter}.\index{Hofstadter, Douglas R.} \begin{verbatim} 1 ax $a |- M I 2 1 II $a |- M I I 3 2 II $a |- M I I I I 4 3 I_ $a |- M I I I I U 5 4 III $a |- M U I U 6 5 II $a |- M U I U U I U 7 6 IV $a |- M U I I U \end{verbatim} We note that Hofstadter's ``MU-puzzle,'' which asks whether MU is a theorem of the MIU-system, cannot be answered using the system above because the MU-puzzle is a question {\em about} the system. To prove the answer to the MU-puzzle, a much more elaborate system is needed, namely one that models the MIU-system within set theory. (Incidentally, the answer to the MU-puzzle is no.) % % \chapter{Disclaimer and Trademarks} % % Information in this document is subject to change without notice and does not % represent a commitment on the part of Norman Megill. % \vspace{2ex} % % \noindent Norman D. Megill makes no warranties, either express or implied, % regarding the Metamath computer software package. % % \vspace{2ex} % % \noindent Any trademarks mentioned in this book are the property of % their respective owners. The name ``Metamath'' is a trademark of % Norman Megill. % \cleardoublepage \phantomsection % fixes the link anchor \addcontentsline{toc}{chapter}{\bibname} \bibliography{metamath} %\input{metamath.bbl} \raggedright \cleardoublepage \phantomsection % fixes the link anchor \addcontentsline{toc}{chapter}{\indexname} %\printindex ?? \input{metamath.ind} \end{document}