Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 27, 2020

Dependent Type Theory as an n-Theory

Posted by David Corfield

Here are slides for a talk I gave last week to my department on some of the advantages for philosophy of adopting dependent type theory. It revolves around Mike’s very interesting theory of n-theories.

MathOverflow saw a flurry of activity the same day on the advantages for proof assistants.

Posted at November 27, 2020 7:20 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3271

59 Comments & 0 Trackbacks

Re: Dependent Type Theory as an n-Theory

It looks like your slide link is wrong.

Posted by: Anthony Hart on November 27, 2020 7:47 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Found the link at nlab: https://ncatlab.org/davidcorfield/files/EvidSem2.pdf

Posted by: Kartik Singhal on November 27, 2020 11:12 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Sorry. Fixed now.

Posted by: David Corfield on November 28, 2020 2:05 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Regarding the MathOverflow topic, I believe the problem isn’t actually whether set theory is less suited for proof assistants than type theories, (both should be equally fine as a foundation for proof assistents) but rather that the most common set theory used by mathematicians happens to be the unwieldy ZFC axioms with first-order classical logic, which gives the appearence that set theories are less suited than type theories, as people think that set theory is ZFC. The solution then would be for the mathematics community, if it wishes to stay with set theories, to move away from ZFC towards a less cumbersome but equally strong axiom system for set theory, such as ECTS + reflection & choice.

Posted by: Madeleine Birchfield on November 28, 2020 3:43 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

I wonder if anyone has a proof assistant employing ECTS.

Ah, I hadn’t noticed in Mike’s In Praise of Dependent Types that he sees dependent types in ordinary language too:

… the point I’m making is that in mathematics and in everyday language, dependent types are what we really talk about, and their encoding in ZFC or ETCS is just that – an encoding.

So it’s not about the power of a system. Neither ZFC nor ETCS allow the same naturalness of expression.

Posted by: David Corfield on November 28, 2020 2:15 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

That’s an interesting remark! I’ve never heard of anyone trying to design a proof assistant around ETCS (with or without stronger axioms). However, there are plenty of very popular proof assistants designed around higher-order logics, which are quite similar to ETCS in flavor, especially if you make ETCS more palatable with abuses of notation (or extensions to the language) like writing x:Ax:A (or xAx\in A or x:Ax:\!\!\in A) to mean x:1Ax:1\to A and considering A×BA\times B and B AB^A to be operations on sets rather than merely \forall\exists axioms. Is HOL a “set theory”? Is SEAR a “set theory”? Is extensional MLTT a “set theory”? They all have set-like 1-categories such as (pre)toposes as their natural models. At some point the argument becomes about the meaning of the word “set theory”.

However, it does seem clear to me that in the intent of the asker of that MO question, “set theory” referred to “membership-based set theory” of the ZFC-sort.

Posted by: Mike Shulman on November 29, 2020 7:48 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

The comparison between conventional set theory (or HOL) and a set theory like ETCS raises the following point (which occurred to me when I read Tom Leinster’s “Rethinking set theory” when it appeared, 2012 I think). One could call it the “How is John Lennon a morphism?” problem. But it’s ultimately to do with what is more conceptually basic.

Why is

x:1Ax : 1 \longrightarrow A

more conceptually basic than

xAx \in A

is?

On the second, we have a collection AA of things “with a lasoo around it” (Kripke’s phrase), and xx is inside the lasoo. On the first, I have no intuition at all about it. Eg,

(i) JohnBeatlesJohn \in Beatles

(ii) John:1BeatlesJohn : 1 \longrightarrow Beatles

The first makes sense to me: John belongs the collection of things with the lasoo around it. In the second, John is a “morphism” from 11 to that collection of things. But how is John Lennon a “morphism”?

I don’t doubt that one can perhaps generate a formal system in which these come out as provable equivalents (as there must be some common definitional extension). But even so, I don’t see how John Lennon is a morphism, though perhaps one can “model” John Lennon as a morphism. But then I don’t know what that means, other than “John \in Beatles”, and (ii) turns out equivalent to it.

Implicitly, I think of John (or a spacetime event, or a voter, or a rabbit, or a planet, etc) as an atom or urelement, which isn’t a collection at all and so doesn’t have elements. One can also think of natural numbers, real numbers, etc. as atoms/urelements too. So the obvious way to do this is set theory with atoms, which is closely related to HOL or type theory, which has a ground level of individuals, perhaps organized into complicated sorts. That’s essentially how second-order arithmetic works (or second-order geometry). We have a ground level of numbers and their six governing axioms (0 isn’t a successor, n+0=nn+0=n, etc), along with Comprehension, Induction and Extensionality for sets of numbers. But numbers aren’t “sets”. They’re atomic individuals.

Posted by: Jeffrey Ketland on November 30, 2020 2:07 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

The fact that ETCS defines xAx\in A to mean x:1Ax:1\to A is just a choice. Some people like it because it reduces the number of basic notions: instead of sets, functions, and elements you have just sets and functions. (Encoding mathematics in ZFC requires lots of different but equally weird-looking choices, like 2={,{}}2 = \{\emptyset, \{\emptyset\}\} and (a,b)={{a},{a,b}}(a,b) = \{\{a\},\{a,b\}\}.) But if you prefer, it’s easy to formulate a theory nearly identical to ETCS in which elements are a basic notion not defined as morphisms. In SEAR I did something like that, also replacing the functions by relations. But of course, as you say, type theory and HOL also solve this issue.

Posted by: Mike Shulman on November 30, 2020 5:07 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Right, but isn’t xAx \in A just conceptually very basic? Theories T 1T_1 and T 2T_2 might be entirely equivalent (i.e., definitionally equivalent) but even so, the basic notions of one might be weird compared to the basic notions of the other.

In principle, one could treat natural numbers as atoms (likewise integers, rationals, reals) and treat pairs as atoms too, all with their appropriate axioms. The axioms for the “natural number atoms” are PA1-PA6 and the set version of induction (if X contains 0 and is closed under S, then X contains all numbers). The relevant categoricity theorem should be provable, and this shows that this system (,0,S,)(\mathbb{N}, 0, S, \dots) of atoms is isomorphic to (ω,,() +,(\omega, \varnothing, (-)^{+}, \dots) of finite ordinals. I think that resolves “2={,{}}2 = \{\varnothing, \{\varnothing\}\}” etc. I.e., it’s false!

Did your SEAR system get published? (I did read it, but several years ago)

Posted by: Jeffrey Ketland on November 30, 2020 9:56 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Mike posted on reasons to prefer the handling of elements by dependent type-theory over material and structural set theories back here.

Posted by: David Corfield on December 1, 2020 9:37 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Yes, I know. But Mike also mentions

In ZFC, the only things that exist are material-sets, so that AA in the proposition “AXA \in X” must itself be a material-set. However, some material-set theories include “atoms”; which are not sets, but which can be elements of material-sets.

and

For instance, we might augment ZFC with atoms, and define the natural numbers to be a set of atoms. We might similarly augment it with a basic “ordered pair” operation, or with a basic notion of “function” in addition to “set”.

That seems right to me. So, we might use (many-sorted, higher-order if need be) set theory with atoms. In my view, one has to do this, or something very similar, to account for applied mathematics. Similarly, HOL is STT (simple type theory): it has a bottom level of individuals, and then sets/relations of them, sets of sets of them, etc: a kind of stratified set theory with atoms, though weaker than the corresponding ZF system. And dependent types are really indexed collections {A iiI}\{A_{i} \mid i \in I\}. So it’s not really the case that someone somehow forgot them! They’re already there, used all the time. The only question is what might be the most practical or convenient way of defining or reasoning about them.

But I’ll repeat the original point. It’s hard to see how one can come up with a mathematical concept more primordial/basic than

xAx \in A

So it doesn’t make much conceptual sense to introduce lots of fancy concepts (morphisms, domains, codomains, initial and terminal objects, etc.) and then definexAx \in A” in those terms, say as

x:1Ax : 1 \longrightarrow A

It’s doable, of course.

But still that seems conceptually upside down. The concept of AA being “a collection of things with a lasoo around it” just seems to be ground level. Cantor expressed it similarly, from memory something like this: “a collection of objects brought together as a single object of thought”.

Furthermore, when one defines the cumulative hierarchy

V 0=V_0 = \varnothing

V α+1=P(V α)V_{\alpha + 1} = P(V_{\alpha})

V λ= α<λV αV_{\lambda} = \bigcup_{\alpha &lt; \lambda} V_{\alpha} (λ\lambda a limit)

V= αOrdV αV = \bigcup_{\alpha \in Ord} V_{\alpha}

Then one obtains a growing structure which is conceptually extremely rich: V ωV_{\omega}, say, contains all structural possibilities for finitely many objects.

Posted by: Jeffrey Ketland on December 1, 2020 5:44 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

You said,

It’s hard to see how one can come up with a mathematical concept more primordial/basic than

xAx \in A

I think the concept of truth and falsehood, logical implication, universal and existential quantifiers are as primordial and as basic of mathematical concepts as elements, sets, and membership. And therein lies the fundamental issue with this discussion about set theory vs type theory, it isn’t really set theory vs type theory, but rather logic and set theory vs type theory; i.e. type theory also replaces the entire framework of first-order classical logic with its type theory, in additional to replacing ZFC or ETCS or SEAR with type theory, which was one of the points that Mike made in his post, and which I personally feel is a more convincing argument in favour of dependent type theory than anything regarding the debate between material-sets vs structural-sets. Why have two foundational theories (logic and set theory) when you could have one (dependent type theory)?

Ignoring type theory and going back to set theory,

So, we might use (many-sorted, higher-order if need be) set theory with atoms. In my view, one has to do this, or something very similar, to account for applied mathematics. Similarly, HOL is STT (simple type theory): it has a bottom level of individuals, and then sets/relations of them, sets of sets of them, etc: a kind of stratified set theory with atoms, though weaker than the corresponding ZF system. And dependent types are really indexed collections {A iiI}\{A_{i} \mid i \in I\}. So it’s not really the case that someone somehow forgot them! They’re already there, used all the time. The only question is what might be the most practical or convenient way of defining or reasoning about them.

I think that set theory should be like classical first-order logic, which is not as parse in its primitives as set theory currently is right now, whether in ZFC or ECTS or SEAR or any other set theory. If we treated first-order logic as we do set theory as currently used, the basic primitives would be the sheffer stroke and the two quantification operators, and every other logical operator and constant would be derived from these basic primitives. But no modern treatment of first-order logic does that. They include primitives that may be redundant, but are more intuitive for the average user or the new student to learn and understand, such as conjunction, disjunction, negation and implication, some of which could be derived from the others. So, instead of only sets and functions, or sets and membership, maybe sets, elements, membership, functions, families of sets, et cetera should all be primitives of set theory, even though some of them might be redundant.

Posted by: Madeleine Birchfield on December 2, 2020 2:10 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Madeleine,

And therein lies the fundamental issue with this discussion about set theory vs type theory, it isn’t really set theory vs type theory, but rather logic and set theory vs type theory; i.e. type theory also replaces the entire framework of first-order classical logic with its type theory, in additional to replacing ZFC or ETCS or SEAR with type theory, which was one of the points that Mike made in his post, and which I personally feel is a more convincing argument in favour of dependent type theory than anything regarding the debate between material-sets vs structural-sets. Why have two foundational theories (logic and set theory) when you could have one (dependent type theory)?

I pretty much agree that this is perhaps the fundamental issue that keeps popping up, and it usefully separates that from certain tangential issues (like constructivity, notational issues; efficiency questions wrt intertranslatable equivalents). But the caveat I’d mention involves the following three, but interlinked, distinctions,

(i) Object language vs meta-language.

(ii) Logical truths vs extra-logical axioms.

(iii) Logical concepts vs non-logical concepts.

To cut a rather long story short, I tend to side with Quine on these connected matters. So, I’d see various set theories, HOL, STT, MLTT, etc., as systems of mathematics, not logic. I don’t see the mixing up of these two as a feature, but as a bug.

Logic is, in a sense, a foundation of everything; or, if one prefers, a foundation for all reasoning in a domain-invariant/topic invariant way.

On the other hand, set theory, type theory, HOL and so on are foundations for … well, our apparent knowledge of sets, types and ‘higher-order’ abstract thingies.

Posted by: Jeffrey Ketland on December 2, 2020 2:46 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

While I would agree with your characterisation of set theories as external to logic, I would disagree with your characterisation of HOL, STT, and MLTT, as I see those as systems of logic that are simply more expressive than FOL, and especially type theories I see as an theory of a typed logic with extra stuff.

This is why I personally believe that the set theory vs type theory debate is largely the wrong one, and the first-order logic vs type theory is the one that should take precedent, because logic comes before set theory in mathematics.

Posted by: Madeleine Birchfield on December 2, 2020 10:38 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

One could also subscribe to the logicist view and argue that all mathematics could be reduced to logic, and that higher order logic and type theories are evidence in favour of the logicist viewpoint.

Posted by: Madeleine Birchfield on December 2, 2020 11:31 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Why have two foundational theories (logic and set theory) when you could have one (dependent type theory)?

Because the simplification this ostensibly provides is somewhat of an illusion.

Dependent type systems are sufficiently flexible that to do metatheory, you end up factoring the type system into raw syntax, and typing rules. At this point, it looks rather like a rudimentary logical theory (a 1-theory!) of membership and equality on top of a functional programming language.

I’ll call this rudimentary logical theory the “logic of judgments”. It’s not the logic of propositions that gets used for math. But it’s there, and the syntax makes it look more basic than propositions. When basing your foundation more overtly on logic, you don’t have this extra layer.

These judgments aren’t entirely analogous to the judgments of a proof system for predicate logic, because with predicate logic, you don’t need to worry about the judgments when doing model theory. But with DTT, it seems you do.

So maybe dependent type systems are not really 2-theories. (Previously, I attempted to argue that ETCS could be considered a 2-theory. It didn’t work. But I can’t shake the feeling that they’re not as different as people around here seem to think.)

Posted by: Matt Oliveri on December 2, 2020 4:24 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

I wonder if it is possible to rewrite dependent type theory as a theory of sets and families of sets.

Posted by: Madeleine Birchfield on December 2, 2020 10:42 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

For sufficiently liberal notions of “theory” and “set”, then yes; this is a pretty typical thing to do when studying or implementing a type system in a logical framework. Especially with the “synthetic” style of encoding, the translation can be very systematic. The synthetic encoding of judgments is an example of what I mean by a “logic of judgments”. It’s a very bare bones logic, though.

Posted by: Matt Oliveri on December 3, 2020 7:55 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Jeff wrote

But I’ll repeat the original point…

which contrasts xAx \in A favourably with x:1Ax: 1 \to A.

The reason I brought up Mike’s discussion of type theory is that it uses a third formation, namely, x:Ax: A. This is not a proposition, such as xAx \in A, nor is it a function such as x:1Ax: 1 \to A.

It sounds to me like you still engaged in a comparison of material and structural set theory, when the post is about something else, namely, type theory.

Posted by: David Corfield on December 2, 2020 12:00 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Not sure if this comment was addressed to me or to Jeff.

Posted by: Madeleine Birchfield on December 2, 2020 12:27 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

To Jeff. We tend to avoid keep nesting, so we don’t get squeezed to the side.

Posted by: David Corfield on December 2, 2020 2:36 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Right, will put anything further down below!

Posted by: Jeffrey Ketland on December 2, 2020 3:27 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

If AA were a genuine quantifiable variable, we could treat “x:Ax : A” as a proposition, i.e.: “xx is of type AA”. And, for example, say “not-(sin:sin : \mathbb{N} \to \mathbb{N})”! That is, the sine function isn’t of the type \mathbb{N} \to \mathbb{N}.

Posted by: Jeffrey Ketland on December 2, 2020 1:49 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

And in type theory, people could treat propositions as types themselves.

Propositional logic is already syntactically a type theory whose only types are propositions, so the real question is whether we want in the predicate logic two types, one of propositions and one of sets, as found in classical first-order logic, or one type that treats both propositions and sets as instances of the same type.

The arguments over material and structural sets never enter into the picture in the first place.

Posted by: Madeleine Birchfield on December 2, 2020 2:29 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

If A were a genuine quantifiable variable, we could treat…

But then we wouldn’t be doing type theory, or at least not the intrinsic kind of type theory devised by Per Martin-Löf.

Posted by: David Corfield on December 2, 2020 2:40 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Something that I just realised is how much of the work on foundational set theory implicitly uses first-order logic as a foundation for said theory; i.e. ZFC and ETCS are both built built upon the axioms and primitives of first order logic, making most foundations in fact of two theories, one of sets and one of logical propositions. On the other hand dependent type theory seems to incorporates both set theory and first-order logic into one unified theory of types, which to me seems to be a lot more pleasing for foundations and proof assistents than having to implement two theories.

Posted by: Madeleine Birchfield on December 1, 2020 3:07 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Right. To put it in Mike’s terms, with a more expressive 3-theory, so a ‘logic’ that allows a richer form of judgment, one can specify via rules, a natural but powerful 2-theory (such as HoTT), without the need to specify via axioms a 1-theory (such as ETCS or ZFC).

Posted by: David Corfield on December 1, 2020 9:32 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Another reason to adopt type theory vs set theory, I think a set is basically a type with equality, which makes types more general than sets. The category of types would then be a finitely complete category with all pullback-stable disjoint coproducts and a terminal generator, and the category of sets would be the ex/lex completion of Type, making Set a Grothendieck topos on the terminal object. The category of dependent types would be a cartesian closed version of the above, whose ex/lex completion is the category of sets in impredicative mathematics.

Posted by: Madeleine Birchfield on January 21, 2021 6:24 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

That’s one traditional perspective on the relationship between type theory and set theory: that types don’t have equality and you have to add it to get a set (often called a “setoid” in this context). For instance, this is how many people have formalized Bishop’s constructive mathematics.

However, ultimately I believe that perspective is too limiting, because it restricts your notion of “set” to those that can be obtained as the ex/lex completion of something. In particular, your sets will always satisfy countable choice and even the presentation axiom. It’s better to view types as a generalization of sets in a different way: every type has an “equality” that’s another type, with the sets being those types whose equality types are propositions (i.e., have at most one element). This is the perspective of homotopy type theory.

Posted by: Mike Shulman on January 21, 2021 4:40 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

However, ultimately I believe that perspective is too limiting, because it restricts your notion of “set” to those that can be obtained as the ex/lex completion of something. In particular, your sets will always satisfy countable choice and even the presentation axiom.

Perhaps Set as the ex/lex completion of Type is the wrong characterisation of Set, and Set should be thought as the subcategory of Type as characterised above where all equivalence relations on a type have effective quotient types that are pullback-stable.

Posted by: Madeleine Birchfield on January 21, 2021 9:50 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Regarding homotopy type theory, I think the types are actually infinity groupoids in disguise in that theory and a set is simply a 0-truncated infinity groupoid.

Posted by: Madeleine Birchfield on January 23, 2021 10:02 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

That’s correct, except that I would say they’re not in disguise at all. (-:

Posted by: Mike Shulman on January 25, 2021 2:08 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Then I wonder if it is better to think of groupoids and higher groupoids as generalised sets with generalised equality, rather than as categories with specific symmetric properties.

Posted by: Madeleine Birchfield on January 26, 2021 6:30 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Indeed! You may enjoy this piece by Voevodsky, where he wrote: “The greatest roadblock for me was the idea that categories are ‘sets in the next dimension.’ I clearly recall the feeling of a breakthrough that I experienced when I understood that this idea is wrong. Categories are not ‘sets in the next dimension.’ They are ‘partially ordered sets in the next dimension’ and ‘sets in the next dimension’ are groupoids.”

Posted by: Ulrik Buchholtz on January 26, 2021 8:00 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

This is argued for philosophers in Dimitris Tsementzis, What is a Higher-Level Set?.

Posted by: David Corfield on January 26, 2021 8:17 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

On the other hand dependent type theory seems to incorporates both set theory and first-order logic into one unified theory of types, which to me seems to be a lot more pleasing for foundations and proof assistents than having to implement two theories.

In first order logic, historically in the 19th century the universal quantifier was represented as Π x\Pi_x and the existential quantifier was represented by Σ x\Sigma_x. It wasn’t until the early 20th century that Peano invented x\exists x for the existential quantifier and the 1930s when Gentzen invented x\forall x for the universal quantifier. The modern quantification symbols didn’t get widely adopted by the mathematics community until the 1960s. From this perspective, dependent type theory with its use of dependent product and sum types for universal and existential quantification is only a return to the notation of 19th century mathematics.

Posted by: Madeleine Birchfield on February 1, 2021 5:19 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Regarding the MathOverflow topic, I believe the problem isn’t actually whether set theory is less suited for proof assistants than type theories, (both should be equally fine as a foundation for proof assistents) but rather that the most common set theory used by mathematicians happens to be the unwieldy ZFC axioms with first-order classical logic, which gives the appearence that set theories are less suited than type theories, as people think that set theory is ZFC.

My view on this has changed significantly, since most set theories are type theories in disguise.

ZFC for example is a simple type theory consisting of two types, the type of propositions and the types of sets, and certain connectives that take in parameters of type propositions (and, or, implication) or type sets (equality, membership) and returns a proposition.

ETCS is a type theory consisting of three types, a type of propositions, a type of sets, and a type of functions dependent on two sets, with different connectives for propositions, sets, and functions.

Thus one could create a proof assistent from ZFC or ETCS, but most likely it would be inherently type theoretic, whether explicitly or implicitly.

Posted by: Madeleine Birchfield on February 1, 2021 9:53 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

First-order logic is a type theory too, as I discussed last week in Oxford.

Posted by: David Corfield on February 2, 2021 9:17 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

ZFC and ETCS are formulated in a type theory (FOL), but the difference is that their contentful information is carried by axioms rather than by the rules of the type theory. This is admittedly a continuum rather than a binary distinction, since (e.g.) Book HoTT is primarily a type theory but relies also on the univalence axiom, but that doesn’t make it less real.

Posted by: Mike Shulman on February 2, 2021 2:15 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

ZFC and ETCS are formulated in a type theory (FOL), but the difference is that their contentful information is carried by axioms rather than by the rules of the type theory.

So would it be more accurate to describe homotopy type theory as a theory formulated in Martin-Lof type theory + higher inductive types, due to the univalence axiom not being a type former?

Posted by: Madeleine Birchfield on February 2, 2021 2:58 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

I think general inductive and higher inductive types in homotopy type theory also require axioms for the computational rules for their point and path constructors.

Posted by: Madeleine Birchfield on February 2, 2021 3:31 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Well, firstly, the way I use the term, “homotopy type theory” is the name of an entire subject, like “homotopy theory” or “number theory”; not the name any particular formal system or axiomatic theory. The theory we’re talking about here is sometimes called “Book HoTT” since it was used in the HoTT book, although it’s not completely formally specified since the book doesn’t give general rules for the allowable HITs.

You’re right that HITs in Book HoTT involve axioms for their path constructor computation “rules”. But the computation rules for ordinary inductive types, and the point constructor computation rules of HITs, are judgemental equalities and not axioms, so in particular Book HoTT cannot be simply described as “MLTT + axioms” since its HITs are not implementable by axioms.

Moreover, as I said, it’s a continuum, not a sharp dividing line. And, of course, an “axiom” can be written as a rule without premises, so formally you are free to regard it as just a type theory with no axioms. Which one could also do with ZFC and ETCS by adding their axioms as “rules” to FOL. (Somewhere else recently we talked about this process of “making a 1-theory into a 2-theory”; anyone have the link?) So the only distinction to be made is a subjective one, and I think Book HoTT is clearly primarily a type theory with just a few axioms, while ZFC and ETCS are clearly primarily systems of axioms that rely only on the ambient FOL for the logical superstructure.

Posted by: Mike Shulman on February 3, 2021 11:26 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Here’s one place where we speak of lifting. It crops up again in that thread.

Regarding the idea that the axiom/rule distinction is subjective, I’ve been flirting with the thought that having one’s power expressed via rules (in a 2-theory) avoids ‘ontological commitment’ in a way that axioms don’t. After all, philosophers typically don’t see FOL itself as generating such commitment.

But blurring the line might lead us to think it makes no difference (if the idea of commitment makes any sense in the first place).

Posted by: David Corfield on February 4, 2021 2:29 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Well, firstly, the way I use the term, “homotopy type theory” is the name of an entire subject, like “homotopy theory” or “number theory”; not the name any particular formal system or axiomatic theory.

I think I have done the same with the term ‘dependent type theory’ which I assumed was Martin-Lof dependent type theory in my previous comments here.

Posted by: Madeleine Birchfield on February 4, 2021 5:22 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Whoops, wrong comment; this was supposed to be in reply to Mike Shulman’s comment above.

Posted by: Madeleine Birchfield on February 4, 2021 5:35 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Thanks for the link.

That’s an interesting idea. Offhand it seems more to me like making the comparison points out that even single-sorted FOL does generate an ontological commitment, namely a commitment to the type of individuals (whether or not any individuals exist). That is, before you even formulate the axioms of ZFC, as soon as you state your intention to formulate a first-order theory of sets you’re committed to the existence of a type of thing called “sets”. (At least, insofar as any mathematical theory entails any ontological commitment, which I’m personally inclined to doubt, but hey.) But maybe I could see it going the other way.

Posted by: Mike Shulman on February 6, 2021 6:49 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

You know Mac Lane had a view on this:

The last chapter of my “big book” [Mathematics: Form and Function] deals with the philosophy of mathematics, with the hope of perhaps reviving this moribund field. My claim was that too many philosophers of mathematics pay too little heed to what there really is in mathematics. This applies in particular to Wittgenstein and Lakatos, but for now I take on the biggest living target. My learned and articulate friend Van Quine has claimed that ontology is served by observing that “to be” is to be existentially quantified. I disagree, and I also doubt if Van realizes that the existential quantifier is a left adjoint–an important observation, again due to Lawvere. (Is Mathias an Ontologist?, p. 120)

Mac Lane S. (1992) Is Mathias an Ontologist?. In: Judah H., Just W., Woodin H. (eds) Set Theory of the Continuum. Mathematical Sciences Research Institute Publications, vol 26. Springer, New York, NY.

It seems like an odd connection, but I can certainly relate to it. Years ago, coming to philosophy on the back of reading Lambek and Scott’s Introduction to Higher-Order Categorical Logic, I couldn’t see why analytic philosophers made such a deal of FOL. Couched in category-theoretic terms with its adjoints, it seemed to be an integral part of mathematics.

That sounds about right with FOL and its commitments. Maybe we wind the story back a step, and say first what we are doing when we opt for a 3-theory.

Then it’s a matter of further specification as we express the 2-theory, and then 1-theory (and even 0-theory). And perhaps the n-category story needs to come in about specifications being up to n-equivalence.

Posted by: David Corfield on February 6, 2021 8:56 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

The blurring of the notions of axiom and rule is already evident in FOL with the principles of double negation and excluded middle; whether one would regard it as as a rule or as an axiom depends upon whether one subscribes to constructivism or not.

Posted by: Madeleine Birchfield on February 4, 2021 4:26 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Were the actual talks recorded?

Posted by: Madeleine Birchfield on November 28, 2020 3:50 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Only one talk. And, no, it wasn’t recorded.

Posted by: David Corfield on November 28, 2020 2:16 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Jeffrey Ketland wrote:

It’s hard to see how one can come up with a mathematical concept more primordial/basic than xAx \in A

I think it just feels that way if you’ve been spending too much time in the category of sets, and not enough time in other categories. Morphisms feel more basic to me. Sometimes your category has a terminal object and you can talk about morphisms x:1Ax : 1 \to A. In categories like Grp or Vect, these morphisms are completely useless. But these morphisms, called ‘elements’, become quite interesting when your category has certain properties that made Lawvere call it a “category of space”. And in a well-pointed topos, these morphisms x:1Ax : 1 \to A become so powerful that you can become utterly enthralled by them, start writing xAx \in A, and try to build up everything based on that notion. But a well-pointed topos is a very special sort of place!

It’s sort of like how if you lived all your life in Paris you might think that a bidet is a very fundamental thing that every home should have… but then you go to the US and discover practically nobody has even heard of them.

Arguing about x:1Ax : 1 \to A versus xAx \in A seems very provincial to me, sort of like arguing about which side of the toilet the bidet should be on.

Posted by: John Baez on December 2, 2020 2:48 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

The cited paper by Lawvere is new to me, and is wonderful.

Posted by: jackjohnson on December 2, 2020 5:37 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

It’s not a claim it’s better somehow (I don’t think it is), but rather that it’s more primordial. The claim is that

xAx \in A

is a more primordial mathematical concept than

x:1Ax: 1 \longrightarrow A

is. For a set is a “bunch of things with a lasoo around it”. While a morphism x:1Ax : 1 \longrightarrow A is a bit hard to think about. After all, what’s 1? Well, it’s a set {blah}\{blah\}, containing something, we care not which. So I have a blah. I put a loop around it, to get {blah}\{ blah \}, a unit set. Then I consider functions from that unit set to AA, where A={a 1,a 2,}A = \{a_1, a_2, \dots\}. Aha! These functions are in one-to-one correspondence with a 1a_1, a 2a_2, \dots.

I think a similar point about “conceptual basicness” can be made with some examples of definitional equivalences. Peano arithmetic can be formulated in the usual first-order signature σ PA={0,S,+,}\sigma_{PA} = \{0,S,+,\cdot\}, and we give some axioms, but we’re thinking of the σ PA\sigma_{PA}-structure (,0,S,+,)(\mathbb{N}, 0, S, +, \cdot). But it can be also be equivalently formulated in a set theoretic signature, σ ={}\sigma_{\in} = \{\in\}, so that

(,0,S,+,)(\mathbb{N}, 0, S, +, \cdot) is definitionally equivalent to (, ack)(\mathbb{N}, \in_{ack})

It can also be formulated in an algebraic concatenation signature σ syntax={a,b,ϵ,*}\sigma_{syntax} = \{a, b, \epsilon, \ast\} (here a,ba, b stand for two atomic strings; ϵ\epsilon is the empty string; x*yx \ast y is the concatenation of x,yx, y), so that,

(,0,S,+,)(\mathbb{N}, 0, S, +, \cdot) is definitionally equivalent to (,a,b,ϵ,*)(\mathbb{N}, a, b, \epsilon, \ast)

At a highly abstract level, these are the same structure, dressed up differently – if you “morleyize” or “atomize” these three structures, the results are identical (a bit like having two extensionally different atlases which generate the same maximal atlas).

But the issue of what I called “conceptual basicness” is separate! When it comes to natural numbers, I have a strong intuition that 00, SS, ++ and \cdot are conceptually basic to the natural numbers. But the Ackermann encoding ack\in_{ack} over \mathbb{N} requires someone to write nn in binary notation, as a finite sequence and check the iith term. I don’t think the binary relation ack\in_{ack} ( 2\subseteq \mathbb{N}^2) is conceptually basic to the natural numbers. It’s a clever trick. And it tells us that the abstract structural features of (,0,S,+,)(\mathbb{N}, 0, S, +, \cdot) are precisely those of (, ack)(\mathbb{N}, \in_{ack}). But that doesn’t mean that the binary relation “the iith term of the binary expression for nn is 1” is conceptually basic (it’s called the BIT predicate in programming). When it comes to strings over an alphabet with two elements, then—although I can define ,0,S,\mathbb{N}, 0, S, \dots over that, using clever tricks—what’s conceptually basic to the strings is the atomic strings and the concatenation operation. I can indeed encode ,0,S,\mathbb{N}, 0, S, \dots into that theory, and treating those as basic, I can now define the original atomic strings and *\ast too by the inverse of this.

To get back to John Lennon. John \in Beatles. So, I definitely agree there is a (unique) morphism f John:{}Beatlesf_{John} : \{\bullet \} \to Beatles such that f John()=Johnf_{John}(\bullet) = John (though I need extensionality to conclude this). However, I really don’t think John is that morphism! And I can’t imagine trying to explain all this to a smart 11 year old. But I can easily explain “John \in Beatles”, by drawing a picture of the Beatles, with a lasoo around them.

Posted by: Jeffrey Ketland on December 2, 2020 8:52 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

I find it odd that “drawing a lasso” around something seems much more primordial than pointing at something with an arrow. I guess it’s a case of cowboys vs. Indians.

When push comes to shove, I don’t really care much about “primordiality”, or “conceptual basicness”, because I think it’s highly subjective. I don’t share your intuitions about it. I think those intuitions arise from thinking a lot more about sets than categories, and thinking about sets in a particular way. If you think a lot about categories, the concept of morphism starts seeming conceptually basic, and the concept of membership seems like a special case that’s only useful in limited cases.

I can think of membership as primordial; I learned how to think that way a long time ago. I also know how to think of morphisms as primordial. I learned that more recently, so it’s more interesting. I think it’s more interesting to try taking something new as basic and see where that goes, rather than stick to my original intuitions for my whole life and keep trying to argue for them.

Posted by: John Baez on December 4, 2020 5:48 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

“Lassos and Arrows: A History of the Debate about Mathematical Foundations in Set Theory and Category Theory”

would make a great title! (And I fixed my poor spelling).

Posted by: Jeffrey Ketland on December 4, 2020 4:09 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

David (I got sidetracked, but from your slides),

The case for the advantages of DTT over FOL can be made not only for advanced reasoning such as mathematics, but also for everyday reasoning.

Shouldn’t the comparison be with DTT and HOL? The set of theorems in FOL (for a fixed language) has no special abstract entities of any kind at all, whereas HOL and DTT have higher-order types.

There’s a nice performance reason (speed-up) for assuming higher-order axioms for logical reasoning, as an example given by Boolos in 1987 shows.

SOL is conservative over FOL, which means if there is a derivation D 1D_1 of a first-order sentence ϕθ\phi \to \theta using axioms and rules of SOL, then in fact a derivation D 2D_2 of ϕθ\phi \to \theta exists in FOL too. Boolos gave an example where ϕθ\phi \to \theta is derivable in SOL in about a page; but the shortest FOL derivation has size at least an exponential stack of 2s of height 64K.

Posted by: Jeffrey Ketland on December 2, 2020 11:26 PM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Fair enough.

We had a conversation on how to fit HOL into Mike’s schema, and it appears as (a class of) 2-theories in the same 3-theory as FOL.

Then we’d need to look for relative advantages of HOL and DTT in philosophy of language, etc.

Modal dependent type theories are flourishing (all tied up with Lawvere’s vision of adjointness in foundations, as in adjoint logic). How is modal HOL faring?

Posted by: David Corfield on December 3, 2020 8:44 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

If only to remind me, an article by Reinhard Muskens, Higher Order Modal Logic, for when my pile of marking is finished.

Posted by: David Corfield on December 3, 2020 11:37 AM | Permalink | Reply to this

Re: Dependent Type Theory as an n-Theory

Modality understood rather loosely, to mean anything that turns out to involve intensional operators like \square and \lozenge, along with some things (“states”, “worlds”, …) that are “evolving”, or “growing”, or “accessible” from one another, is an extremely big topic, and I can’t say I keep track of it all. There’s modal provability logic, Visser’s interpretability logic, modal set theory, fancy applications in tense logics and epistemic logics, Montague grammar/semantics, hybrid logics, Carnap/Church etc intensional logics (which these reach back to Frege’s syntax and semantics), model-theoretic and proof-theoretic connections between intuitionist logic and modal logic (going right back to a short neat paper by Godel in 1933), the modal logic of Hamkins’ multiverse, modal logic of end-extensions and forcing extensions and probably lots more I’ve not heard of!

Posted by: Jeffrey Ketland on December 4, 2020 1:14 AM | Permalink | Reply to this

Post a New Comment