[FOM] Harrison Advocates ZFC (Metamath)
Norman Megill
nm at alum.mit.edu
Sat Jun 2 20:56:11 EDT 2018
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
More information about the FOM
mailing list