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 UTCTrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3271
Found the link at nlab: https://ncatlab.org/davidcorfield/files/EvidSem2.pdf
Sorry. Fixed now.
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.
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.
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 (or or ) to mean and considering and to be operations on sets rather than merely 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.
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
more conceptually basic than
is?
On the second, we have a collection of things “with a lasoo around it” (Kripke’s phrase), and is inside the lasoo. On the first, I have no intuition at all about it. Eg,
(i)
(ii)
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 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 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, , etc), along with Comprehension, Induction and Extensionality for sets of numbers. But numbers aren’t “sets”. They’re atomic individuals.
The fact that ETCS defines to mean 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 and .) 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.
Right, but isn’t just conceptually very basic? Theories and 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 of atoms is isomorphic to ) of finite ordinals. I think that resolves “” etc. I.e., it’s false!
Did your SEAR system get published? (I did read it, but several years ago)
Mike posted on reasons to prefer the handling of elements by dependent type-theory over material and structural set theories back here.
Yes, I know. But Mike also mentions
In ZFC, the only things that exist are material-sets, so that in the proposition “” 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 . 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
So it doesn’t make much conceptual sense to introduce lots of fancy concepts (morphisms, domains, codomains, initial and terminal objects, etc.) and then define “” in those terms, say as
It’s doable, of course.
But still that seems conceptually upside down. The concept of 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
( a limit)
Then one obtains a growing structure which is conceptually extremely rich: , say, contains all structural possibilities for finitely many objects.
You said,
It’s hard to see how one can come up with a mathematical concept more primordial/basic than
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 . 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.
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.
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.
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.
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.)
I wonder if it is possible to rewrite dependent type theory as a theory of sets and families of sets.
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.
Jeff wrote
But I’ll repeat the original point…
which contrasts favourably with .
The reason I brought up Mike’s discussion of type theory is that it uses a third formation, namely, . This is not a proposition, such as , nor is it a function such as .
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.
Not sure if this comment was addressed to me or to Jeff.
To Jeff. We tend to avoid keep nesting, so we don’t get squeezed to the side.
Right, will put anything further down below!
If were a genuine quantifiable variable, we could treat “” as a proposition, i.e.: “ is of type ”. And, for example, say “not-()”! That is, the sine function isn’t of the type .
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.
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.
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.
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).
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.
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.
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.
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.
That’s correct, except that I would say they’re not in disguise at all. (-:
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.
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.”
This is argued for philosophers in Dimitris Tsementzis, What is a Higher-Level Set?.
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 and the existential quantifier was represented by . It wasn’t until the early 20th century that Peano invented for the existential quantifier and the 1930s when Gentzen invented 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.
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.
First-order logic is a type theory too, as I discussed last week in Oxford.
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.
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?
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.
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.
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).
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.
Whoops, wrong comment; this was supposed to be in reply to Mike Shulman’s comment above.
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.
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.
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.
Were the actual talks recorded?
Only one talk. And, no, it wasn’t recorded.
Jeffrey Ketland wrote:
It’s hard to see how one can come up with a mathematical concept more primordial/basic than
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 . 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 become so powerful that you can become utterly enthralled by them, start writing , 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 versus seems very provincial to me, sort of like arguing about which side of the toilet the bidet should be on.
The cited paper by Lawvere is new to me, and is wonderful.
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
is a more primordial mathematical concept than
is. For a set is a “bunch of things with a lasoo around it”. While a morphism is a bit hard to think about. After all, what’s 1? Well, it’s a set , containing something, we care not which. So I have a blah. I put a loop around it, to get , a unit set. Then I consider functions from that unit set to , where . Aha! These functions are in one-to-one correspondence with , , .
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 , and we give some axioms, but we’re thinking of the -structure . But it can be also be equivalently formulated in a set theoretic signature, , so that
is definitionally equivalent to
It can also be formulated in an algebraic concatenation signature (here stand for two atomic strings; is the empty string; is the concatenation of ), so that,
is definitionally equivalent to
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 , , and are conceptually basic to the natural numbers. But the Ackermann encoding over requires someone to write in binary notation, as a finite sequence and check the th term. I don’t think the binary relation () is conceptually basic to the natural numbers. It’s a clever trick. And it tells us that the abstract structural features of are precisely those of . But that doesn’t mean that the binary relation “the th term of the binary expression for 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 over that, using clever tricks—what’s conceptually basic to the strings is the atomic strings and the concatenation operation. I can indeed encode into that theory, and treating those as basic, I can now define the original atomic strings and too by the inverse of this.
To get back to John Lennon. John Beatles. So, I definitely agree there is a (unique) morphism such that (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 Beatles”, by drawing a picture of the Beatles, with a lasoo around them.
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.
“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).
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 of a first-order sentence using axioms and rules of SOL, then in fact a derivation of exists in FOL too. Boolos gave an example where 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.
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?
If only to remind me, an article by Reinhard Muskens, Higher Order Modal Logic, for when my pile of marking is finished.
Modality understood rather loosely, to mean anything that turns out to involve intensional operators like and , 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!
is it right? Dependent Type Theory (DTT) is a formal system used in the field of computer science and logic for specifying and verifying the correctness of programs and mathematical proofs. It is not typically referred to as an “n-Theory” in the same sense as other mathematical or theoretical frameworks like category theory or set theory. However, let’s explore the idea of considering DTT in the context of an “n-Theory.”
In category theory, there is a notion of an “n-category,” which generalizes the concept of a category. An n-category is a higher-dimensional generalization of a category, and it helps mathematicians and theorists study mathematical structures and relationships in a more abstract and flexible way.
If we were to draw an analogy between DTT and the concept of n-categories, we might consider DTT as a specific instance of a higher-dimensional theory, perhaps a 1-dimensional theory. In this analogy:
0-Theory: This would correspond to the most basic form of logic, where propositions and types are treated independently, similar to classical logic or simple type theory.
1-Theory: Dependent Type Theory itself. In DTT, types can depend on values, which allows for precise encoding of mathematical structures and reasoning about programs. You could view it as a 1-dimensional theory because it introduces a single level of dependency between values and types.
n-Theory: In a speculative sense, we might imagine the development of higher-dimensional type theories (n-Theory) where types can depend on other types, which, in turn, depend on values, and so on. This would be a more advanced and abstract extension of DTT. However, such theories would be highly complex and speculative, and I’m not aware of any established n-Theory for dependent types as of my last knowledge update in September 2021.
It’s important to note that the analogy between DTT and n-categories is a conceptual one and does not imply that DTT itself is inherently a part of any n-Theory. Dependent Type Theory remains a foundational framework for formalizing mathematics and programming languages, and its relationship to higher-dimensional theories is an area of ongoing research and exploration within the field of type theory and category theory.
Re: Dependent Type Theory as an n-Theory
It looks like your slide link is wrong.