Email Gateway (Aug 22 2022 at 17:22): Email Gateway (Aug 22 2022 at 17:22):From: Ken Kubota <mail@kenkubota.de>
John Harrison has recently (in March 2018) proposed a return to set theory
in a presentation with the title "Let’s make set theory great again!"
available at
http://aitp-conference.org/2018/slides/JH.pdf
(mentioning the inflexibility of the type systems of HOL and Isabelle/HOL)
which I would like to comment, and use this occasion to reply to Jan Burse
concerning Q0/R0 vs. ZFC as a foundation of mathematics.
Both Russell's type theory and Zermelo's set theory were published in 1908
to solve the problem with Russell's antinomy causing inconsistency.
In order to decide which approach is appropriate, the philosophical reason
for this antinomy and the formal system's adequateness for representing
mathematics should be taken into account.
Philosophically, Russell correctly stated that self-reference is responsible
(but didn't recognize that negation is the second component for an antinomy:
the set of all sets that do NOT contain THEMSELVES).
Mathematically, Russell draw the correct conclusion and drafted a formal system
(type theory) in which the language doesn't allow one to express such constructions.
In other words, the syntactic means of the language are the key to the solution.
This means that all of mathematics can be expressed, and only those
constructions involving self-reference and negation are excluded.
Set theory (e.g., ZFC, the variant of Zermelo set theory in use today)
takes a very different approach by giving the class status by default,
and giving the set status only to those constructions often used.
Compared with the type theoretic approach this means that the set theoretic
solution is to simply forbid all reasoning first, and then to allow only certain
constructions (a positive list).
The result (ZFC) is a not systematic solution of the problem (Russell's antinomy),
but a preliminary solution based on the explored fields of mathematics at that time.
For example, ZFC is not sufficient to handle large cardinals (which require an
additional axiom), and it should be easy to construe other examples not covered
by ZFC by introducing other axioms.
This means that the (from a logical point of view) arbitrary set of axioms in ZFC
(containing both logical and non-logical axioms) can cover only parts of mathematics,
but not (all of) mathematics in general, and, furthermore, this limitation cannot
be circumvented by adding further axioms (resulting in another arbitrary set of axioms).
A systematic solution can consist only in shaping the syntactic means of the
formal language (finding the grammar of mathematics) such that they correctly
preserve dependencies and, hence, prohibit constructions involving both
self-reference and negation.
Jean van Heijenoort has described both approaches (type theory and set theory)
properly: "The two responses are extremely different; the former is a far reaching
theory of great significance for logic and even ontology, while the latter is an
immediate answer to the pressing needs of the working mathematician.”
[Heijenoort, 1967c, p. 199] - http://www.owlofminerva.net/files/fom.pdf
Note that Q0 and R0 have the five logical axioms only
https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
http://doi.org/10.4444/100.3 (pp. 353 ff.),
and non-logical axioms such as the three axioms of group theory are not
introduced as axioms, but are expressed in the form of a definition:
http://doi.org/10.4444/100.3 (p. 362).
The introduction of any further non-logical axioms (in the form of a definition)
will not cause the inconsistency of the system, but only prove the emptiness
of the set obtained by this definition (since no mathematical entity can
satisfy contradictory properties).
John Harrison correctly states that the current type systems suffer either from
inflexibilities (HOL, Isabelle/HOL) or from too complex rules (Coq) in a
presentation from March with the title "Let’s make set theory great again!"
available online at
http://aitp-conference.org/2018/slides/JH.pdf
The same critique was already expressed by Freek Wiedijk, see
section 3 of http://www.owlofminerva.net/files/fom.pdf
In a private email from January, John considered both HOL as well as
the axiomatic type classes in Isabelle as not solving the problem due to
the "lack of quantification over types in HOL".
Up to this point I fully agree, but I clearly disagree with set theory
being the solution, since it would be nothing else than a fallback
to a workaround (ZFC) based on a rather arbitrary set of axioms
involving non-logical axioms, too, and incapable of systematically
representing all of mathematics; van Heijenoort: "immediate answer
to the pressing needs of the working mathematician."
The inflexibilities mentioned above only show that the syntactic means
of the language (of current type theory, i.e., HOL and Isabelle/HOL) are
not developed enough to fully represent all of the dependencies.
But the problems mentioned by John can be easily solved with explicit
quantification over types (i.e., binding type variables with lambda),
as done in R0:
In R0, any non-empty set (hence, any non-empty subset) is
automatically considered (and introduced as) a type (cf. p. 11 of
http://www.owlofminerva.net/files/formulae.pdf ),
and instantiating general properties of a group to a specific group is actually
the main example for demonstrating the power of quantification over types
in R0, cf. pp. 12 (explanation), 362 (definition of group). The uniqueness of
the identity element (p. 421, GrpIdElUniq) is used in combination with fact
that <o, XOR> is a group (p. 422, theorem "Grp o XOR") to obtain
by substitution (without having to carry out the proof of uniqueness of the
identity element in a group again) the uniqueness of the
identity element of the specific group <o, XOR> (p. 423, XorGrpIdElUniq).
This has already been discussed in July 2017 at
https://sourceforge.net/p/hol/mailman/message/35962259/
A transfinite type theory Q was presented by Andrews in his 1965 PhD thesis
(based on his Q0 first published in 1963).
R0 avoids the stratification (the type hierarchy) of Q by its flexible handling of types,
allowing top-down definitions (similar to ZFC) rather than just the classical bottom-up
type hierarchy, since any non-empty set is a type in R0.
The key feature of R0 is internal type referencing, which preserves the
dependencies when quantifying over types (or, more exactly: binding type
variables with lambda). A quote on this is attached below.
Let me finally note that there is a minor flaw in John's presentation.
Metamath is, like Isabelle, a logical framework, and capable of coding
type theory, too. There is an implementation of Q0 in Metamath:
https://github.com/tirix/q0.mm
(For further links, see 1.1. in http://www.owlofminerva.net/files/fom.pdf )
Therefore, on pp. 6 and 7 there should be written
Simple type theory (HOL family, Isabelle/HOL, Metamath/Q0)
instead of
Simple type theory (HOL family, Isabelle/HOL)
and on p. 7 there should be written
Metamath/ZFC
Isabelle/ZF (but much less popular than Isabelle/HOL)
instead of
Metamath
Isabelle/ZF (but much less popular than Isabelle/HOL)
Ken
Ken Kubota
http://doi.org/10.4444/100
http://www.owlofminerva.net/files/tutorial.r0i.out.txt
June 2, 2018
Last updated: Apr 20 2024 at 12:26 UTC