[Hol-info] Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC) – Re: [Metamath] [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[Ken K. <ma...@ke...>]

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.


1. Type Theory vs. Set Theory (Reply to Jan Burse)

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).


2. Type Theory vs. Set Theory (Reply to John Harrison)

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:

1. John: "For example, if you prove something generic about groups over a type,
you may not be able to instantiate it later to a group over a subset of a type." (p. 21)

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).

2. John: "Thinking of F as a base type, we have jumped up a couple of levels
in the type hierarcy just to adjoin one root.
If we want to construct the algebraic closure of a field we have to do
this transfinitely ..." (p. 24)

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



## Internal type referencing
## Note that the universal quantifier has type '{{o,{o,\3{^}}},^}', or written
## without brackets, type 'o(o\3)^':
## Command:    A

# wff      29 :  [\t.[\p.((=_[\x.T])_p)]]                   :=  A
# w typd   29 :  [\t{^}{^}.[\p{{o,t{^}}}{{o,t{^}}}.((={{{o,{o,t{^}}},{o,t{^}}}}_[\x{t{^}}{t{^}}.T{o}]{{o,t{^}}}){{o,{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){o}]{{o,{o,t{^}}}}]
#                                                { {{o,{o,\3{^}}},^} }
#                                                           :=  A

## The specification '\3' is a reference within the type, pointing to the type
## '^' of the first argument within 'o(o\3)^', thus handling dependencies of
## types within the formula structure similar to de Bruijn indices. For
## example, the application of 'ALL' of type 'o(o\3)^' to '@' of type '^'
## would result in the wff 'ALL @' of type 'o(o@)'.
## Similarly, 'ALL NAT' would have type 'o(o NAT)'.

http://www.owlofminerva.net/files/tutorial.r0i.out.txt
June 2, 2018



> Am 04.05.2018 um 03:43 schrieb Jan Burse <bur...@gm...>:
> 
> What is your "satisfaction" criterion exactly when you for
> example compare R0 and ZFC. This is a little vague to
> refere first to "reducibility" from Andrew, and then replace
> it by your own "expressiveness".
> 
> Does this have something to do with recursion theory?
> Why do you think R0 and ZFC have different "expressiveness",
> in what respect exactly? Do you consider ZFC with our without
> classes. Levy, Basic Set Theory and also metamath,
> 
> which is closely modelled after Levy, Basic Set Theory classes,
> both have ZFC with classes. In ZFC with classes you
> have something like beta reduction, for example:
> 
>     x in { y | P(y) }  <=> P(x)
> 
>     http://us.metamath.org/mpegif/df-clab.html
> 
> This is pretty much the same as beta-conversion:
> 
>     (lambda y.P(y))x = P(x)
> 
> So there is not much difference between R0 and ZFC with classes.
> So why do you think one is superior to the other? Did you
> make a systematic research based on the actual 
> 
> underpinnings of ZFC with classes, 
> respectively its metamath incarnation?
> 
> Am Donnerstag, 3. Mai 2018 23:47:59 UTC+2 schrieb Ken Kubota:
> If the criterion is representing all of mathematics, then ZFC is unsatisfactory.
> 
> Of course, a language capable of doing so requires dependent types.
> Therefore, I have extended Q0 (simple type theory) to R0,
> which provides some of the means for dependent types, see pp. 11 f. of
> 	http://doi.org/10.4444/100.3
> 
> For the definition of the universal quantifier in R0, see p. 359.
> (The logical constant 'Q' was replaced by '=', since 'Q' has no own syntactic function.)
> This definition simply defines the universal quantifier as the set of properties (sets) in which
> all objects of the given type are mapped to true (are element of), hence the proposition holds 'for all'.
> Moreover, the variable binders are reduced to a single one (lambda).
> 
> I share Bertrands Russell's program of logicism (that mathematics is reducible to formal logic),
> hence a sharp distinction between both of them is rather difficult.
> A preliminary distinction may be the limitation of the language to rather simple definitions
> (such as on pp. 359 f., using basic types like 'o' and similar only; for comparison, see
> the rather complex group definition on p. 362).
> 
> Types naturally express the distinctions between different kinds of mathematical objects
> (e.g., between numbers and operators) made by the mathematician intuitively.
> There are some excellent quotes on this in Andrews' 2002 textbook.
> Indeed, types are more fundamental than objects of first-order logic, as you,
> for example, wish to distinguish between propositions (of type 'o'), operators ('oo'),
> and connectives ('ooo' = '((oo)o)'). Type theory naturally expresses the grammar
> of formal logic (and mathematics).
> 
> In lambda calculus, variables are clearly distinguished from constants (primitive symbols,
> lambda abstractions and lambda applications) by the fact that only variables can be
> bound by lambda (and by Theorem 5215 [Andrews, 2002, p. 221], instantiated freely).
> Lambda calculus allows the reduction of functions of more than one argument to
> those of just one argument (implementing Schönfinkel's concept), so "we can avoid explicitly
> admitting into our language functions of more than one argument." [Andrews, 2002, p. 206]
> 
> All of mathematics can be expressed using just a few principles, which Andrews calls
> "expressiveness" (I prefer the term "reducibility").
> 
> For the references, please see: http://doi.org/10.4444/100.111
> 
> Ken
> 
> ____________________________________________________
> 
> 
> Ken Kubota
> http://doi.org/10.4444/100
> 
> 
> 
>> Am 03.05.2018 um 22:52 schrieb Jan Burse <bu...@gm...>:
>> 
>> I did NOT say its unsatisfactory. Its very satisfactory, 
>> since its very flexible, and still doesn't have too much 
>> assumptions built in. 
>> 
>> Also I don't know what you mean by type theory. Simple
>> types, dependent types? In ZFC the logic part is delegated
>> to FOL=, and the domain part is ZFC itself built on the
>> 
>> logic part, thats a very nice separation, how do you apply 
>> your type theory? For example if you define in Q0 the forall 
>> operator (later used in the forall quantifier) as follows:
>> 
>>    Πο(οα) stands for [Qο(οα)(οα) [λxα Tο] ] 
>>    https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
>> 
>> Then things are somehow upside-down. You use types,
>> a kind of domain, to define logic. How do you justify such
>> a proceedings?
>> 
>> Am Donnerstag, 3. Mai 2018 22:31:55 UTC+2 schrieb Ken Kubota:
>> Hi Jan,
>> 
>> I definitely agree on that ZFC is unsatisfactory: This is why I prefer type theory.
>> 
>> But historically ZFC (axiomatic set theory) was designed exactly for this purpose
>> in the aftermath of Russell's paradox, see [Zermelo, 1908] (English translation [Zermelo, 1967]).
>> 
>> For the references, please see: http://doi.org/10.4444/100.111
>> 
>> Ken
>> 
>> ____________________________________________________
>> 
>> 
>> Ken Kubota
>> http://doi.org/10.4444/100
>> 
>> 
>> 
>>> Am 03.05.2018 um 22:08 schrieb Jan Burse <bu...@gm...>:
>>> 
>>> For example Ramsey Cardinal and V=L seem to be two
>>> opposite extensions of ZFC, in some aspects. 
>>> 
>>> So I am very currious how this would look like in metamath,
>>> the other post "Definition of L" form 6. April,
>>> 
>>> and more...
>>> 
>>> Am Donnerstag, 3. Mai 2018 22:03:51 UTC+2 schrieb Jan Burse:
>>> I don't agree with what Ken wrote: "But all the systems in discussion 
>>> here (e.g., ZFC) implicitly or explicitly claim to represent (significant 
>>> parts of) mathematics". 
>>> 
>>> If you read Levy, Basic Set Theory, you see that ZFC has a lot of 
>>> holes, and isn't in itself interesting mathematics. Its a foundation you 
>>> need to apply and/or extend.
>>> 
>>> Am Donnerstag, 3. Mai 2018 17:22:59 UTC+2 schrieb Ken Kubota:
>>> Hi Russell, 
>>> 
>>> While your statement (a "proof" always refers to a proof within a certain formal system) is correct looked at in an isolated way, 
>>> I find it problematic as it overlooks that the formal systems (deduction systems) in discussion here are designed to represent mathematics. 
>>> 
>>> Of course, this is the standard use of the terminology ("Now we prove the theorem MUIIU." - p. 179), 
>>> even in toy systems such as the MIU system, cf. pp. 177 ff. at 
>>>         http://us.metamath.org/downloads/metamath.pdf 
>>> 
>>> But all the systems in discussion here (e.g., ZFC) implicitly or explicitly claim to represent (significant parts of) mathematics, 
>>> making it difficult to follow a pure relativism (denying provability "in any absolute sense"). 
>>> For example, if one of the systems mentioned previously would be shown to be inconsistent (or otherwise not sound), it would be discarded. 
>>> 
>>> Moreover, I would even argue that some of these formal systems are better than others in representing mathematics, 
>>> e.g., type theory is superior to (axiomatic) set theory, and the ideal system should follow the concept of expressiveness of Q0 
>>> by Peter B. Andrews, who regularly emphasizes that mathematics should be expressed "naturally". 
>>> 
>>> Hence, there should be an ideal formal system for representing mathematics, and proofs in it would be proofs in an "absolute sense". 
>>> 
>>> I still owe Randy an answer in the HOL mailing list, which I hope to finish soon. 
>>> 
>>> Best regards, 
>>> 
>>> Ken 
>>> 
>>> ____________________________________________________ 
>>> 
>>> 
>>> Ken Kubota 
>>> http://doi.org/10.4444/100 
>>> 
>>> 
>>> 
>>> > Am 03.05.2018 um 02:57 schrieb ro...@th...: 
>>> > 
>>> > On Thu, 3 May 2018, Jose Manuel Rodriguez Caballero wrote: 
>>> > 
>>> >> Russell said: 
>>> >> "I also want to point out that proving that PA is consistent doesn't by itself mean that there isn't a proof that PA is inconsistent” 
>>> >> Ok, we are not talking the same language. In my world: PA is consistent means that there isn't a proof that PA is inconsistent (a proof that 1=0 formalized inside PA). I’m following 
>>> >> Hilbert’s metamathematical standards: https://plato.stanford.edu/entries/hilbert-program/ 
>>> 
>>> > Firstly, your statement is incomplete.  There isn't a proof according to what system?  Please, if you are going to dive into logic like this, don't use the term "proof" unaddorned like this.  Mathematical statements are not provable in any absolute sense.  Mathematical statements are only provable or not within some deduction system.  Coq can prove something, or ZFC can prove something or PA can prove something, and these different systems form completely different classes of statements of what they can or cannot prove. 
>>> 
>>> > Let me reiterate again that "Essential Incompleteness of Arithmetic Verified by Coq" is only claiming that "PA is consistent" is provable in Coq (and this is just a side remark within that paper).  This is a claim that you can directly verify yourself by downloading the development and checking it in Coq and seeing for yourself that Coq indeed considers the deduction valid.  The paper does not directly claim that "PA is consistent" is true; that would only follow if you assume that Coq is sound, and the paper doesn't discuss the soundness of Coq. 
>>> 
>>> 
>>> -- 
>>> You received this message because you are subscribed to the Google Groups "Metamath" group.
>>> To unsubscribe from this group and stop receiving emails from it, send an email to met...@go....
>>> To post to this group, send email to me...@go....
>>> Visit this group at https://groups.google.com/group/metamath.
>>> For more options, visit https://groups.google.com/d/optout.
>> 
>> 
>> -- 
>> You received this message because you are subscribed to the Google Groups "Metamath" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to met...@go....
>> To post to this group, send email to me...@go....
>> Visit this group at https://groups.google.com/group/metamath.
>> For more options, visit https://groups.google.com/d/optout.
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to met...@go....
> To post to this group, send email to met...@go....
> Visit this group at https://groups.google.com/group/metamath.
> For more options, visit https://groups.google.com/d/optout.