[FOM] Harrison Advocates ZFC (Metamath)

[Norman Megill]

Since Metamath has been mentioned, I'll make some remarks on it that may 
be of interest.

Compared to other proof languages, Metamath was primarily intended as a 
way to document and verify proofs more than as a tool for creating them. 
  The existing tools are relatively primitive with little automation - 
"using the system [to create proofs] is like writing assembly code" 
(Avigad) - although Mario Carneiro and others have done impressive 
things with them.

For documenting proofs, the level of detail is such that a high school 
student with little math background can mechanically follow the proofs. 
One contributor, Andrew Salmon, started in the 10th grade, inspired by a 
link to Metamath on a gaming forum, and is now in college studying 
towards becoming a math professor.

Understandably, people with some mathematical maturity may find 
Metamath's extreme detail distracting or annoying.  That may change 
somewhat with recent work by Thierry Arnoux, announced a few days ago, 
that displays collapsible proofs with more conventional notation and by 
default shows only "important" steps: 
http://metamath.tirix.org/ftalem2.html

While Metamath's ZFC database (called set.mm) is by far the largest, 
I'll note that Metamath is not synonymous with ZFC; Metamath 
implementations of NF, HOL, Q0, and intuitionistic logic also exist.

[Regarding NF, Scott Fenton's implementation proves the standard 
"surprising" results:  the existence of the universal class, the failure 
of Cantor's theorem, the failure of AC, and the existence of an infinite 
set.  In addition, Scott conjectures that an axiom he calls Singleton, 
"forall x exists y forall z (z \in y <=> z = x)", is missing from 
Hailperin's axiomatization - I would think it would be important to 
prove or disprove that, but no takers so far...]

"Metamath" is so-called because it works exclusively with metavariables 
ranging over variables or expressions of the object language, including 
metavariables ranging over arbitrary wffs.  Metamath's ZFC 
implementation, set.mm, is 100% pure FOL+ZFC, meaning the object 
language instantiations of its schemes result in exactly and only the 
primitive language statements of FOL+ZFC (with = and \in as the only 
predicates).

On this forum I've seen mention of "tweaked" or "sugared" ZFC that 
includes some additional primitive notions beyond those in the axioms. 
To me this would seem to go against what ZFC is supposed to represent 
i.e. a system sufficient for most mathematics.  I don't understand what 
this would accomplish that can't be achieved definitionally.  The raw 
ZFC axioms may be awkward, but they are hardly ever used directly once a 
library of convenient definitions is introduced.


The complex numbers and urelements

Because complex numbers are so commonly used, as a _practical_ matter it 
is convenient to have available (i.e. construct) a set we can call "the" 
complex numbers.  This way we don't have to preface every theorem using 
them with "Let C be an arbitrary member of the class of all complex 
number systems".  (We do that for other structures such as groups, where 
we define the class Grp of all groups then prove things about an 
arbitrary member G of Grp.)

However, even though we declare a specific set as being "the" complex 
numbers, we don't want to be dependent on any particular construction. 
For example, the current construction is based on Dedekind cuts, and 
someday we may want to replace it with one based on Cauchy sequences. 
To provide this independence, the construction proves as theorems all of 
the necessary properties of a complex number system.  At that point, we 
re-state these properties as new "axioms", and all further theorems 
about complex numbers must start with these axioms.

An extension to the Metamath language (thanks primarily to David A. 
Wheeler) provides a mechanism to ensure that (1) theorems that are part 
of the construction are not referenced outside of the construction, and 
(2) the new axioms match exactly the corresponding theorems in the 
construction part.  Point (2) ensures we are doing nothing that extends 
ZFC in any way.

One consequence of this separation from their construction is that all 
complex numbers effectively become urelements.  For example, the "axiom" 
1 =/= 0 specifies a required property of 0 and 1 without saying what 0 
and 1 contain as sets.

Once we have the complex numbers, we define the natural numbers, 
integers, rationals, and reals as specific subsets of them, giving us 
the relationship N \subset Z \subset Q \subset R \subset C.  Thus we 
don't need any kind of embedding or shifting of types.  A theorem such 
as commutativity of addition that holds for complex numbers also holds 
automatically for the subsets N, Z, Q, R.  We can use the same symbol + 
without overloading because the domain of complex numbers includes N, Z, 
Q, and R.

Because of their special applications, we do develop the Von Neumann 
ordinals separately from all this, with different symbols 0o, 1o, 
2o...(symbols cannot be overloaded in Metamath).  We have a mapping from 
omega to N that we use occasionally, such for transferring finite 
recursion from ordinals to N, but we don't use it routinely.

In set.mm, 1/0 is "undefined" because the domain of the 2nd argument of 
the division operation excludes 0.  Technically, 1/0 evaluates to the 
empty set (that's what we chose for out-of-domain behavior of functions 
in general - why we chose that is another discussion), but there is 
nothing we can do with it in the context of complex numbers, whose 
members are the urelement-like objects I described.  We cannot prove 
that 1/0 is or is not a complex number, so it is effectively undefined.


On 5/30/18 3:43 AM, Harvey Friedman wrote:

 > 3. Any attempt to veer beyond tweaked ZFC (e.g., class theory)
 >
 > CREATES MORE TROUBLE THAN IT IS WORTH

I am not sure what this means.  ZFC in set.mm is extended definitionally 
with Quine's virtual class notation in the standard textbook way (e.g. 
Levy's Basic Set Theory) and does not go "beyond" ZFC in any way.  The 
translation from class notation back to the primitive language is 
unambiguous and relatively simple, involving successive mechanical 
application of 3 definitions.  Class notation provides a powerful 
mechanism to state and prove things efficiently.

Norm Megill