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.
I noticed that there was a neglected stub entry universe that failed to link to the fairly detailed (though left in an unpolished state full of forgotten discussions) Grothendieck universe.
I renamed the former to universe > history and made “universe” redirect to “Grothendieck universe”
I don’t agree with this. Not every universe (as a place that mathematics takes place in) is a Grothendieck universe. Indeed, most of the examples at universe are not Grothendieck universes. Even the ones which are are large categories, whereas tje point of the existence of a Grothendieck universe is that it is supposed to be small.
I have moved it back, while mentioning Grothendieck universes on it.
I have not encountered the use of “universe” to mean “a category in which mathematics takes place.” The only uses of “universe” in mathematics that I can think of are Grothendieck’s in set theory and Martin-Lof’s in type theory. Do you have some references for this usage, or are we proposing to introduce it?
I’m not sure. It looks like I wrote that page, but now I don’t know why. (I posted a message about its creation at 2009 August changes, but I no longer understand it.) It does look as if most of the links there could go to Grothendieck universe; some seem to be a little more vague.
There is a comment at Grothendieck universe that I made:
Maybe we should reserve this page for the strict notion in material set theory and make another page, say universe, for the non-evil concept. Then most (if not all) links here would really want to go there.
You (Mike) seemed to endorse that, but we didn’t do anything with it. I could rewrite universe along those lines, mentioning more general ideas but keeping the focus on size issues.
I still agree that it would be better for the page called Grothendieck universe to be mainly about the material notion, though with easy-to-find links to the structural version (I forgot about the existence of universe in a topos in my last comment) and perhaps to the type-theoretic version (which I don’t think we have a page about, do we?). So it might make sense for universe to perform both a disambiguation function between all three of these, and also include a less specific/precise discussion of the general idea of how universes of all sorts are used to deal with size issues. I suspect that most places on the lab which link to [[universe]] will be using the notion in a way which would work equally well in any choice of foundations, with the appropriate notion of universe.
I am a bit confused by Toby’s use of “universe” as “a category inside of which we do math”. My understanding is that on the contrary, a “universe” is an object inside the ambient category inside of which we do math.
So here is a would-be creation story for doing math:
we start with assuming that we all understand ETCS and its naive definition of .
insider we pick a universe in a topos-oject .
(and then we know an object of is -small if it is isomorphic to a fiber of , otherwise it is -large)
Maybe it feels like here is “more of a universe than ”, but that’s not the way the terminology is used.
Toby? I am inclined to edit universe following Mike’s suggestion
So it might make sense for universe to perform both a disambiguation function between all three of these, and also include a less specific/precise discussion of the general idea of how universes of all sorts are used to deal with size issues.
and make your material there some kind of subsection.
I’m inclined to completely rewrite it in line with Mike’s suggestion, actually.
The confusion here is the usual one of reflection: we take something that was large and posit that there exists a small equivalent. and are both places in which mathematics takes place, and in fact they are supposed to be the same kind of place. So they are both universes in the naïve sense of the word, and you can find uses of the word in such a general way on the Lab (I forget where, but in backlinks from universe).
Anyway, you can edit the article if you want, Urs, but I will rewrite it if you don’t and say more about this.
in fact they are supposed to be the same kind of place
Methinks the difference is that is designed to look like as much as possible, but is different in that it is the ultimate ambient context.
As far as I understand, the difference is drastic: is not even fully formally defined. It is a kind of a priori that we take as given by grace (at least if we follow ETCS). Once we have it, we do formal axiomatic math inside it. But itself is not subject to formal math. It is a “naive” pre-axiomatic notion that we agree to all accept.
If somebody does not believe a statement about , there is no way to prove it to him or her. If somebody however accepts and then does not believe a statement about inside it, there is a way to prove or disprove it.
That’s at least how I understand it.
How about von Neumann universe ? It is not a Grothendieck universe nor is an object in something as it is a proper class. The usage of the term predates Grothendieck, I suppose.
@Zoran: Yes, that’s right, there’s another notion of universe.
@Urs: I disagree that SET is not fully defined; insofar as it “exists,” it’s defined as a model of some particular first-order theory, and it satisfies some axioms, which you could use to prove something about it to someone. They may not believe that an object exists satisfying those axioms, or they might not want to call an object satisfying those axioms “SET,” but that’s no different from a Grothendieck universe, since someone just as well might not believe that such a thing exists or want to call it a “universe.” I would say rather that the difference is that U is an element of the first-order model SET, whereas SET is the model itself (although it might in theory be taken to be an element of some still larger model, etc.).
it’s defined as a model of some particular first-order theory,
Can we say “model” before we have said ?
My understanding was that we need to say that has a “collection” of objects, before we have set up to formalize what “collection” is supposed to mean. So we need to fall back to a naive pre-axiomatic notion of “collection” and assume that we all know what it means to say that has a “collection of objects”.
For if we tried to formalize this, we’d be going in circles. No?
A collection is very much weaker than a notion of set, in that it doesn’t really have any ’build new collections from old’ rules. In the formulation at fully formal ETCS, which take the 1-sorted path of defining a category, the only rules imposed on the collection which make it a model of ETCS are the statements that make it a well-pointed topos with choice and an NNO. The axioms don’t tell you about anything you can do with the collection itself, only the elements of the collection, so in a sense collections satisfy no axioms (or only very weak ones like equality)
I suppose it’s the same in material set theory. I’ve seen people start theorem with ’Assume a model of ZFC exists ….’, because they have to assume that some collection of sets exist.
In traditional approach to logics, one needs to have sets of formal symbols to do logics, nothing else. Everything else is in formal manipulations with sequences of symbols. Now for doing model theory you assume one weak axiomatics of set theory to form models of a stronger axiomatics which is equiconsistent with it. But this story is done within formal manipulations on the basis of assumed axioms. No additional “naive” story is needed than the one needed for manipulation of logics plus axioms of the weaker axiomatics which give models of stronger axiomatics. I think that the only part which should be called “collections” here is the stuff about collections of symbols to establish logical computations. The part about axiomatics of set theory needed to model stronger set theories, is just a sample theory, and it is purely formal, no “naive” notions needed to proceed, once we can do symbolic manipulations.
Okay, so is the full process as follows:
start with a naive/pre-axiomatic notion of collection and of first-order theory and of model of a theory .
then formalize as a model for a 1st order theory in that context;
and then define a universe object in .
?
I am mostly interested in seeing some expert admit that we need to start somewhere with a naive/pre-axiomatic notion that is not itself further formalized.
Why you talk that dramatically ? Every intro book on logics dwells on these issues of metalanguage and language; the lowest (or highest if you like) level being “informal”. The formal language consists of symbols and they form collections; one can say that those do not obey axioms, but one can always go one level further in metalanguage and assume some weak axioms on those, where those axioms will be prescribed in language one level below. This is convenient as one sometimes likes to have axiomatic systems with infinitary languages; their usually interesting properties rarely depend on some rich axiomatics. But rules of inference are anyway just a game as long as we talk about finite part of it. So what I would disagree with your scheme is that what you call level 1 must already be the bottom metalanguage. Often that level is already modelled in some weaker set theory, where we sometimes already play things like Peano axioms and use mathematical induction for example for playing with an infinitary language. The informal level is one level below.
In that sense in which you talk on primitive collections as needed, Joyal asserted once that one can not talk about category theory in elementary way not preceded by some primitive form of set theory needed for proofs about elementary approach to categories. Thus one can not establish set theory from category theory without any set theory. For some reason when Joyal said that Toby disagreed with him in the discussion. But I think it was a misunderstanding: Joyal did not mean fully fledged “set theory”, but some very weak part needed to do proofs to set the stage.
I think that first order logic fits into your 1. at some point, Urs, which is really just a way of talking about the symbols used and how to manipulate them. I agree that there is a preaxiomatic step, certainly involving ’a collection’, but I’m not sure about ’first order theory’ - this is fairly well established I believe. From Wikipedia:
For every natural mathematical structure there is a signature listing the constants, functions, and relations of the theory together with their valences, so that the object is naturally a -structure. Given a signature there is a unique first-order language that can be used to capture the first-order expressible facts about the -structure.
it goes on to say that a theory can be specified as
List or describe a set of sentences in the language , called the axioms of the theory.
and another way, which I will not describe. The use of the word ’set’ is unfortunate, because it is not needed in full strength for the exercise. ETCS is finitely axiomatisable, and has a finite signature, and so as a first order theory is expressed in finite language, which is a lot less strenuous than axiom schemas as in ZFC. A finite language with a finite number of axioms is pretty much formal. This is something basic, which I suppose could go into your 1. as ’first order logic’.
The existence of a model of a theory is I suppose something that is hard to pin down (for me at least). Once one assumes the preaxiomatic notion of ’collection’, then how does one say that given a collection it is a model? More knowledgeable people than I will have an answer here I’m sure.
The short answer (and I’m not an expert) is yes, there is a step which is naive and preaxiomatic, but what it deals with is a lot, lot weaker than the next step, as Zoran says. The strongest assumption is the existence of a model of ETCS, and after that everything is automatic.
It’s questionable to me that there is anything “preaxiomatic” in mathematics. It seems to me that at the root of everything is a manipulation of symbols, e.g. the syntax of first-order logic in a logical theory such as ETCS. We usually like to interpret that manipulation of symbols as being “about” a “model” of the theory, but we can’t actually “have” a model of any theory until we have a model of some metatheory in which to build it, so if we insist on reducing everything to the end we don’t “have” a model of anything at all. Nevertheless, when we speak in the language (syntax) of some ambient theory, we can talk about having a model of some other theory, which is what people do in model theory. This is what I was trying to get at with the caveat “insofar as it ’exists’”, but I wasn’t very clear.
Going back to the original #8, if ETCS is our basis foundational theory, then there is really no such thing as “a statement about SET” because at root there is no “SET,” rather there are only statements in the language of ETCS—which we nevertheless frequently think of (and speak of) as referring to some “model” of it that we call “SET.” Any statement of this sort has the potential to be proven or disproven from the axioms of ETCS (although of course by the Incompleteness theorem, there will always be statements which can neither be proven or disproven).
@David #16, I don’t really think the axiom schemas in ZFC (or other equiconsistent theory, like SEAR) are really any more of a problem, ontologically, than the finite axioms of ETCS, because they are computably enumerable.
It’s questionable to me that there is anything “preaxiomatic” in mathematics. It seems to me that at the root of everything is a manipulation of symbols, e.g. the syntax of first-order logic in a logical theory such as ETCS.
What is “manipulation of symbols”, what is “syntax”, what is “first-order logic”, what is a “logical theory”? For at least some of this you have to assume that I know what you mean without you having to give me the axioms for it.
We usually like to interpret that manipulation of symbols as being “about” a “model” of the theory, but we can’t actually “have” a model of any theory until we have a model of some metatheory in which to build it, so if we insist on reducing everything to the end we don’t “have” a model of anything at all. Nevertheless, when we speak in the language (syntax) of some ambient theory, we can talk about having a model of some other theory, which is what people do in model theory. This is what I was trying to get at with the caveat “insofar as it ’exists’”, but I wasn’t very clear.
Okay, so then we take model theory to be the basis of it all?
Let me try again to deduce the creation story for mathematics:
we assume that it is clear what it means to speak in the language (syntax) of some ambient theory and fix one;
in terms of that ambient theory we formulate the theory called ETCS, including the axiom of universes
using that axiom we consider a universe object
and so forth.
How does that sound?
Eventually I would enjoy an nLab page with a good version of what I am trying to find here. (Well, we are still trying to figure out how universe has to be rewritten.)
What is “manipulation of symbols”, what is “syntax”, what is “first-order logic”, what is a “logical theory”? For at least some of this you have to assume that I know what you mean without you having to give me the axioms for it.
I refrained from saying it before, but I can’t now: this is very Wittgensteinian (at least, Tractatus Wittgenstein). We could treat working with ETCS, as Mike says, as a formal game manipulating symbols on a piece of paper according to the rules of formal logic and the axioms of ETCS, but then one might object to this.
I would perhaps put it like this:
It is in step 2. that the naive idea of ’collection’ comes into it, in that we can pretend we have a bunch of things that the symbols of ETCS represent, and that they obey the rules of ETCS, but this is not strictly necessary; we can just manipulate the symbols. Maybe this is little circular, in that the model of ETCS is a symbol guaranteed to exist and behave in a certain way, but if, inside the rules of the system, it smells like Set, looks like Set, moves like Set, then I suppose it is Set.
@ Urs #8:
That’s at least how I understand it.
I guess that this is one way to look at it. But it seems very limited to me.
On person’s is another person’s . For example, if is a topos, then you might think of as . Whereas, if is a small topos, then you might think of as . But a small topos is a topos, so you can also think of as . Only it’s a more restricted kind of now, which may or may not have yet another topos inside of it.
Going the other direction, if is a moderate topos that is not small, then surely must be and not . But there is an even larger non-moderate topos (such as the topos of all moderate discrete categories) that lies inside. So if you think of that topos as , then the original topos must have been all along.
(The above paragraphs are written as if “small” has a clear meaning, but that is relative too. However, that’s not really anything extra; it’s just what I’ve been saying all along, from a different perspective.)
If somebody does not believe a statement about , there is no way to prove it to him or her. If somebody however accepts and then does not believe a statement about inside it, there is a way to prove or disprove it.
I don’t understand this. What I can prove depends on what assumptions I make. If you tell me that is a topos, then I can prove (for example) that it’s cartesian closed. But if you tell me nothing about , then there is nothing that I can prove about .
If you’re a mathematical realist, then you might say that is a real object about which certain things are simply true (although that doesn’t mean that these things can actually be proved), whereas is merely a convenient fiction. Perhaps some people do believe that, but I’m no mathematical realist, so I can only make sense of such things in (yet again) a relative way.
I agree with David #19, except that I don’t think it’s circular. (-:
Also, I thought #s 5,6,7 constituted more or less agreement about what [[universe]] should be like. Is the subsequent discussion of philosophy changing our minds about that?
Thanks, Mike. It’s nice to pin down one’s own philosophical foundations and find they are not ill-conceived.
I think the philosophical discussion may help shape universe, but ultimately the detail should go elsewhere in the ’foundations’ pages. The question that Urs may be trying to get at (please correct me if I’m wrong) is that if we are going to work inside some universe, and this universe is supposed to exist by some metatheory, then where does the metatheory sit. If we agree to work at the very bottom with first-order logic, then it won’t be ’turtles all the way down’, or all resting on some informal, naive idea. Even just a pointer at universe when Grothendieck universes and structural set theory is mentioned to the appropriate foundational page would be good, in my opinion.
@Mike #21 I didn’t think it was circular either, but I thought that it might appear circular.
The question that Urs may be trying to get at (please correct me if I’m wrong) is that if we are going to work inside some universe, and this universe is supposed to exist by some metatheory, then where does the metatheory sit. If we agree to work at the very bottom with first-order logic, then it won’t be ’turtles all the way down’, or all resting on some informal, naive idea.
Yes. I started by saying that the difference between and is that the former is metatheory.
Apparently I didn’t say this well, but your #19, which it seems finds agreement, I take as a way to say that well.
So I moved that now into universe. Everybody check.
While I can live with it, I still have a question about it: do we need to take the notion of first order logic as the a priori basis of it all and then proceed as in #19?
I thought Lawvere’s idea had been that instead we take the notion of the category as the a priori and then find logic inside it.
first order logic as the a priori basis
But first order logic is just a game with rules and symbols. Once you concieve with the help of that logic an axiomatics of a system which you intepret as SET you can form a new game from it, make new models of that SET and than again make new games from every model. You can try to postulate that you do not care how one such particular game is derived or you can enjoy the variety of possibilities, including that very similar SET, with similar powers, could have being derived from a bit different kind of logic in the first place. It has some appeal to forget where the whole thing came from when setting the general scene. But if I want to know the details, like independence results etc. than I will eventually come to the concrete aspects of a particular SET I work with, or I will have to investigate what are the relatively consistent possibilities by constructing models relative to something. It is in the end not really that much different game from the classical model theory.
Perhaps we need some precise notions of what is a logic, and more discussion of syntax v. semantics, etc.
Urs wrote:
Okay, so is the full process as follows: 1. start with a naive/pre-axiomatic notion of collection and of first-order theory and of model of a theory . 1. then formalize as a model for a 1st order theory in that context; 1. and then define a universe object in . ? I am mostly interested in seeing some expert admit that we need to start somewhere with a naive/pre-axiomatic notion that is not itself further formalized.
and then
Okay, so is the full process as follows: 1. start with a naive/pre-axiomatic notion of collection and of first-order theory and of model of a theory . 1. then formalize SET as a model for a 1st order theory in that context; 1. and then define a universe object in SET. ?
Various replies have been given, and I’ve been wanting to say something, but just haven’t found the time until now. In brief, I find myself agreeing with Zoran and Mike (and maybe others too, but I can recall nodding my head at for example #17).
Of course there is the mathematician’s use of (at least some fragment of) first-order logic, always, at the meta-level of working with any theory, so FOL is generally a given. But it would be hard to say that FOL or first-order theories are naive or undefined notions. The proof? You can implement the whole shebang on a computer, so that the computer will infallibly recognize when a formula (delivered as a string of bytes) is well-formed and when a formal proof is valid (according to some fragment of logic). These are very well-defined things, in the sense of having definite descriptions.
(I guess there could be some philosophical questions here, such as: does a first-order theory, as a “completed infinity” which consists of all wffs which might potentially be used in a theory and of all consequences which are derived from the axioms, exist in some sense? But this has no bearing on practice, in the sense that we only see and use finite parts of the theory at any time.)
Similarly, the notion of first-order theory, and individual instances of first-order theories, are very well-defined things (“very well-defined” is sort of like “very pregnant”, but never mind).
As for models: here it gets trickier. Except for extremely simple theories, an absolute model is almost never completely specified; for example, to assert that we have a model of ZF is like a confession of faith that ZF is consistent, which nobody knows. Here, one finds that the notion of a “universe of sets”, as a collection of objects together with a binary relation in which all the theorems of ZF are true for , is a convenient way of talking, but it is just a way of talking and completely optional or fictional for those who do not believe in Platonic reality.
Most of the time though, in practice, models are relative models, and it might be helpful to think of a model as a translation (or morphism if you like) from one theory to another. A default practice is that a model of a theory translates the terms and predicates of one theory into terms and predicates of ZF, so that ZF serves as the background set theory. Or, if one prefers to speak in terms of an absolute model of ZF (which, again, may be a pleasant fiction for others), then one can consider a model of relative to that absolute model as a translation from into the complete theory consisting of all statements in the language of ZF which are true for .
There is a lot of confusion (even from people who should know better, as on the FOM list) along the lines of “to even speak of categories, you need to speak of collections of objects and morphisms, and in order to deal with these collections you need to have set theory to begin with”. In fact, I wrote fully formal ETCS (or whatever it’s called) to meet that objection: ETCS can be dealt with entirely on the level of symbolic manipulation, just like any theory of sets, and needs no undefined notion of collection (which I think is an argument Harry was giving in an MO exchange when a similar discussion came up). I find it weird that people direct that argument at category theory, but never think of applying the same argument at set theory!
Thanks, Todd.
But I am not sure that I understand “theory” and “model” before we have set up .
When I go to the page “theory” I see right away plenty of occurences of “set”, “class”, “category”.
How do you think of theories and their morphisms before having anything like ?
Urs, you do not need to have SET to talk about finitely many axioms. The fact that one talks about set of axioms, is just a way to say it in full generality and in a bit more formal context. But for our purposes you can take some finite subset and not consider it as a “set” in some SET. Todd was talking “syntactic viewpoint”. Urs, you probably see that “category” usage while appearing on the page, may be in the cases discussed above lived without. Urs seems to indirectly make a case against category theory. Having parallel categorical reformulations at the page, there appeared a confusion as how elementary the treatment of theories can be (if they are not too big).
you do not need to have SET to talk about finitely many axioms.
So you take finite sets to be pre-axiomatically given, then?
Urs seems to indirectly make a case against category theory.
I thought I was in for making the case for category theoretical foundaitons:
it (still, I have to admit, despite all the discussion) seems to me (complete layman that I still am on these matters) that if I base foundations on the assumption that we all know what is it is cleaner than if I base foundations on the assumptios that we all know what theories and their models in firstorder logic are.
Try to explain to a 12 year old on the one hand and theories in first-order logic on the other. I think it is clear which one he will rather understand. And Isn’t that the point of Lawvere-Rosebrugh: they explain in elementary terms to kids. Once that is done, the scene is set for doing mathematics. And very cleanly so.
So you take finite sets to be pre-axiomatically given, then?
No, the choice of words is bad. You do not need axioms for something you can directly check by the tables of truth values and so on. Hilbert was hoping we can check everything including the consistency of ZFC by finitistic means, just as a game with symbols, but Goedel shown we need to assume axioms for things which are powerful enough. To state those axioms in most cases you can at least state them by finite means, syntactically.
I thought I was in for making the case for category theoretical foundaitons
I know you wanted that, but you showed that the appearance of words like “category” in article theory confuses you, as it is to be expected. One needs to think through foundations of logics quite a lot before accepting some modern framework with its own flexibility, including the one devised by the genius of Lawvere. I understand that you would like to cut the path either by accepting the category theory from start plus some simplifying tricks about preaxiomatic at the place where really we have choices.
You do not need to explain nor postulate SET to 12 years old. First order logic can be effectively worked with at syntactical level without ever introducing the axiomatic theory of sets. But it can be also alternatively introduced using axiomatic or naive theory of sets if you choose so. If your needs are minimalistic you do not need to use that alternative.
if I base foundations on the assumption that we all know what SET is it is cleaner than if I base foundations on the assumptios that we all know what theories and their models in firstorder logic are.
It seems you are starting to agreeing with me that there are choices here. For a human it may be cleaner to have some intuition of sets and run the logics with help of some working naive (or weak axiomatic) set theory along the way. From the start. If you are a computer, you want to be run by the implementation/representation of symbolic computation which is defined at syntactic level. The latter contains more of a secure proof than the intuitive way humans do. I do not know what you mean by clean – the intuition or the rigor.
And Isn’t that the point of Lawvere-Rosebrugh: they explain SET in elementary terms to kids.
Here I am less educated. My, possibly false, understanding is that this enables you to use the language and logics “of sets” coming from topos picture, based on finite/elementary presentation, but this is not a model yet where you can possibly check what is true and what is not. Before or later one needs to take choices (using in this or that language, essentially what model theorists usually do). Also, for your purposes: simplicial objects are not elementary, because you need set of integers to talk about simplicial objects (I do not know if a postulated arbitrary natural numbers object in a topos is enough to exhibit constructively something what is really equivalent to the simplex category).
Edit: while not having true simplex category, one can imagine some sort of internalized test categories in the sense of Grothendieck and look for those. Durov in his thesis had produced the theory of pseudomodel stacks, a flexible analogue of model categories adapated to situations involving Kripke-Joyal semantics, with a bit weaker axioms. We could imagine results of Grothendieck and Cisinski (on Grothendieck’s homotopy theory) adapted to internalized versions of test categories.
Todd, Zoran,
okay, thanks. It helps to have this conversation. It should be all very simple, but maybe it’s never spelled out for the non-insiders. (?)
So here might be a road map. If you want a theory of sets, let’s say ETCS, then that’s a specific finitely axiomatizable theory, and anything you want to say and any proof within the theory is fully formalizable (computerizable), without an infinite regress of background theories.
Okay, thanks. That’s good.
We should write this out somewhere. It would be fun if there were an Lab page that would literally serve as the foundation of it all. Given a hypothetical reader who knows nothing about math and decided to start reading the Lab in its entirety would start at this page and would have completely and concisely all the information there as to what the basis of math is. No references back to other entries. The full story.
As this can be worrying to folks new to the formality, perhaps the idea of a brief formal/informal FOL for Dummies section written with a lightish touch (some First Order jokes :-)<- of a very tasteful type, of course!) could be one facet of such a page or better series of linked pages. Eric and I suggested that when we had something we did not understand clearly enough a (category:for Dummies) entry is appropriate, containing a simpler type of discussion plus ’examples’ where appropriate.)
By the way, (off subject), I needed a definition and discussion of term algebra for the new entry on Lindenbaum-Tarski algebra. I noted we have Lindenbaum algebra in several places with no explanation. I am no logician and have very few logic books available. Are these the same and what generality should be used for the term algebra. I also looked at the entry on Boolean algebra and was a bit surprised to find there was no elementary algebraic version given. This is the (for dummies) version perhaps, but seeing one of the usual algebraic description and examples (although these are in the Wikipedia page I’m sure) might enable the ideas about Heyting algebras etc there to be more useful. I’m not sure what level to pitch any additions to that, any ideas or thoughts? (I will put this on another thread so as not to clog the universe.)
perhaps the idea of a brief formal/informal FOL for Dummies section written with a lightish touch (some First Order jokes :-)<- of a very tasteful type, of course!) could be one facet of such a page
That might have it’s uses, too, but I’d like the foundational page itself to be no-nonsense-style. The basis of math. Not a long-winded chat about this and that. There is too much long-winded chat about these issues already. I have to say that when I try to read many of the foundational and type-theory entries on the nLab I am struck by their high ratio of text over formal statements. Probably that’s useful for the experts, but for somebody from the outside trying to figure out what the heck is really going on, it can be very frustrating,
Maybe we should have a Talmud-style page on foundations: in the middle the concise creation story, around it the commentary.
@Urs I think you are right. When I said section, i really meant ’associated page’. My thought would be a ’what do WE mean by a logic when were have to be precise and concise!’ but there needs to be an elementary page which should be non-woffle but precise, so with limited objectives.
Related comment. I have checked online for the concise “first” logics textbook Mathematical Logic: A First Course by my Ph.D. advisor Joel Robbin from around 1969 and learned that there is a Dover paperback now: http://www.amazon.co.uk/dp/048645018X/ref=asc_df_048645018X1230081/?tag=ciaouk-books-21&creative=22110&creativeASIN=048645018X&linkCode=asn
I think that Todd #36 explains it fairly well. We should have a page on foundations for Eric Forgy.
I have rewritten universe. I kept most of what was there, moving a bit to the introduction of internalisation.
Great service Todd!
Yes, thanks, Todd, that’s very nice. Looking forward to it.
This might, once connected with “fully formal ETCS” and what follows, eventually be something of quite general interest, I suppose.
I like how universe is shaping up. Especially the explicit link between reflection and internal universe objects.
Yes, I like Toby’s restructuring.
@ 48 & 49: Thanks!
I see Wittgenstein’s attitude to logic appeared at #19. Coincidently, I was reading yesterday a piece by the philosopher Michael Friedman, On the Sociology of Scientific Knowledge and its Philosophical Agenda, Studies in History and Philosophy of Science, Vol. 29, No. 2, pp. 239–271, 1998, which runs over relevant material.
the Tractatus…attempts to present the philosophical foundations of the new mathematical logic recently articulated by Gottlob Frege and Bertrand Russell—which logic, according to the Tractatus, depicts the universal and absolutely necessary framework within which alone any linguistic representation whatsoever is possible. It is in virtue of this logical framework, and this framework alone, that it is possible at all to represent the world:
Logical propositions describe the framework of the world, or rather they present it. They do not ’treat’ of anything. They presuppose that names have meaning and elementary propositions have sense; and this is their connection with the world. It is clear that it must indicate something about the world that certain connections of symbols— which essentially have a determinate character—are tautologies. Herein lies the decisive point. We said that some things are optional in the symbols we use and some things are not. In logic only the latter is expressed. This means, however, that in logic we do not express what we wish with the help of signs; rather, in logic the nature of the absolutely necessary sign itself gives testimony: if we know the logical syntax of any sign language whatsoever, then all the propositions of logic are already given. (T, 6.124)
And it is in this way, too, that logic obtains a uniquely privileged status: ’Logic is not a doctrine, but a mirror-image of the world; logic is transcendental.’ (6.13) (Friedman, pp. 256-7)
Both Wittgenstein and Carnap, leading light of the Vienna Circle and admirer of the Tractatus, were later profoundly influenced by the construction of an alternative logic by Heyting from Brouwer’s ideas.
So, in 1934, Rudolf Carnap, the leading representative of logical positivism, bit the bullet and took the decisive step of asserting that there is no over-arching notion of universal validity or ’correctness’ independent of the particular, and diverse, rules of the particular, equally possible and legitimate, formally specifiable calculi. For this reason, the very notions of ’rationality’, ’objectivity’, and ’correctness’ must be relativized to the choice of one or another formal language or ’linguistic framework’. The particular logical rules of a given linguistic framework define what counts as ’correct’ and therefore rational within that given framework, and it follows that no over-arching notion of rationality or ’correctness’ can govern the choice between different such frameworks. This latter choice, as Poincaré had first emphasized in the particular case of Euclidean and non-Euclidean geometries, can only be a free stipulation or convention governed by pragmatic—as opposed to rational—criteria. The result is Carnap’s celebrated ’Principle of Tolerance’:
In logic there is no morality. Anyone may construct his logic—i.e., his form of language— as he wishes. But, if he wishes to discuss [matters] with us, he must clearly specify how he wishes to construct it and give syntactical determinations instead of philosophical considerations.
(Friedman, p. 250)
Interesting to see Mac Lane’s contribution to debates about logic in the 1930s. According to Steve Awodey, in Mac Lane’s review of Carnap’s Logical syntax of language
he observed that there was a crucial flaw in the all-important definition of logical validity. Carnap had attempted to define the “logical symbols” as the largest collection of symbols such that every sentence constructed only from them is logically determinate, and Mac Lane observed that there need be no unique such maximal set. The situation is, of course, similar to one arising often in algebra, as he surely recognized. Mac Lane concluded:
Such technical points might raise doubts as to the philosophical thesis Carnap wishes to establish here: that in any language whatsoever one can find a uniquely defined “logical” part of the language, and that “logic” and “science” can be clearly distinguished. (Mac Lane 1938, p. 174; see also pp. 173-175).
(Awodey, p. 117)
Awodey, In Memoriam: Saunders Mac Lane, 1909-2005, Bull. Symb. Logic Vol. 13, No. 1, Mar., 2007 (pp. 115-119)
I wonder what there is to say about Tarski’s idea (and Jim Dolan’s continuance ) described by Todd here of an Erlanger Program for logic, logical notions being those preserved by every automorphism.
David,
I read now with a certain renewed interest these quotes that you give. It seems striking that in the words of all these deep thinkers I see no indication of the clear story that people have eventually been teaching me here, the one I imagine Todd is writing out currently.
Urs,
the reason of disparancy you note in 53 is I think in different objectives. One is to try to see what are the possibilities and limitations of foundations which these great people discuss and another is to set up a minimal extension of controllable finitistic machine approach by independent axioms and further modelling in the sense of model theory which is the minimalistic need for a community like lab. Nobody said that the foundations are closed subject, but rather that there are rather standard syntactic ways to avoid the non-finitistic content in foundations and move all the rest into axioms. The unprovability of consistency of the axioms of set theory has nothing to do with conceptual part like thinking collections, or with the way we construct the syntactic machine. The uneasinees with using any axioms of set theory, being unprovable for consistency, is, I think, the reason people want to free from set theory. The Lawvere approach talks about logics from SET object, regardless how that one was constructed in first place. This gives the flexibility which i was talking about before, but it also looses the assertiveness a choice of some SET theory gives you. Abstracting the notion of set theory internally and elementary is indeed quite an achievement. But at some point you will have to have a concrete choice. In any case, the reasons for categorical foundations are not in classical approach being unclear. The philosophical aspects out of reach are still out of reach.
I feel we somehow need better entries on universe , at least in the context of higher topos theory.
For instance I want to put the following statement somewhere, but our current design of universe-related entries doesn’t really suggest a place where it should go:
so the codomain fibration plays the role of an internal universe, as mentioned a bit here and there, say at internal sheaf or at 2-sheaf. I would like this discussed more systematically somewhere.
Maybe give me some feedback to organize my thoughts.
So this here should be relevant: if is an -topos with object classifier (of some size), then the codomain fibration is the dependent sum along , namely is and
is the codomain fibration itself.
Somehow I feel like playing around with this more should tell me something. But not sure yet.
Hm, so if is the internal version of the codomain fibration, maybe one should really look at the full
This is the internal version of the exhibiting the codomain fibration as a map of pointed -toposes
Added the pointer
to universe and to type of types.
(From this HoTT discussion, old but still viral here at CRM. From personal discussion I know that the pure homotopy theorists are confused about what is going on and so far no type theorist has given a clear answer…)
What is going on about what?
So here is what I know:
At the beginning of my talk at CRM I had recalled/amplified the fact that HoTT without possibly univalence is interpreted in any locally cartesian closed category. That had seemed to be widely un-appreciated.
Then, inspired by this, I think, next day Bas in his talk had started by amplifying that the failure of the univalence axiom to hold in These models is at worst… and then something from that discussion linked to above. People started questions about that, but nobody really gave an answer.
Later I asked some of the pure homotopy theorists who were attending over coffee what they take from the talks. They tell me that it is confusing, since they can’t tell which statement in which talk will actually be true in which model, and to which extent that’s a Theorem and to which extent it is a hope.
What I know for sure, and what I try to spread word of, is that everything not using univalence holds in all locally Cartesian closed categories, and that everything with Univalence holds in infinity-groupoids and the models that you discussed.
And finally that I think that unless they care specifically about Computer code, then that issue about strictness of the pullback of the univalent universe is negligible. But of course that’s precisely where they would like to hear a more definite Statement.
(Sorry for the funny capitalization in this post. Need to figure out how to tell my new machine how to stop interfering with that.)
The issue of strictness is if you want to actually construct a model of type theory using the universe, rather than just using it as an object classifier.
Okay. Maybe someone should write out some part of chapter 8 (for instance) in the sort of type theory that we know is modeled by any -topos. Then by comparing the two, one might more easily be convinced that “all other arguments of this sort” will also work similarly.
@Zhen Lin, yes, that’s the issue, and “people” would like to know what the general answer is. My experience from talking over coffe to a mixed audience of more or less pure type theorists and more or less pure homotopy theorists is that providing more solid statements here about what is and what is not “clear” will fill an unnecessary communication gap.
@Mike: that might be good!
Mike,
for instance here is a question that I was going to ask after Peter Lumsdaine’s talk at CRM, had I not had to leave early to catch my flight:
Peter started his (very nice) talk by saying that he will announce a formalization of the Blakers-Massey theorem in homotopy type theory and that at the end he will indicate how he and his co-authors used this to extract a new proof of the theorem in infinity-topos theory.
So I was wondering: to which extent they found this “extraction” to be automatic, trivial, clear by existing results, or to which extent they found they needed original ideas here.
Well, I don’t know what Peter would have said, but based on my experience doing something similar for , it depends on what you mean by “infinity-topos theory”. All the chapter-8-style proofs require only Rezk descent rather than univalence/object-classifiers, and it shouldn’t be too much work to reformulate such a proof to work with the up-to-homotopy descent that holds in known infinity-topos models (this is what I was envisioning in #61). Then it would automatically be a proof that applies to all infinity-toposes — but it wouldn’t look especially topos-theoretic, being couched in type theory language. One could then “compile” it out into a more categorical proof, which would be algorithmic but tedious, and may not result in a very readable proof. Sometimes, however, the resulting categorical proof might admit a simplification that would make it prettier, but that probably requires some thought.
1 to 67 of 67