Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In view of Urs’s contribution to the FOM list mentioned here, I suggested a ’Homotopy Type Theory as Foundational Language for Mathematics FAQ’ page, like string theory FAQ. I’m happy to contribute to it since there’s quite a literature already on what might possibly be meant by a foundation. But what’s the best title for this? I guess it depends on what we took to be its scope.
It could have as opening blurb the equivalent of
This page is to provide non-technical or maybe semi-technical discussion of the nature and role of the theory of fundamental physics known as string theory. For more technical details and further pointers see at string theory.
I find this an excellent idea. One would think we effectively created such an FAQ constituted by the relevant nLab pages, but just as in the case with the string theory FAQ, for complex topics where knowing “how to properly think about it” is important, people find it hard to connect this and an FAQ may help.
I need to focus on something else now. But maybe later tonight I find the leisure to start one or two entries.
I like the different tone of the string theory FAQ compared to the ordinary entry. Obviously we can take the ’Advantages’ at homotopy type theory and expand them. Anyway, I put in the preamble at homotopy type theory FAQ. We could open up to suggested questions at FOM and G+.
I think this is a nice idea. Please recall that there is also a (low traffic) designated HoTT wiki.
Of course, Bas means this wiki. The FAQ might be something worth having on the more visible and well-known main nLab, though; I’m not sure. It’ll be easier to have an opinion about that once I have some idea what will be on it…
It’ll be easier to have an opinion about that once I have some idea what will be on it…
For FAQs that’s easy, one just looks for questions that are being frequently asked. :-)
(The string theory FAQ grew from replies to questions which kept being asked on sites like PO. Each time I replied to a question which I knew had come up a bunch of times before, I created another item in that entry.)
Besides the vague one I hear a lot “What’s all the fuss about HoTT?”, we need
Is Univalent foundations limited to constructive mathematics?
and can draw on this.
But maybe first we need a policy for the page on when to use UF and when HoTT.
re the “proof challenge” I’ve added the following section to Wikipedia: Blakers–Massey theorem.
In 2013 a fairly short fully formal proof using homotopy type theory as a mathematical foundation and an Agda variant as a proof assistant was announced by Peter LeFanu Lumsdaine. It became theorem 8.10.2 of Homotopy Type Theory – Univalent Foundations of Mathematics[3]. The proof is generalized as to hold in any infinity topos.
Remember this is Wikipedia and anybody (no login required) who doesn’t like my wording or thinks I misstated something can fix it.
Thanks, this is an excellent idea.
The following points might be worth highlighting (I could do it tomorrow, not tonight, have to go offline in a minute):
that the BM-theorem in induces the BM-theorem in any -stack -topos follows, “externally”, simply by applying the classical theorem locally/stalkwise. This is what Charles Rezk has been saying for a long time.
But of course for various reasons it may be good to have an “internal” proof of this fact, and this is what Lumsdaine et al. claim to provide.
In particular, the traditional proof of the theorem in is actually not very direct and elegant. And people who looked into it in detail, notably again Charles Rezk, say it’s already a good accomplishment (which he tried to do but failed) to find a clean proof already in the classical case. Which is what the result in question would in particular imply.
On (1), surely that only works if your -topos has enough points?
Then it’s easy. But my impression was that the idea is that it also works by going like: for every object in the site there is a cover such that locally with respect to that cover, etc.
But I haven’t thought about how to make a detailed proof. It just seems to me that this is what Charles’s point is. Somebody with a spare minute should think about it.
Voevodsky suggested recently on the HoTT list that (if I understood him correctly) “univalent foundations” refer to the non-precise idea of a foundation for mathematics whose basic objects are homotopy types and which is invariant under equivalence, while “homotopy type theory” refer to the subject of homotopical interpretations of dependent type theory. Thus neither strictly includes the other: “homotopy type theory” includes both homotopical models of type theory constructed in a set-theoretic foundation, as well as mathematics done inside of type theory with enhancements such as univalence and HITs; the latter is one possible way to make “univalent foundations” precise, but in principle there might be others (though we don’t know of any yet).
Re #11:
That sounds more like working in the sheaf semantics of the internal logic, i.e. respelling the “internal” proof. It’s not at all clear to me in what sense this could be construed as applying the classical theorem locally.
Of course, that is not to say you can’t get theorems “for free” when you don’t have enough points. But then one has to work in more constrained fragments of logic where one has stronger classical completeness theorems.
back to the topic of this thread, I wrote what is by now a frequent answer to a frequent question: Does HoTT have models in infinity-toposes?.
I seem to have sketched a proof of Blakers-Massey in an -topos (using a model category formulation) as Prop. 8.16 of http://www.math.uiuc.edu/~rezk/homotopy-topos-sketch.pdf.
Ah, I see! So the trick is to use the fact that stackification on the one hand preserves connectivity, pushouts, and pullbacks, while on the other hand it is essentially surjective on diagrams. This is the same strategy used to prove that filtered colimits preserve finite limits in Grothendieck toposes.
Mike has sent a paragraph via g+ which I have taken the liberty to feed right away into the FAQ. Now at
I added a paragraph on What is HoTT? – For set theorists with reference to the interpretation of HoTT in set theory and vice versa.
The reason I put in the question about the proof of the fundamental group of the circle was that I remember (a) someone raising an eyebrow that this was a great achievement (like Poincare on Russell and Whitehead’s proof of 1+1=2 in Principia) and (b) Mike spoke eloquently about the achievement somewhere. I was going to copy in the latter, but can’t now find it. Anyone remember where it is?
@Bas #18
thanks! I have added a bit more glue, and something like a lead-in, and rearranged slightly to connect to the other paragraph there.
(Remember that this is an FAQ and that the item we are looking at it is supposed to give an answer to the question: “What is HoTT?”. )
Right now the item What is HoTT? – For set theorists reads as follows:
Homotopy type theory is a refinement of constructive set theory that takes fully seriously the constructive nature also of identity. (As with all constructive mathematics, with the relevant axioms added, this subsumes, rather than excludes, classical mathematics, see below at Is HoTT limited to constructive mathematics?.
It is this insistence on witnesses for identity and witnesses for identity of such witnesses, and so ever on, makes what in set theory are just sets (whose elements are either equal or not) instead be groupoids (whose elements may have non-trivial isomorphism between them) and indeed 2-groupoids (with isomorphisms between these isomorphisms) and so ever on; hence what makes what used to be just sets be what is kown as ∞-groupoids or homotopy types.
More technically, the 0-truncated types in HoTT (the “h-sets”)from a predicative topos, and even a topos if one allows the resizing axiom. When adding the axiom of choice to HoTT, one obtains a model of ETCS. The iterative notion of set can also be captured. Aczel’s sets-as-trees interpretation gives a model of constructive set theory CZF. Again by adding choice to HoTT, one obtains a model of ZFC; see Ch10 of the HoTT book.
Conversely HoTT has models in ZFC (+a number of Grothendieck universes to model the type theoretic universes), namely in structures called (∞,1)-toposes which are presented by presheaves of simplicial sets.
The nature and role of these higher toposes in HoTT is to be understood by analogy with the familar forcing models: When one proves something in ZF, it is automatically also true in all forcing extensions. The same is true for constructive set theory, except that there are more forcing extensions since we don’t have to force the law of excluded middle; those constructive notions of forcing (which also subsume permutation models) are called “sites” and their models are called “1-toposes”. Now in HoTT we have an even more general sort of forcing appropriate for homotopy theory, called (∞,1)-sites, whose models are called (∞,1)-toposes.
By the way, presently CZF redirects to ZFC. (!) I suppose this needs to be changed. Notice that there is (only) a stub constructive set theory. Some expert might want to take care of this.
I made some changes and added some links. Meanwhile, I found out that there is quite a bit of material at ZFC, including a comparison of the axioms. I am not sure whether all of this stuff should be move.
BTW: Is there a reason for not automatically including redirects for capitalizations and plurals ?
@Urs #21 Probably you meant CZF (?)
Fixed, thanks.
Fixed, thanks.
CZF redirected to ZFC because is discussed (with a definition and a bit of historical context) at ZFC, a page which discusses many many variations on , of which is one.
In contrast, is not even defined at constructive set theory (and there is less historical context), so I'm not happy about redirecting it there. Obviously the definition could be added, but there was a good reason for having them all together: for purposes of comparison. I certainly don't like having them separated without at least copying over the relevant information.
The issue is compounded because ‘constructive set theory’ is the name of a specific set theory that is not even mentioned at constructive set theory, but it is mentioned (and defined, and a bit of historical context given) at ZFC. So currently anybody linking to constructive set theory is going to exactly the wrong place.
There is certainly a problem with ZFC as it is: the beginning of the article doesn't reflect its contents well. This is because it grew out of an article that was much more limited, and the Idea section was never updated. I would rather update the Idea section (and perhaps the name) so that people landing there from CZF will realize that they indeed came to the correct place. Then if we really want to separate out a new article specifically on constructive versions, OK, but then at least we know what we're starting with (and can make sure that it all gets copied over as needed).
Toby, my apologies. I started to “fix” the redirection that Urs mentioned and then saw what you wrote there. I’ve currently solved it by putting links in two directions, but I am aware this is not perfect.
You might well be right that keeping all of set theory together on one page (and updating the Ideas section) is the best solution.
I’ve added a paragraph at ‘why HoTT is preferable to set theory’. It’s far from perfect, but perhaps it is something to start from.
Maybe the page ZFC should be renamed to something like “Zermelo-Frankel-style set theory”?
Thanks, Toby. But then something needs to be done in any case, so that people who follow some link don’t get the impression that they are being sent to the wrong place. Could you think of some way of improving on the situation?
I've fixed the introduction to ZFC.
We have several other articles (linked to from ZFC) on variations of : NBG, Morse-Kelley set theory, and ZFA. We could make constructive set theory an article along the same lines for , or have pages for and/or .
Or we could have a page that does what constructive set theory currently does, which is to cover constructive variations of . I would not want to have it at that title, for a couple of reasons:
In any case, there is still more coverage of this at ZFC.
What ZFC really needs is a table listing, for each theory with a name and each of the 10 axioms listed, whether than axiom appears in that theory (and if so which version). I would find that useful! The information is already on the page, it just needs to be organized into that form.
I am inclined to call the page on ZFC set theory, or perhaps material set theory. Constructive set theory no longer refers to Myhill’s system: e.g. the book “Notes on Constructive Set theory” is mostly about CZF. setoid->history should probably be remove and redirected to Bishop set and this could be referenced in constructive set theory. There is also set which contains h-sets.
Thanks for looking into this!
(As a tiny edit, I have just re-ordered the very first sentence at ZFC.)
We do already have a page material set theory, with not much there.
I found the clustering of search results in Carrot somewhat useful/assuming. It would be nice to see what kind of information we can get out of the treasure trove that the nlab has become.
prompted by this request on the HoTT mailing list, I started adding something under What role does the univalence axiom play?
Added something under Why should I care? For homotopy theorists.
(This is the question about HoTT that I have heard most frequently. Typically in a sneering manner.)
Nice, thanks!
Material set theory includes Zermelo-style, but it also includes other things like New Foundations. Certain people like to speak of ‘the iterative conception of set’; that's what Zermelo & Fraenkel axiomatized.
‘the iterative conception of set’; that’s what Zermelo & Fraenkel axiomatized.
Doesn’t Material set theory say that every element of a set is encoded as an unordered tree of sets in which the leaves are the empty set? (non well founded versions such as New Foundations may have infinite trees and no leaves and one can imagine versions where trees are replaced with things that are cyclic).
Two elements are equal if they are the same tree. The elements of a set must be tree structures though often they can be arbitrary and most times mathematicians don’t bother choosing particular structures. (and this notion of equality says that the encoding really isn’t a tree but is instead a rooted DAG with possibly shared equal substructures)
The only case I can think of where the tree structure does matter is in various ways of encoding the natural numbers which allow an order relation, , to be derived from the trees.
Are there any other examples where something useful can be derived from the tree structure? Sure, ordered pairs can be encoded in various ways as trees but does that have any advantage other than providing some way to unpack them.
Should something along these lines be added to material set theory?
I thought that the “iterative conception of set” was formalized by the axiom of foundation. It’s not clear to me that the difference between ZF-without-foundation and NF has anything to do with iterativity.
I have added to homotopy type theory FAQ a section
This is trying to express the observation that type theory is “more foundational” than set theory in that it is rather on the same “foundational level” as first-order logic. In addition this is trying to highlight that, in this vein, homotopy type theory is, in turn, “more foundational” than (extensive) type theory, since it removes an axiom (uniqueness of identity).
Check out what I wrote. This may need fine-tuning. Please feel invited to edit.
(This is prompted by further discussion on the FOM list and behind the scenes. It seems many people reading there have a strong interest in a deductive system being “very foundational” but at the same time have no good idea of how type theory is “more foundational”, many of them seem to think of type theory as some exotic baroque variant of standard foundations, reversing the actual state of affairs)
You make a good point about type theory supporting FOL (so also Ch3 of the book). However, this seems quite crude, and I am not entirely sure where to start. Perhaps what you wrote will upset people more than convince them. A clear technical remark is that we need to add inductive types to get any kind of interesting set theory. So we should compare type theory + inductive types with FOL+set theory. The work of Aczel on type theory vs set theory is relevant here. Type theory may be considered “more foundational” due to the meaning explanations. However, these are currently missing for univalent type theory, so one needs to be careful. Some preliminary work is here. SEP has a small part on univalent foundations and on the relation between sets and types.
All right, thanks for the feedback.
First of all I have added more pointers. Where FOL in type theory is mentioned I added
(details are here)
and where sets as h-sets are mentioned I added
(details are here)
Incidentally, that points to a list including articles you wrote and supervised which have “sets in homotopy type theory” in their titles without adding “with inductive types”. Since it is understood. But I did add mentioning of and pointer to inductive types now to the discussion in the FAQ.
The article by Aczel that you point me to seems to be more about semantics of MLTT in set theory, than about set theory inside type theory. No?
Regarding “meaning explanation”: if I understand well this is in the vein of arguing that the rules of type theory are “right” from “pre-mathematical common sense”. Is there a document which would lay this out in a more pronounced way? I am not sure if the slides you are pointing me to would be of much help to a non-specialist reader that would be the audience of the FAQ. But let me know if I am missing your point.
Finally regarding your “I am not entirely sure where to start”: let’s just go through the text; what is the first line that makes you cringe?
I think the beginning is good, but it gets a little misleading later. “First order logic is recovered inside type theory as the sub-system of those types which have unique terms” is usually true for how we do logic in HoTT, but it’s not true for type theory in general; plenty of type theorists use any type as a proposition.
And while I think I see what you’re trying to say with “one obtains first-order logic from type theory by adding an axiom, namely that all types are propositions”, I don’t think it’s quite right. It would be more faithful to the usual presentations to say that one obtains first-order logic from type theory by removing information, namely the terms which inhabit types, turning the judgment “” into the judgment “ is true”.
Bas also has a good point about inductive types. Furthermore, in HoTT we also usually add the univalence axiom (and its consequence of function extensionality) to bare intensional type theory. So maybe the “layers of foundations” diagram should start with intensional type theory at the bottom below extensional type theory where you currently have “homotopy type theory”, and then add a few branches. Instead of going up from extensional type theory to FOL and set theory, one could instead add inductive types and get to an extensional type-theoretic foundation for math. And instead of going up from intensional type theory to extensional type theory, one could add HITs and univalence and get to HoTT.
I would suggest not mentioning the “meaning explanation” in anything aimed at set theorists; it seems to me that only a certain sort of constructivist can see it as “explaining” anything. (-:
Thanks.
“First order logic is recovered inside type theory as the sub-system of those types which have unique terms” is usually true for how we do logic in HoTT, but it’s not true for type theory in general; plenty of type theorists use any type as a proposition.
Okay, sure, I have made it read “homotopy type theory” in this paragraph.
I’d rather not, in this section, go into all the flavors of type theories and how they branch off, that might be a topic for another subsection of the FAQ. I think it makes sense here to display a hierarchy with HoTT and nothing but HoTT at the bottom and how that iteratively restricts to subsystems.
It seems to me that the perspective is that adding univalence to intensional type theory “fixes” intensional type theory and for the first time gives a truly satisfactory type theory foundations, even apart from the homotopy-theoretic aspect. Therefore at this point in the FAQ all historical variants are distractions. This section “Why should I care? For foundationalists” in not supposed to explain type theory, but to explain in which sense HoTT is “more foundational” than set theory.
And while I think I see what you’re trying to say with “one obtains first-order logic from type theory by adding an axiom, namely that all types are propositions”, I don’t think it’s quite right. It would be more faithful to the usual presentations to say that one obtains first-order logic from type theory by removing information, namely the terms which inhabit types, turning the judgment “a:A” into the judgment “A is true”.
That sounds like making a distinction between the Prop-subuniverse and the reflection into it. Is that a distinction worthwhile at this point in an FAQ?
…add a few branches. Instead of going up from extensional type theory to FOL and set theory, one could instead add inductive types and get to an extensional type-theoretic foundation for math.
Let’s see, except for the branching, this seems to be what I have in the entry. First there is “going up from extensional type theory to FOL and set theory” and then the next (the second) diagram is “add inductive types and get to an extensional type-theoretic foundation for math.”
I’d think. Of course if it’s not coming across this way, I need to change it. I am prepared to change it, but maybe I need more input.
I don’t know what “foundationalists” are, I guess you are targeting formalists/platonists. This is fine, but could be clearer.
Also, “more foundational” is not an established notion, and feel rather informal to me. There are technical notions such as interpretability of one logic into another, or proof theoretic strength. Perhaps, if you just emphasize that “more foundational” is meant to be colloquial, I’d be happier.
type theory is even a little more foundational than first-order logic.
For this one has to buy into Curry-Howard, don’t you think. Type theory is a calculus for predicate logic may be more precise. Adding Id types one obtains a calculus for predicate logic with equality.
homotopy type theory also offers the following more immediate route to sets
… to structural set theory ?
Perhaps, if you just emphasize that “more foundational” is meant to be colloquial, I’d be happier.
Okay, in this sentence
For instance a foundational system B might be obtained from foundational system A by adding axioms, or by enriching the logical framework, and then A could be regarded “more foundational” than B, as then A in fact serves as foundation for B.
I have changed “would be called” to “could be regarded”.
But this must be a standard concept. Is “proof theoretic strength” the right word here? Maybe the better term here is “fragment”?
type theory is even a little more foundational than first-order logic.
For this one has to buy into Curry-Howard, don’t you think.
That’s mentioned just a few words before what you quote. Does it need more highlighting?
homotopy type theory also offers the following more immediate route to sets
… to structural set theory ?
Okay, I have added “structural” with a link again.
type theory is even a little more foundational than first-order logic
Propositions as types gives you a form of choice that is not part of FOL. Set theorists may object to this being a subpart of FOL. HoTT gives you one way of capturing FOL+sets, but there may be others and set theorists may object to this.
If we get this clearer, I think it could be a good explanation.
Propositions as types gives you a form of choice that is not part of FOL.
You must be thinking of using untruncated types as propositions, right? In the FAQ text I am talking about (-1)-truncated types as propositions. I am now adding a half-sentence to make this yet more explicit.
Sorry to be persistent, but type theory is not a “fragment” (in the sense of having fewer axioms) of FOL. There is no notion of “type” in FOL. As Mike says, you seem to be thinking of the “logical reflection” (terminology?) of type theory. However, even the restriction to brackets types gives unique choice which is not part of FOL (with equality).
Since set theorists allow unique choice they may not care, but people in reverse math (Friedman) may.
I agree with Mike that a tree may better represent the state of affairs than the linear order you have now.
I tried “fragment” as an improvement on the suggestion “proof theoretic strength”, which seemed wrong to me (but let me know if I am missing something).
Let’s change the mode of proceeding here. Instead of me guessing which exact terminology you prefer, you should just say it directly.
Mike said it here before:
By contrast, type theory is not built on top of first-order logic; it does not require the imposing superstructure of connectives, quantifiers, and inference to be built up before we start to state axioms. Of course, type theory has first-order logic, which is a necessity for doing mathematics. But first-order logic in type theory is just a special case of the type-forming rules. A proposition is merely a certain type; to prove it is to exhibit an element of that type. When applied to types that are propositions, the type-forming operations of cartesian product, disjoint union, and function types reduce to the logical connectives of conjunction, disjunction, and implication; the quantifiers arise similarly from dependent sums and products. Thus, type theory is not an alternative to set theory built on the same “sub-foundations”; instead it has re-excavated those sub-foundations and incorporated them into the foundational theory itself. So not only is it more faithful to mathematical practice than either kind of set theory, it is literally simpler as well.
I don’t want to be a pain, but now I grew curious and searched a bit. Asking Google for “first-order fragement” produces plenty of hits.
In particular there is this thesis
which considers pretty much what we are talking about here and speaks of the “first-order fragment” of Coq when bracketing types to propositions (first on p. iv).
I am aware that there are a thousand little details in this business, and that no writeup is fully compatible with any other. But for the sake of communication and trusting the common sense of the reader, I am getting the impression that saying that “FOL is a fragment of HoTT” should not be illegal.
I think perhaps part of the confusion here comes from the distinction between “type theory” as a subject and “type theory” as a particular formal system. Type theory as a subject can, I think, be honestly said to be more foundational than set theory, because FOL is naturally presented as a type theory. However, that type theory is not the same as the type theory that we enhance with univalence and HITs to get HoTT. I do not think it is correct to say that HoTT is at the “bottom” in any sense, although one can maybe argue that it’s “closer to the bottom”. Notice that in the paragraph of mine you just quoted I said “re-excavated the sub-foundations”, i.e. it is not built on, or identical to, the sub-foundation underlying set theory.
I like the way Mike phrased it!
Dimitri Hendriks was talking about Coq with Prop and Set separated. In particular, we do not have unique choice in Prop, hence there is a better claim that it is in fact a subsystem/fragment.
FWIW, I also don’t think it’s a good idea to try to sell people on HoTT by telling them that it’s “more foundational” than set theory. As has been pointed out, there’s no accepted definition of what that means, and it might or might not be true. Moreover, as you well know, it’s not really the point. What I think we should say, and can be defended, is that HoTT is at least as foundational as set theory. And once we have that out of the way, then we can move on to the actual advantages of HoTT.
Believe it or not, but I don’t get what the complaint is. But I have removed the whole section now.
HoTT is at least as foundational as set theory
The problem with that, at least with the fom crowd, and they’ve already said it, is they turn that around and say ’ah, so it’s not more foundational than set theory, so we might as well use set theory, since we know so much about that’. I don’t have a solution to this, other that what Urs is trying to do: point people to the facts, and let the mathematics itself sort things out.
By the way, I am not after selling anything to anyone. I am not a salesperson.
I think we all know that what I said here and removed now is just true. But if it takes a lot of effort to find politically correct ways of saying it, then I am fine with keeping it an esoteric secret. Maybe that’s more fun, anyway.
@Urs: I thought we were objecting to parts of it that we didn’t think were true.
@David: If someone doesn’t want to listen, or if they have their priorities wrong, then I figure that’s their problem; we shouldn’t bend the truth to make it more appealing to them.
@Mike,
I’m just not up to playing their game. I don’t mind saying these things here, but there is a reason I’m not in the discussion anymore. Perhaps Urs was not going to point people on fom to the FAQ page, and I’m just overly cautious of giving fuel to a fire.
@David, I agree with you. I’m doing my best to ignore this whole fooferaw, and being very glad that I decided never to read fom.
Re 60: Like Mike, I was also reacting to the parts that I did not think were quite right.
I don’t understand what you are disagreeing with, I don’t see how the corrections you propose are different from what I said.
On my end I receive that Bas is disagreeing with the statement that there is FOL inside HoTT and Mike is telling me that the right word is that HoTT “excavates” FOL. I can’t believe you actually mean this, and so I believe something really weird is going on in the conversation. It’s a pity, because the point I made is really neat, and I know you both know this, nonwithstanding the difference between excavating or fragmenting.
This here not to continue the discussion, I have no further energy for it. Just to let you know that I don’t understand where you think you are disagreeing with the evident points I made.
I really just came back here because I made another edit to another part of the entry, and need to announce it here, to stick to the rules. Will do that in the next comment.
Slightly expanded the text under Is homotopy type theory limited to constructive mathematics?
Re 64: Urs, sorry for being (overly) critical. The point I was making is that FOL is not really a fragment of HoTT in a precise sense. Of course, it is in a slightly looser sense. That’s why I liked Mike’s “re-excavates” (also because I learned a new word). I think what you wrote is actually quite good, but your target audience will be more critical than I am.
So, if we put in Mike’s text and add the observation on inductive types and the tree Mike mentioned, I think it would be good to put it back in.
Speaking of excavating, I am excavating Mike #41 here:
I thought that the “iterative conception of set” was formalized by the axiom of foundation. It’s not clear to me that the difference between ZF-without-foundation and NF has anything to do with iterativity.
I think that this is a mistake.
To take an analogy, Robinson arithmetic, like Peano arithmetic, treats natural numbers iteratively, as built from zero using the successor operation. It lacks induction, which is important, so there are many facts about natural numbers that it cannot prove (and the same goes for Peano arithmetic, for that matter, just less so), but it’s still about the same kind of numbers. The axiom of induction should be there, to close off the universe, but we already had the iterative conception of natural numbers; we just want to say that there aren’t any more. (By the way, Wikipedia refers to Robinson arithmetic as a ‘fragment’ of Peano arithmetic, which supports a broad usage of that term.)
Similarly, , like , treats sets as built from the empty set with a limited repertoire of constructions. This contrasts with the anything-goes approach of Frege, in which any predicate with a free variable defines a set. The axiom of separation is questionable from this perspective; you justify it by saying that the new set is smaller than one already constructed. (To me, that’s cheating, but people used to Cantor’s linear hierarchy of sizes are easily fooled in this respect. Restricting to bounded separation —giving a theory equivalent in strength to — is the non-cheating version.) The axiom of foundation is like the axiom of induction (indeed, it is an axiom of induction): it should be there, for the same reasons, which is why the founders all eventually accepted it; but they didn’t think of it at first, and they didn’t change their conception of set when they adopted it.
I don’t see how it’s justified to say that “treats sets as built from the empty set with a limited repertoire of constructions” when it is consistent with various anti-foundation axioms in which that is not true. I’m happy to accept that the founders of set theory had the iterative conception in mind when formulating , but I don’t see how that conception is formalized by anything in ; merely asserts that sets admit certain operations, not that they are generated by those operations.
Can you comment on the analogy with Robinson arithmetic? Does Robinson arithmetic not formalize a conception of natural numbers in which they are built from zero using the successor operation? I would prefer to say that Robinson arithmetic does formalize this conception, but incompletely, because it includes the introduction rules but not the elimination rule. The same is true of .
Since you write
I’m happy to accept that the founders of set theory had the iterative conception in mind when formulating
we are probably not really disagreeing on much. I just want to say that formalized what they had in mind (the iterative conception of set), but the formalization was incomplete, and then they fixed that a few years later. Whereas you want to say, if I understand you, that even if it was supposed to formalize what they had in mind, it didn't actually do that job until it was fixed. Which is not much different.
Yes, we’re probably not disagreeing on much if anything. I see your point that and Robinson arithmetic “partially” formalize their respective iterative conceptions by including the intros but not the elims.
Every now and then,when I get a chance, I am checking with an expert on what the politically correct way is to say that FOL is part of type theory.
Some kind soul points me to Barendregt 91,which I assume you all know well. In its section 4 this discusses how the L-cube of intuitionistic logics includes into the Lambda-cube of type theories, under propositions-as-types.
Right before 4.1 it says that for all 8 corners the inclusions are sound, and that for propositional and for predicate logic it is also complete.
I am inclined to add that statement to the homotopy type theory FAQ at the point where I previously removed (rev 20) the paragraphs that meant to say this.
[ edit: have added a brief paragraph here ]
first order logic maps soundly and completely into type theory
Does this mean typed (many sorted) first order logic? Or does one just thing of a single given domain type ?
1 to 73 of 73