Although some work has been done on the metamathematics of Metamath, there has not been a clear de nition of a model for a Metamath formal system. We de ne the collection of models of an arbitrary Metamath formal system, both for tree-based and string-based representations. This de nition is demonstrated with examples for propositional calculus, ZFC set theory with classes, and Hofstadter's MIU system, with applications for proving that statements are not provable, showing consistency of the main Metamath database (assuming ZFC has a model), developing new independence proofs, and proving a form of Godel's completeness theorem.
Metamath is a proof language, developed in 1992, on the principle of minimizing
the foundational logic to as little as possible [
The logic on which Metamath is based was originally de ned by Tarski in [
In this paper, we will develop a de nition for models of Metamath-style formal systems, which will operate by associating a function to each syntactical construct according to its type. For example, the forall symbol is de ned by the axiom \w 8x '", which is to say it takes as input a set variable and a w variable, and produces a w expression. This construct is associated to an interpretation function 8 : Uset Uw ! Uw , where Uset is the universe of set variables and Uw is the universe of w variables, which are each provided as part of the de nition of a model.
Note the di erence from the usual signature of the forall, 80 : (M ! Bool) ! Bool, which maps functions from the model universe M to boolean values, to a boolean value. In order to make our de nition work, we need the set Uw to be more complicated than just Bool. Instead, it is e ectively (V ! M ) ! Bool, that is, a function from assignments of variables to elements of the model, to a boolean value. In other words, a w can be thought of as an in nite-place predicate '(v0; v1; v2; : : : ) (although the value can only depend on nitely many of the provided variables). 1.1
Grammars and trees
Unfortunately, although it is possible to de ne what it means to be a model
for any Metamath formal system, we can't quite reduce it to a collection of
interpretation functions, like it is normally done, without a way to parse the
strings which are used in the proof. This leads to the idea of grammatical parsing,
which we take up in earnest in x 2.3. By separating all axioms into \syntax
axioms" and \logical axioms", we can nd an isomorphism to a representation
of statements as trees, with syntax axioms forming the nodes of the tree. Most
interesting Metamath systems are grammatical, but for example Hofstadter's
MIU system [
The main work is presented in x 2. A short recap of Metamath's formalism as it will be used in this work is in x 2.1, followed by the de nition of a model in x 2.2. Then we de ne the subset of \grammatical" formal systems, which are those for which parsing is possible, in x 2.3, and rebuild the theory for a tree representation of formal systems in x 2.4. The model theory of tree formal systems is developed in x 2.5. A selection of examples is provided in x 3, and in particular we prove that Metamath's ZFC formalization, set.mm, has a model in Theorem 4. Some applications of model theory are developed in x 4, nishing with a proof of Godel's completeness theorem in x 4.2. 2 2.1
Metamath recap
We recall the de nitions from Appendix C of the Metamath book [
A 2 EX. 11. The reduct of hD; H; Ai is hDM ; H; Ai where DM = D \ P(V(H [ fAg)), and a statement is de ned as the reduct of some pre-statement. 12. A formal system is a tuple hCN; VR; Type; i where CN; VR; Type are as above and is a set of statements. 13. The closure of a set H EX relative to D is the smallest set C such that: { H [ fVHv j v 2 VRg C { For every hD0; H0; A0i 2 and every substitution , if
For all e 2 H0 [ fVHv j v 2 VRg, (e) 2 C, and For all f ; g 2 D0, if 2 V( (VH )) and 2 V( (VH )), then f ; g 2 D, then (A0) 2 C. 14. A pre-statement hD; H; Ai is provable if A is in the closure of H relative to D, and a theorem is a statement that is the reduct of a provable pre-statement. 15. Let TC be the set of typecodes of theorems. (Explicitly, this is TC = VT [ fType(A) j hD; H; Ai 2 g.) 16. Two formal systems hCN; VR; Type; i and hCN; VR; Type; 0i are equivalent if they generate the same set of theorems (or equivalently, if every axiom in one is a theorem of the other).
Why a global type function? A careful comparison with Appendix C of the
Metamath book [
Nevertheless, it is a simple x to convert a formal system with multi-typed variables to one with a global type function: Take the set of variables to be VT VR, and de ne Type(c; v) = c. Then whenever a variable v appears in a statement with type c, use the variable hc; vi instead. This is equivalent to just prepending the type of the variable to its name, so that uses of the same variable with a di erent type are distinguished. 2.2
Models of formal systems Fix a collection of sets Uc for c 2 TC, which will represent the \universe" of objects of each typecode.
De nition 1. A valuation is a function on VR such that (v) 2 UType(v) for all v 2 VR. The set of all valuations is denoted by VL.
De nition 2. A freshness relation # is a symmetric relation on the disjoint union F U = Fc2TC Uc such that for any c 2 VT and any nite set W F U, there is a v 2 Uc with v # w for all w 2 W .
De nition 3. A model of the formal system hCN; VR; Type; i is a tuple hU; #; i where U is a function on TC and # is a freshness relation, and for each 2 VL, is a partial function on EX such that: { (Type correctness) For all e 2 EX, if (e) is de ned then { (Variable application) For all v 2 VR, (VHv) = (v). { (Axiom application) For each hD; H; Ai 2 , if ( ) # ( ) for all f ; g 2 D, and (h) is de ned for all h 2 H, then (A) is de ned. { (Substitution property) For each substitution and e 2 EX,
( )(e), where ( ) 2 VL is de ned by ( )(v) = ( (VHv)). { (Dependence on present variables) For all 2 VL, e 2 EX, If (v) = for all v 2 V(e), then (e) = (e). { (Freshness substitution) For all v 2 F U, e 2 EX, if v # (w) for all w 2 V(e), then v # (e). ( (e)) =
(v) (e) is de ned and (e) 2 UType(e).
Here equality means that one side is de ned i the other is and they have the same value. We say that e 2 EX is true in the model if (e) is de ned for all 2 VL.
The key property of a model is soundness, the fact that the axiom application law applies also to theorems.
Theorem 1. For any theorem hD; H; Ai, if ( ) # ( ) for all f ; g 2 D and (h) is de ned for all h 2 H, then (A) is de ned. Proof. By dependence on present variables, we may replace by any other 0 such that (v) = 0(v) for all v 2 V(H [ fAg) without a ecting the truth of the hypotheses or conclusion. If hD; H; Ai is the reduct of hD0; H; Ai where D0 refers to nitely many additional variables (i.e. D0 P(V ) for some nite set V V(H [ fAg)), order these as V = fv1; : : : ; vng with V(H [ fAg) = fv1; : : : ; vkg for some k n. Then use the freshness constraint to recursively select values 0(vi) for each k < i n such that 0(vi) # 0(vj ) for all j < i. Then this new 0 will satisfy the hypothesis 0( ) # 0( ) for all f ; g 2 D0, so that it su ces to prove the theorem for provable pre-statements.
We prove by induction that whenever A is in the closure of H relative to D, (A) is de ned. If A 2 H, it is true by assumption, and if A = VHv for some v 2 VR, then it is true by the variable application law. Otherwise we are given hD0; H0; A0i 2 and a substitution , such that for all e 2 H0 [ fVHv j v 2 VRg, ( (e)) is de ned (by the induction hypothesis), and for all f ; g 2 D0, if 2 V( (VH )) and 2 V( (VH )), then f ; g 2 D, and we wish to show that (A), with A = (A0), is de ned.
For each 2 V( (VH )) and 2 V( (VH )), f ; g 2 D implies ( ) # ( ) from the theorem hypothesis, hence by freshness substitution on the left and the right, ( ) # ( (VH )), and then ( (VH )) # ( (VH )), or equivalently, ( )( ) # ( )( ) for each f ; g 2 D0.
Apply the axiom application law to ( ) and hD0; H0; A0i. The substitution property reduces ( (e)) to ( )(e) in the hypotheses, and ( )(A0) to ( (A0)) in the conclusion, hence ( (A0)) is de ned, as we wished to show. tu
In particular, if h;; ;; Ai is provable, then (A) is de ned for all 2 VL, which makes it a useful technique for showing that certain strings are not provable (see x 4.1).
For any formal system, there is a model, where Uc = f g for each c, # is true, and (e) = for all ; e. Thus statements like \formal system X has a model" are not as useful here as they are in rst-order logic. To marginalize this kind of model, we will call a model where each is a total function trivial. (We will have a slightly wider de nition of trivial model given grammatical information, cf. De nition 6.)
Although this de nes the property of being a model under the full generality of Metamath formal systems, the process simpli es considerably when expressions can be parsed according to a grammar. 2.3
Grammatical parsing De nition 4. A formal system is said to be weakly grammatical if for every hD; H; Ai 2 , if Type(A) 2 VT, then there is some axiom h;; ;; A0i 2 such that (A0) = A for some substitution and no variable occurs more than once in A0.
For these systems we will de ne SA = fA j h;; ;; Ai 2
^ Type(A) 2 VT ^ 8mn; (Am = An 2 VR ! m = n)g; the set of syntax axioms. (We will identify the expression A with its statement h;; ;; Ai when discussing syntax axioms.)
For example, any context-free grammar is a weakly grammatical formal system, where each production translates to a syntax axiom, and each nonterminal translates to a variable typecode. Most recursive de nitions of a well-formed formula will t this bill, although we can't capture the notion of bound variables with this alone.
Conversely, a weakly grammatical formal system yields a context-free grammar, where the terminals are CN n VT, the non-terminals are VT, and for each A 2 SA there is a production Type(A) ! , where n = An+1 2 CN if An+1 2 CN or n = Type(An+1) 2 VT if An+1 2 VR. (This assumes that An+1 2 VT is always false, but the two sets can be disjointi ed if this is not the case.) De nition 5. A grammatical formal system is a weakly grammatical formal system augmented with a function Syn : TC ! VT such that Syn(c) = c for all c 2 VT and, de ning Syn(e) for e 2 EX such that Syn(e)0 = Syn(e0) and Syn(e)n = en for n > 0, h;; ;; Syn(e)i is a provable statement for all hD; H; Ai 2 and e 2 H [ fAg.
Remark 1. Of course, this notion is of interest primarily because it is satis ed by all major Metamath databases; in particular, set.mm is a grammatical formal system, with VT = fset; class; w g, TC = VT [ f`g, and Syn(`) = w . De nition 6. A model of a grammatical formal system is a model in the sense of De nition 3 which additionally satis es Uc USyn(c), v # wc $ v # wSyn(c) when w 2 Uc (and wc, wSyn(c) are its copies in the disjoint union), and (e) = (Syn(e)) if the latter is in Uc, otherwise unde ned. Such a model is trivial if Uc = USyn(c) for all c 2 TC. 2.4
Tree representation of formal systems The inductive de nition of the closure of a set of statements immediately leads to a tree representation of proofs. A proof tree is a tree with nodes labeled by statements and edges labeled by expressions.
De nition 7. We inductively de ne the statement \T is a proof tree for A" (relative to D; H) as follows: { For each e 2 H [ fVHv j v 2 VRg, the single-node tree labeled by the reduct of hD; H; ei is a proof tree for e. { For every hD0; H0; A0i 2 and every substitution satisfying the conditions for (A0) 2 C in x 2.1.13, the tree labeled by hD0; H0; A0i with edges for each e 2 H0 [ V(H [ fAg) leading to a proof tree for (e), is a proof tree for (A0).
The de nition of closure ensures that there is a proof tree for A relative to D; H i hD; H; Ai is provable pre-statement. (The branches for variables outside V(H [ fAg) are discarded because they can always be replaced by the trivial substitution (hvi) = hvi without a ecting the closure deduction.) Additionally, we can prove by induction that every proof tree T encodes a unique expression Expr(T ).
De nition 8. An unambiguous formal system is a grammatical formal system whose associated context-free grammar is unambiguous.
Remark 2. Note that for this to make sense we need SA to contain only axioms and not theorems, i.e. this property is not preserved by equivalence of formal systems. For such systems every Expr is an injection when restricted to the set ST of syntax trees, trees T relative to ;; ; such that Type(T ) := Type(Expr(T )) 2 VT (or equivalently, Type(T ) = Type(A) 2 VT where hD; H; Ai is the root of T ). The subtrees of a syntax tree are also syntax trees, and the nodes are syntax axioms, with variables (of the form VHv) at the leaves.
With this, we can \rebuild" the whole theory using trees instead of strings, because the all valid substitutions have unique proof tree representations. The expressions in this new language will be trees, whose nodes are syntax axioms such as wa = \w (' ^ )", representing the \and" function, with variables at the leaves. However, we no longer need to know that wa has any structure of its own, besides the fact that it takes two w variables and produces a w . Thus we can discard the set CN entirely. (That is, the constant \(" has no meaning of its own here.)
Instead, we take as inputs to the construction the set TC0 of typecodes, a set VR0 of variables, a set SA0 of things we call syntax axioms, although they have no internal structure, the function Type0 : VR0 [ SA0 ! VT0, as well as Syn0 : TC0 ! VT0. A tree T 2 ST0 is either a variable from VR0 or a syntax axiom a 2 SA0 connecting to more subtrees; each syntax axiom has a set via of variables labeling the edges, and a type Type0(a); Type0(T ) is de ned as the type of the root of T .
We replace EX in the string representation with EX0, which consists of tuples hc; T i where c 2 TC0, T 2 ST0, and Syn0(c) = Type0(T ). We extend Type0 to EX0 by Type0(hc; T i) = c. V0(T ) is de ned by induction such that V0(v) = fvg and V0(T ) at a syntax axiom is the union of V0(Ti) over the child subtrees Ti. A substitution is a function ST0 ! ST0 such that (a[T1; : : : ; Tn]) = a[ (T1); : : : ; (Tn)] for each syntax axiom a, with the value at variables left undetermined, extended to EX0 ! EX0 by (hc; T i) = hc; (T )i.
Pre-statements and statements are de ned exactly as before: A pre-statement is a tuple hD; H; Ai where D DV0, H EX0 is nite, and A 2 EX0. The reduct of hD; H; Ai is hDM ; H; Ai where DM = D \ P(V0(H [ fAg)). A tree formal system (this time unambiguous by de nition) is a tuple hTC0; VR0; SA0; Type0; Syn0; 0i where 0 is a set of statements. The closure of a set H EX0 relative to D is de ned as in the string case, but the base case instead takes H C and hType0(T ); T i 2 C for every T 2 ST0.
To map an unambiguous formal system hCN; VR; Type; ; Syni to a tree formal system hTC0; VR0; SA0; Type0; Syn0; 0i, one takes TC0 = TC, VR0 to be the set of VHv singleton trees for v 2 VR, SA0 = SA, Type0(T ) = Type(T ), Syn0 = Syn, and 0 = fhD; ft(h) j h 2 Hg; t(A)i j hD; H; Ai 2 n STg, where t(e) = fType(e); Expr 1(Syn(e))g.
These two formal systems are isomorphic, in the sense that expressions and statements can be mapped freely, respecting the de nitions of theorems and axioms, variables and typecodes. 2.5
Models of tree formal systems Given the isomorphism of the previous section, the model theory of unambiguous formal systems can be mapped to models of tree formal systems, with hU; #; i satisfying an exactly equivalent set of properties. But the major advantage of the tree formulation is that the substitution property implies that is completely determined except at syntax axioms, so for trees we will replace with a new function .
De nition 9. Given a function U on TC0 satisfying Uc USyn(c), and a SAindexed family of functions, where a : Qi UType(via) ! UType(a) for each a 2 SA, de ne for 2 VL recursively such that: { For all v 2 VR, (v) = (v). { For each T 2 ST with a 2 SA at the root, { For e = hc; T i 2 EX0, (e) = (T ) if (T ) = a(f (Ti)gi) (T ) 2 Uc, otherwise unde ned.
De nition 10. A model of a tree formal system is a tuple hU; #; i where U is a function on TC0 satisfying Uc USyn(c), and # is a freshness relation (which is extended from Fv2VT Uc to Fv2TC Uc by setting v # wc i v # wSyn(c) for the copies of w in the disjoint union), and is a SA-indexed family of functions, where a : Qi UType(via) ! UType(a) for each a 2 SA, such that for each 2 VL, and de ning as above: { For each hD; H; Ai 2 0, if ( ) # ( ) for all f ; g 2 D, and (h) is de ned for all h 2 H, then (A) is de ned. { For all v 2 F U, a 2 SA, and f 2 v # a(f ).
Qi UType(via), if v # fi for all i, then Theorem 2. Let hU; #; i be a model for the tree formal system. Then the associated hU; #; i is a model in the sense of De nition 6.
Proof.
{ The variable application law is true by de nition of , and the axiom application law is true by assumption. { For the substitution law, suppose and e 2 EX0 are given. We want to show that ( (e)) = ( )(e), where ( ) 2 VL is de ned by ( )(v) = ( (v)). We show this for Syn(e) = hType(T ); T i by induction on T . In the base case, T = v for v 2 VT, so ( )(v) = ( )(v) = ( (v)). Otherwise let a 2 SA be the root of T , so ( )(T ) = a(f ( )(Ti)gi) = a(f ( (Ti))gi) = ( (T )): Then for e = hc; T i, if ( )(T ) = ( (T )) is in Uc, then both are de ned and equal, otherwise both are unde ned. { Dependence on present variables is also provable by induction; in the base case (v) = (v) only depends on V(v) = fvg; and for a tree with a 2 SA at the root, (T ) = a(f (Ti)gi) only depends on V(T ) = Si V(Ti). For e = hc; T i this property is maintained since V(e) = V(T ) and (e) = (T ) or unde ned. { For the freshness substitution law, in the base case v # (v) = (v); and for a tree with a 2 SA at the root, if v # V(T ) then v # V(Ti) so v # (Ti) for each i, and then by de nition v # a(f (Ti)gi) = (T ). For e = hc; T i this property is maintained since V(e) = V(T ) and (e) = (T ) or unde ned. tu
By the isomorphism this approach also transfers to models of unambiguous formal systems. So we are left with the conclusion that a model can be speci ed by its functions a, for each a 2 SA; this is known in conventional model theory as the interpretation function. 3 3.1
Propositional logic We start with a model for classical propositional logic. We de ne: CN = f(; ); !; :; w ; `g
VR = f'; ; ; : : : g = fwn; wi; ax-1; ax-2; ax-3; ax-mpg; where the axioms are { wn: w :' { wi: w (' ! ) { ax-1: ` (' ! ( ! ')) { ax-2: ` ((' ! ( ! )) ! ((' ! { ax-3: ` ((:' ! : ) ! ( ! ')) { ax-mp: f` '; ` (' ! )g implies ` ) ! (' ! )))
Additionally, TC = fw ; `g and VT = fw g are implied by the preceding de nition.
Although the axiom strings appear structured with in x notation, this is not required; we could just as easily have an axiom with string ` )'( !. That this is not the case is what makes this a grammatical formal system, with Syn(w ) = Syn(`) = w . The syntax axioms are SA = fwn; wig. In fact this formal system is unambiguous, but we will not prove this here.
This formal system has a nontrivial model:
Uw = Bool := fT; Fg
U` = fTg x # y is always true :(F) = T; !(F; F) = T; !(F; T) = T; :(T) = F !(T; F) = F; !(T; T) = T
We will write \ = T" simply as \ is true" or \ ", treating the elements of Bool as actual truth values in the metalogic. The a functions generate as previously described, so that, for example, if (') = T, ( ) = F, then (w (:' ! (' ! ))) = !( :(T); !(T; F)) = !(F; F) = T.
In order to verify that this indeed yields a model, we must check the axiom application law for each non-syntax axiom (usually called \logical axioms" in this context). By our de nition of given , (hc; T i) is de ned i (hSyn(c); T i) 2 USyn(c) (where Syn(c) = Type(T )); in this case this translates to (T ) = T since Syn(c) = f`g.
{ ax-1: (` (' ! ( ! '))) = !( '; !( ; ')) = T { ax-2: !( !( '; !( ; )); !( !( '; ); !( '; { ax-3: !( !( :( '); :( )); !( ; ')) = T { ax-mp: If ' and !( '; ) are true, then = T. ))) = T
In each case, there are a nite number of variables that range over fT; Fg (such as '; ; in the case of ax-3), so it su ces to verify that they are true under all combinations of assignments to the variables, i.e. truth table veri cation. 3.2
MIU system
Let us solve the MU puzzle by using a model. Hofstadter's MIU system [
The syntax axioms are fwe; wM; wI; wUg. Note that in we, there are no symbols after the typecode, so this says that the empty string is a valid w . This formal system is weakly grammatical, but not grammatical, because w s are built from the right, while axiom II contains the string ` Mx, which cannot be parsed as a w . If there was a syntax axiom \w xy", then it would be grammatical, but not unambiguous.
In order to solve the MU puzzle, we build the relevant invariant, which is the number of I's modulo 3, into the model. Let Uw = f0; 1; 2g, U` = f1; 2g, let x # y be always true, and de ne (w e) to be Pi f (ei) mod 3, where f (v) = (v) if v is a variable, f (I) = 1, and f (c) = 0 for other constants. Let (` e) = (w e) when (w e) 2 f1; 2g.
Verifying that this yields a model is then equivalent to verifying that the axioms preserve the invariant, and we can deduce that MU is not provable because (` MU) is not de ned for any . 3.3
Set theory Of course, the more interesting case is the veri cation that the full structure of set.mm has a nontrivial model. As the background, we need a model of ZFC set theory; let this be hM; "i.
The typecodes are TC = fset; class; w ; `g, with the only non-variable typecode being ` and Syn(`) = w . With these de nitions set.mm becomes an unambiguous formal system. (Again, the proof of unambiguity is complex and not undertaken here.) Let V =: Uset be any in nite set. This is the set of variables of the \object language" over which Metamath is understood to sit; they are customarily labeled V = fv0; v1; v2; : : : g. Note that these are not actually variables in our sense, they are constants, elements of the set V . Set variables such as x in Metamath range over elements of V .
We will need a few preliminary sets before properly de ning Uw and Uclass. Take U0w = (V ! M ) ! Bool, that is, the set of functions from V ! M to Bool. The subset of Uw corresponding to true formulas, U`, is the singleton f f Tg (i.e. the constant function true). Similarly, U0class = (V ! M ) ! P(M ). De nition 11. Given A : (V ! M ) ! B (A is a w or class variable) and W V , we say A is constant outside W if for all f; g : V ! M , if f (v) = g(v) for all v 2 W , then A(f ) = A(g).
We de ne a relation # on the disjoint union V t U0w t U0class: { If x; y 2 V , then de ne x # y i x 6= y. { If x 2 V and A 2 U0class t U0w , then de ne x # A if A is constant outside
V n fxg. { The case A # x when x 2 V and A 2 Uclass t Uw is covered by symmetry; x # y is true for any other combination.
To de ne the real set Uw , we take the set of A 2 U0w such that A is \e ectively nite-dimensional", that is, A is constant outside some nite V 0 V . Similarly, Uclass is the set of e ectively nite-dimensional A 2 U0class. There is a minimal set V 0 outside which A is constant; this set is called Free(A). It immediately follows from the de nition that A # x for x 2= Free(A). We can extend the de nition slightly to set variables by taking Free(x) = fxg when x 2 V .
Theorem 3. # as de ned above is a freshness relation.
Proof. Clearly # is a symmetric relation, so we need only verify that for every c 2 fset; w ; classg and every nite set W VR, there is a v 2 Uc with v # W . If c = w then take v = f T, and if c = class then take v = f M ; in each case v # w for any w 2 F U, so the condition is satis ed.
If c = set, then for each w 2 Uc the set Free(w) is nite, as is the union Sw2W Free(w). Since V is in nite by assumption, choose some v 2 V n Sw2W Free(w); then for w 2 W , v 2= Free(w) implies v # w. tu De nition 12. For f : V ! M , x 2 V and m 2 M , the function f [x ! m] : V ! M is de ned by f [x ! m](y) = f (y) for y 6= x and f [x ! m](x) = m.
Finally, we de ne the a functions. By de nitional elimination, we can ignore de nitional syntax axioms without loss of generality.
{ Take :(f ) = f :0, where :0 is the function called : in x 3.1, and similarly for !(f ) = f !0. { 8(x; ') is the w corresponding to 8x; ' and is de ned so that 8(x; ')(f ) i '(f [x ! m]) for all m 2 M . (Since it comes up often, the restricted quanti er 8m 2 M will be abbreviated 8M m.) { The class abstraction, cab: class fx j 'g, is de ned so that cab(x; ')(f ) = fm 2 M j '(f [x ! m])g. { The set-to-class type conversion is a syntax axiom called cv: class x. The function for this is de ned so that cv(x)(f ) = fm 2 M j m " f (x)g. { Equality of classes is de ned by wceq: w A = B, and is de ned so that =(A; B)(f ) is true i A(f ) = B(f ). { We de ne 2(A; B)(f ) true if 9M m(A(f ) = fn 2 M j n " mg ^ m 2 B(f )).
For the common case where one or both of the arguments to =; 2 are sets, we note that 2( cv(x); A)(f ) i f (x) 2 A(f ), 2( cv(x); cv(y))(f ) i f (x) " f (y), and =( cv(x); cv(y))(f ) i f (x) = f (y). We need hM; "i to satisfy the extensionality axiom for this to work.
Lemma 1 (The deduction theorem). plies (f ). !('; )(f ) if and only if '(f ) imProof. Suppose not. Then !('; )(f ) = F, which by de nition implies '(f ) = T and (f ) = F, a contradiction. The converse is just ax-mp (veri ed by truth tables). tu Lemma 2 (The non-free predicate). x # ' i !('; 8(x; '))(f ) is true for all f (which is also equivalent to (` ('0 ! 8x0'0)) being de ned, where ('0) = ' and (x0) = x).
Proof. By de nition, x # ' i for all f; g : V ! M , f (v) = g(v) for all v 6= x implies '(f ) = '(g). In this case, given f , and using the deduction theorem, if '(f ), then since f [x ! m] di ers from f only at x, '(f [x ! m]) = '(f ) is true for each m, so 8(x; ')(f ). Thus !('; 8(x; '))(f ) by Lemma 1. Conversely, if f; g di er only for v = x, either '(f ) = '(g) = F, or one of them (say '(f )) is true. Then by ax-mp, 8(x; ')(f ), so taking m = g(x), '(f [x ! g(x)]) = '(g) is true. Hence '(f ) = '(g), so x # '. tu Theorem 4. The tuple hU; #; i de ned via the above construction is a model for the set.mm formal system.
Proof. As in the baby example for propositional calculus, we must verify that honors all the logical axioms. The tricky ones are the predicate calculus axioms: { ax-1,ax-2,ax-3,ax-mp: Veri cation by truth tables, as in the propositional calculus example { ax-5: ` (8x(' ! ) ! (8x' ! 8x ))
Assume 8(x; !('; ))(f ) and 8(x; ')(f ); then '(f [x ! m]) and !('; )(f [x ! m]), so by ax-mp, (f [x ! m]). Conclude by Lemma 1. { ax-6: ` (:8x' ! 8x:8x')
By Lemma 2, this is equivalent to x # :( 8(x; ')). If f; g di er only at x, then 8(x; ')(f ) if '(f [x ! m]) for all m; but f [x ! m] = g[x ! m], so 8(x; ')(f ) = 8(x; ')(g) and :( 8(x; ')(f )) = :( 8(x; ')(g)). { ax-7: ` (8x8y' ! 8y8x')
By Lemma 1, assume 8(x; 8(y; '))(f ). If x = y then this is the same as 8(y; 8(x; '))(f ), otherwise it reduces to '(f [x ! m][y ! n]) for all m; n 2 M , and note that f [x ! m][y ! n] = f [y ! n][x ! m]. { ax-gen: ` ' implies ` 8x'
If '(f ) for all f , then set f := g[x ! m] to deduce '(g[x ! m]) for all m, hence 8(x; ')(g). { ax-8: ` (x = y ! (x = z ! y = z))
By Lemma 1, assume =(x; y) and =(y; z). Then f (x) = f (y) = f (z), so =(x; z). { ax-9: ` :8x:x = y
This is equivalent to 9m 2 M , =(x; y)(f [x ! m]), or 9m 2 M; m = f [x ! m](y). If x = y, then any m 2 M will do (M is assumed nonempty because it is a model of ZFC), and if x 6= y then take m = f (y). { ax-11: ` (x = y ! (8y' ! 8x(x = y ! ')))
Assume f (x) = f (y) and 8M n; '(f [y ! n]), take some m 2 M , and assume f [x ! m](x) = f [x ! m](y). We want to show '(f [x ! m]). If x = y, then the second hypothesis implies '(f [y ! m]) = '(f [x ! m]). Otherwise, m = f (y) = f (x), so '(f [x ! m]) = '(f ) = '(f [y ! m]). { ax-12: ` (:x = y ! (y = z ! 8x y = z))
Assume f (x) 6= f (y) = f (z), and take m 2 M . We want to show f [x ! m](y) = f [x ! m](z). If x = y or x = z then f (x) = f (y) or f (x) = f (z), a contradiction, so f [x ! m](y) = f (y) = f (z) = f [x ! m](z). { ax-13: ` (x = y ! (x 2 z ! y 2 z))
Assume f (x) = f (y) and f (x) " f (z); then f (y) " f (z). { ax-14: ` (x = y ! (z 2 x ! z 2 y))
Assume f (x) = f (y) and f (z) " f (x); then f (z) " f (y). { ax-17: x; ' distinct implies ` (' ! 8x ')
This is just the forward direction of Lemma 2.
We can also verify the class axioms: { df-clab: The left hand expression x 2 fy j 'g expands to f (x) 2 fm 2 M j '(f [y ! m])g, that is, '(f [y ! f (x)]), while the right side says f (y) = f (x) ! '(f ) and 9M m; (f [y ! m](x) = m ^ '(f [y ! m])). If x = y, the left conjunct becomes '(f ) and the right becomes 9M m; '(f [x ! m]), which is provable from the other conjunct by setting m = f (x) so that f [x ! m] = f . At the same time the left expression also reduces to '(f [x ! f (x)]) = '(f ). If x 6= y, then f [y ! m](x) = f (x) and the right conjunct becomes '(f [y ! f (x)]), and the left conjunct is provable from this since f (y) = f (x) implies f [y ! f (x)] = f [y ! f (y)] = f , so both sides are equivalent to '(f [y ! f (x)]). { df-clel: We want to show that 2(A; B)(f ) i there is an m such that fn j n " mg = A(f [x ! m]) and m 2 B(f [x ! m]), which matches our de nition after replacing A(f [x ! m]) = A(f ) and B(f [x ! m]) = B(f ), since x # A and x # B. { df-cleq: (This has an extra hypothesis ax-ext which is already built into our model.) We want to show that =(A; B)(f ) i for all m, m 2 A(f [x ! m]) $ m 2 B(f [x ! m]). We are also assuming x # A and x # B in this axiom, so this reduces to m 2 A(f ) $ m 2 B(f ), or (using extensionality in the metalanguage) A(f ) = B(f ), which is the de nition of =(A; B)(f ).
The \true" axioms of set theory are all phrased in terms of only =; 2, and so factor straight through to axioms in hM; "i: { ax-ext (Axiom of Extensionality): The original expression is
!( 8(z; wb( 2(z; x); 2(z; y))); =(x; y))(f ); which simpli es, according to the de nitions, to 8M m(m"f (x) $ m"f (y)) ! f (x) = f (y), for all f . With a change of variables this is equivalent to 8M x8M y8M z(z " x $ z " y) ! x = y; exactly the same as the original universally quanti ed Metamath formula, but with " in place of 2 and 8M instead of 8. Since the other axiom expressions are long and the process is similar, I will only quote the nal equivalent form after reduction. { ax-pow (Axiom of Power sets): Equivalent to:
8M x9M y8M z(8M w(w " z ! w " x) ! z " y) { ax-un (Axiom of Union): Equivalent to: { ax-reg (Axiom of Regularity): Equivalent to:
8M x9M y8M z(9M w(z " w ^ w " x) ! z " y) { ax-inf (Axiom of In nity): Equivalent to: { ax-ac (Axiom of Choice): Equivalent to: 8M x9M y8M z8M w((z " w ^ w " x) ! 8M x(9M y; y " x ! 9M y(y " x ^ 8M z(z " y ! :z " x))) 8M x9M y(x " y ^ 8M z(z " y ! 9M w(z " w ^ w " y)))
9M v8M u(9M t(u " w ^ w " t ^ u " t ^ t " y) $ u = v)) { ax-rep: This one is more complicated than the others because it contains a w metavariable. It is equivalent to: for all binary relations ' M 2: 8M w9M y8M z('(w; z) ! z = y) ! 9M y8M z(z " y $ 9M w(w " x ^ '(w; z))): To show the Metamath form of the axiom from this one, given '0 2 Uw and f : V ! M , de ne '(w; z) $ 8M t; '0(f [w0 ! w][y0 ! t][z0 ! z]), and apply the stated form of the axiom. tu
Thus if ZFC has a model, so does set.mm. 4
4.1 Independence proofs We conclude with a few applications of the \model" concept. The primary application of a model is for showing that statements are not provable, because any provable statement must be true in the model. (The converse is not usually true.) This extends to showing that a system is consistent, because any nontrivial model has unprovable statements (and in a logic containing the principle of explosion ` (' ! (:' ! )), this implies that there is no provable statement whose negation is also provable). But it can also be applied for independence proofs, by constructing a (necessarily nonstandard) model of all statements except the target statement.
For an easy example, if we change the de nition of our model of propositional calculus so that instead :(T) = :(F) = T, we would have a new model that still satis es ax-1, ax-2, and ax-mp (because they do not involve :), but violates ax-3. If we take ' = F and = T, we get (w ((:' ! : ) ! ( ! ))) = !( !( :( '); :( )); !(
; ')) = !( !(T; T); = !(T; F) = F; !(T; F)) so (` ((:' ! : ) ! ( ! ))) is not de ned. Thus this shows that ax-3 is not provable from ax-1, ax-2, ax-mp and the syntax axioms alone (although this should not come as a surprise since none of the other axioms use the : symbol). One important construction that can be done for any arbitrary (string-based) model is to use a formal system as a model of itself. This model will have the property that the theorems (with no hypotheses) are the only statements that are true in the model, leading to an analogue of Godel's completeness theorem for statements with no hypotheses and all variables distinct. It is also the \original" model of Metamath, from which the terminology \disjoint variable condition" and the \meta" in Metamath are derived.
Given a formal system hCN; VR; Type; i, choose some set VR0, with types for each variable, such that fv 2 VR0 j Type(v) = cg is in nite for each c 2 VT. (It is possible to use VR0 = VR here, provided that VR satis es this condition, but it is also helpful to distinguish the two \levels" of variable in the contruction.) Using CN0 = CN, de ne EX0 analogously with the new sets. We will call formulas in EX0 the \object level" and those in EX the \meta level".
We also de ne a substitution : EX ! EX0 in the same way as x 2.1.8. Here variables of the meta level are substituted with expressions in the object level.
We can build another formal system at the object level, where hD0; H0; A0i 2 0 if there is some hD; H; Ai 2 and a substitution : EX ! EX0 such that 8v 2 VR; (v) 2 VR0 ( substitutes variables for variables) and (v) 6= (w) for each fv; wg 2 D, and D0 = DV0 (all variables are distinct), H0 = (H) and A0 = (A). This new formal system di ers from the original one only in having a di erent set of variables.
Theorem 5. Let A 2 Uc if there is some theorem hD; ;; Ai in the object level formal system with Type(A) = c, de ne e # e0 when V(e) \ V(e0) = ;, and let be the unique substitution EX ! EX0 satisfying (VHv) = (v), restricted to the e such that (e) 2 UType(e). Then hU; #; i is a model for the meta level formal system hCN; VR; Type; i. { The type correctness and variable application laws are true by de nition, and substitution and dependence on present variables are a consequence of properties of substitutions. { The relation # is a freshness relation because the nite set Se2W V(e) misses some variable in each type. { The freshness substitution rule says that if V(w) \ V( (w)) = ; for all w 2 V(e), then V(w)\V( (e)) = ;, which follows from V( (e)) Sw2V(e) V( (w)) which is a basic property of variables in a substitution. { The axiom application law translates directly to the induction step of closure in x 2.1.13 for the object level formal system.
Corollary 1 (Godel's completeness theorem). A statement hDV; ;; Ai of a formal system is a theorem i it is true in every model.
Proof. The forward direction is trivial by the de nition of a model. For the converse, a statement true in the model of Theorem 5, with VR0 VR extended to contain in nitely many variables of each type, is derivable by de nition. Acknowledgments. The author wishes to thank Norman Megill and the anonymous reviewers for pointing out some minor and major omissions in early drafts of this work.