Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory?

Ken Kubota

unread,

Mar 9, 2020, 7:21:23 AM3/9/20

to coq-...@inria.fr, agda-list, lean-user, meta...@googlegroups.com, Martin Escardo, James McKinna, Prof. Peter B. Andrews

There are two problems with this quote in favor of set theory.

1. The axioms of set theory are historically contingent, i.e., they only cover the mathematics practiced at a given time.

For example, ZFC doesn’t cover large cardinals. An additional axiom is necessary.

One can easily generalize this argument by establishing new mathematical fields not covered by a given set of axioms.

As mentioned earlier:

I would consider type theory superior to set theory as type theory is a systematic approach, whereas the axioms of set theory are historically contingent.

https://groups.google.com/d/msg/lean-user/_A82awhFlcM/4odQJX3rCgAJ

2. It should be possible to derive all of mathematics from type theory (in particular, from a dependent type variant of Andrews' Q0).

This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").

Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".

The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:

https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ

fl

unread,

Mar 10, 2020, 3:45:51 PM3/10/20

to Metamath

What would be interesting and relevant would be a formalization of the different types of theories of types applied to lambda calculus.

At the moment we have the Simple Type Theory (i.e. HOL) developed by Mario Carneiro but there are many type theories.

Dependent Type Theory is only one of them. Of course it would need a lot of commentary and references to book sources.

--

FL

fl

unread,

Mar 11, 2020, 2:57:01 PM3/11/20

to Metamath

I took a quick look at Jouko Väänänen's article in the Standford Encyclopedia, an article referenced by Mario in his Higher-Order Logic Explorer Home Page. I think it's a very good article because there were some things that were not clear to me until now that suddenly made sense. I would just like to make one comment. Mr. Väänänen says that in first-order logic it is impossible to talk about a collection of natural numbers. This seems suspicious to me because set.mm is full of propositions using a set of natural numbers. Suddenly I understood. The author doesn't have FOL + ZFC in mind, because in this case his remarks don't make sense; he thinks of FOL + Peano (the system of axioms for arithmetic designed by the Italian mathematician). In this case everything is perfectly clear since in such a system the individual variables can only denote isolated natural numbers.

I can also add that, in a way, the quantifier added to second order logic simply quantifies what, in set.mm, would be a propositional variable. In fact, this remark should only be seen as an analogy, because in second order logic propositional variables also exist. (If formalized in a "metamath" style.)

It would be interesting to add a formalization of a second order logic with Peano's axioms and taking this paper as a basis. This would show concretely what all this means.

--

FL

Mario Carneiro

unread,

Mar 11, 2020, 3:14:30 PM3/11/20

to metamath

While it is not explicitly based on Väänänen's article, I should note that the Peano arithmetic formulation that I'm working on in peano.mm1 (https://github.com/digama0/mm0/blob/master/examples/peano.mm1#L974-L977) is quite similar to this. It axiomatizes PA in much the same way as set.mm axiomatizes ZFC. There are "class variables" (called "set" denoting possibly infinite sets of natural numbers), as well as a sort "nat" for individual variables, and there is only quantification over nat, resulting in a "slightly second order" conservative extension of PA.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e63e5824-1b42-40d1-94a4-f6b7965d4ca5%40googlegroups.com.

fl

unread,

Mar 11, 2020, 3:25:52 PM3/11/20

to Metamath

> There are "class variables" (called "set" denoting possibly infinite sets of natural numbers)

It's true. There are also class variables. So I'm wondering how to do to get a system close

to what Mr Väänänen had in mind. A system without class variables ?

--

FL

fl

unread,

Mar 11, 2020, 3:43:30 PM3/11/20

to Metamath

Moreover, it is rather the class variables of the first-order logic than the propositional

variables that are quantified by the additional quantifier in the second-order logic.

--

FL

Mario Carneiro

unread,

Mar 11, 2020, 4:12:53 PM3/11/20

to metamath

You can't really do raw first order logic in metamath, you would need an infinite number of axioms (even for things like propositional logic). Metamath needs to be able to use schemes to define axiom systems, and to write those schemes you need some concession to higher order variables, although you can limit their scope such that you get exactly the correct "first order image" out if no second order variables appear in the statement.

The use of class variables in peano.mm1, as in set.mm, is a convenience only. The real power is already encapsulated in the wff variables, which are schematic variables that do not appear in raw FOL. This is done for a variety of practical reasons, including the exponential speedup it brings relative to direct from axioms proofs, but it is this very speedup that indicates that a real strengthening of the system is at work (conservative though it is). A similar phenomenon happens in FOL vs SOL as traditionally studied. For example, ACA_0 is a conservative extension of PA, but there are O(n) proofs in ACA_0 whose shortest proof in PA has length O(2^^n) (that is, 2^....^2 n times), if I recall correctly. The peano.mm0 system lies somewhere in between these systems, because ACA_0 can have formulas containing any number of second order quantifiers, as long as they don't appear in instances of the induction axiom, while peano.mm0 can only do one level of second order universal quantification (i.e. Pi^1_n, one second order universal quantifier and any number of first order quantifier alternations), which is why it gets only an exponential speedup (or possibly double exponential, not sure) rather than an iterated exponential speedup.

Again, set.mm is in the same position between ZFC and second order ZFC (also known as NBG). NBG is a conservative extension of ZFC with second order quantifiers, but not in the schemes (otherwise the proof system becomes stronger and you get MK set theory instead). All the same kinds of theorems from above still apply. ZFC (resp. PA) is not finitely axiomatizable, but proves all its finite fragments. NBG (resp. ACA_0) is finitely axiomatizable, and set.mm (resp. peano.mm0) is also finitely axiomatizable (axiomatized, even - they are clearly text files of finite length). The proofs of the finite fragments of ZFC (resp. PA) get longer and longer, irreducibly, because you necessarily have to bring in the power of the higher levels. The speedup comes from the fact that the higher order axiomatizations have compact ways of referring to these higher levels. (See Solovay's method of "shortening of cuts".)

On Wed, Mar 11, 2020 at 12:43 PM 'fl' via Metamath <meta...@googlegroups.com> wrote:

Moreover, it is rather the class variables of the first-order logic than the propositional
variables that are quantified by the additional quantifier in the second-order logic.

To clarify: the reason why class variables and wff variables are equivalent in strength here is because of binding notations like "A." that can take a set variable and a wff variable and bind the set variable in the wff. This means that a wff variable can have some number of free variables that can later be bound, and so the denotation of a wff variable is really a relation on all its free variables, which is a proper class, a second order variable in SOL. If a wff was really just a truth value, then every wff would be equivalent to T. or F., but this implies that "A." is useless, since "A. x T." is equivalent to "T." and "A. x F." is equivalent to "F." - but this is clearly not the case, "A. x ph" is not equivalent to "ph" in general. A class variable is also a relation on its free variables, plus one designated extra variable that is baked into the class itself. That is, it's just an n+1-ary relation for some n. This is why you can easily go back and forth between class variables and wff variables using the syntax constructors "{ x | ph }" and "x e. A".

Mario

fl

unread,

Mar 12, 2020, 8:21:44 AM3/12/20

to meta...@googlegroups.com

Thank you for all these interesting remarks. I think I will spend some time on the logic of the second order. So I note that there are two ways to formalize second-order logic: either by typing or by using separate quantifiers. And that the case of typing can be subdivided into two sub-cases: either by adding the type to the variable or by using different letters (as Metamath does).

I find your code rather readable.

--

FL

fl

unread,

Mar 12, 2020, 10:56:59 AM3/12/20

to Metamath

"Second-order logic is more expressive than first-order logic. For example, if the domain is the set of all real numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀x ∃y (x + y = 0) but one needs second-order logic to assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum." Wikipedia 'Second-Order Logic'.

I insist. That kind of sentence is wrong. In FOL + ZFC we can express the least-upper-bound property for real numbers. Maybe in FOL+ Real if Real is a system of axioms of real numbers we cannot. But at last we must stop giving this kind of example without specifying the axiomatic added to FOL.

--

FL

fl

unread,

Mar 12, 2020, 3:16:05 PM3/12/20

to meta...@googlegroups.com

I insist. That kind of sentence is wrong. In FOL + ZFC we can express the least-upper-bound property for real numbers. Maybe in FOL+ Real if Real is a system of axioms of real numbers we cannot. But at last we must stop giving this kind of example without specifying the axiomatic added to FOL.

Ah! Yes. They specify the domain. But it's barely visible, and even less decodable.

--

FL

Ken Kubota

unread,

Mar 13, 2020, 12:06:42 PM3/13/20

to coq-...@inria.fr, Prof. Peter B. Andrews, Prof. Kevin Buzzard, meta...@googlegroups.com, lean-user, agda-list

Hi Thorsten,

Am 10.03.2020 um 12:10 schrieb Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>:

2. It should be possible to derive all of mathematics from type theory (in particular, from a dependent type variant of Andrews' Q0).
This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").
Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".
The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:
https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ

I don’t agree with this description. As set theory, type theory is an evolving system. For example a while ago we were using intensional type theory with uniqueness of identity proofs and now we have a much more extensional type theory with univalence and without uip. And also the question isn’t just wether we “can derive” all Mathematics but can we structure mathematical constructions in a reasonable way. Otherwise we are left with the usual argument that all programs can be written in machine language.

It seems that the traditions of type theory we represent are very different, so a reasonable answer should reflect the underlying basic design decisions.

In the examples you mention intensional type theory, the univalence axiom, and the desire to "structure mathematical constructions in a reasonable way".

My concept of type theory is in the tradition of Russell, Church, and Andrews – in particular Andrews' Q0, which is an elegant reformulation of Church's type theory (1940, see: https://owlofminerva.net/sep-q0).

The purpose of the types in this concept of type theory is mainly to preserve the dependencies such that (negative) self-reference causing paradoxes/antinomies is avoided, as discussed here: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html

This means that types are the result of simple operations such as lambda abstraction and lambda application (cf. wff constructions (b) and (c) at [Andrews 2002 (ISBN 1-4020-0763-9), p. 211]).

Moreover, using Andrews' concept of "expressiveness" (also intuitively used by Church before), all mathematical concepts can be reduced – naturally (not like in machine language) – to a few basic notions:

Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.

R0 has only little more (some features required for type variables, type abstraction, and dependent types).

Both are Hilbert-style systems (operating at the object language level only).

The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.

The univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.

These motivations have their legitimation, but shouldn’t be part of the formal language.

For this reason I already object to the Pi type (as implemented in Lean), or dependent function type, which I consider a metamathematical notion: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ

I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.

How is type abstraction implemented in Lean, and where can I find the group definition?

Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.

I fully agree to Kevin Buzzard’s argument that "within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe." – https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

Ken Kubota

unread,

Mar 14, 2020, 4:38:18 PM3/14/20

to meta...@googlegroups.com

Simple Type Theory doesn't have type variables.

Since HOL (by Mike Gordon) has type variables, it is not Simple Type Theory, but Polymorphic Type Theory.

____________________________________________________

Ken Kubota

doi.org/10.4444/100

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2337506c-0c61-4269-be58-cde052ed7ec7%40googlegroups.com.

Ken Kubota

unread,

Mar 14, 2020, 6:00:48 PM3/14/20

to coq-...@inria.fr, Prof. Peter B. Andrews, Prof. Kevin Buzzard, meta...@googlegroups.com, lean-user, agda-list

Am 13.03.2020 um 17:19 schrieb Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>:

This means that types are the result of simple operations such as lambda abstraction and lambda application (cf. wff constructions (b) and (c) at [Andrews 2002 (ISBN 1-4020-0763-9), p. 211]).

This means you have a very intensional view of Mathematics centred around encodings. I think this is misleading because Mathematics is about abstraction and abstract concepts, encodings are only coincidental.

Of course, encoding is not a self-purpose.

That all logical connectives can be defined in terms of the Sheffer stroke is coincidental and not of particular interest.

But the concept of expressiveness (reducibility) used by Andrews (and intuitively by Church) is very natural, and for good reason many mathematicians endorse these formulations of higher-order logic (Church's type theory, Andrews' Q0, Gordon's HOL), and the implementations are widely used (HOL4, HOL Light, Isabelle/HOL).

In this concept, the reduction to certain primitive symbols is very natural and reveals the inner logic of high level notions.

Moreover, using Andrews' concept of "expressiveness" (also intuitively used by Church before), all mathematical concepts can be reduced – naturally (not like in machine language) – to a few basic notions:
Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.
R0 has only little more (some features required for type variables, type abstraction, and dependent types).

Both are Hilbert-style systems (operating at the object language level only).

This seems to be a view of mathematical foundations stuck in the middle of the last century.

The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.
The univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.
These motivations have their legitimation, but shouldn’t be part of the formal language.

For this reason I already object to the Pi type (as implemented in Lean), or dependent function type, which I consider a metamathematical notion: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ

I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.

So you are only interested in some mathematical machine code but not in the high level notions. Such a view of mathematical foundation is akin to the view some programmers had (and maybe still have) that all what matters is machine code. To the contrary you can build the same foundations on different notions of machine code. The machine code is irrelevant, all what matters are the abstractions.

It is important to distinguish two different kinds of high level notions:

Those that can be reduced naturally to primitive symbols, and those which try to express metamathematical ideas (which seems to be your notion).

The latter shouldn't be implemented as primitive symbols in the basic formal language, but should be the result of metamathematical reasoning.

How is type abstraction implemented in Lean, and where can I find the group definition?

I have no idea about Lean, not do I know what you mean by “type abstraction”. Polymorphism, that is constructions which are parametric in types are simply depdnent functions which have a universe as input.

Lambda as the single variable binder in formulations of higher-order logic (Church, Andrews, Gordon) traditionally can be used to bind _term variables_ only.

Type abstraction allows for binding _type variables_ also.

See https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/

and https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html

Kevin Buzzard has (like Freek Wiedijk) correctly stated that current classical higher-order logic is too weak to express certain mathematical concepts.

The main reason is that the feature of type abstraction is missing.

Gordon has suggested implementing this, but unfortunately this didn't happen in the current HOL systems (HOL4, HOL Light, Isabelle/HOL).

Andrews and Melham did some work into this direction, but used the traditional quantifiers to bind type variables, not lambda.

Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.

I fully agree to Kevin Buzzard’s argument that "within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe." – https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

I think you miss a trick or two here. Constructivism is highly relevant, especially in computer science when we want to marry computer science with mathematical constructions. Hilbert is already dead since a while and before the first computer has been build. The world is changing, maybe philosophers and mathematicians should take notice of this.

The formulation of the formal system depends on the purpose.

Even within mathematics different formulations are required: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/lArtWey5CQAJ (last part on the two-step approach).

However, from a logical (mathematical) point of view I do not see any need for constructivism.