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.
To Toby, mainly, of course also to anyone interested:
We have a page-“category” foundational axiom, but we have no entry of that name. We should start one! foundational axiom.
(We do have axiom of foundation. A bit of a different thing.)
I’m not sure what I’d put there; we have foundations and axiom.
I’m not sure what I’d put there;
An explanation would be good. Complete the sentence:
“An axiom is called a foundational axiom if … foundations …(?)”
we have foundations and axiom.
What do you mean by saying this? I am not sure I understand. (We also have, say, differential and geometry, but still also differential geometry is necessary. )
I have created a stub foundational axiom now and linked to it from foundations - contents .
By the way, the entry foundations would deserve some attention. Somehow it should start with a word on “foundations” in general, before talking about foundations of category theory. There is also a lot of discussion boxes between you and me that should be removed and replaced with their result, if any. Finally I guess we’d want something about type theory and homotopy type theory there.
You are probably aware of these deficiencies of the entry. I just thought I’d highlight them again. Maybe somebody sees me saying this and feels inspired to help out with some edits.
@Urs: I sympathize with Toby’s #2, or more precisely I’m not sure what you have in mind. Is a foundational axiom supposed to mean an axiom belonging to a theory which purports to be a foundation of mathematics, or something along those lines?
Having written that, I’m not sure it’s such a coherent notion, since it makes about as much sense to consider an axiom outside the context of an ambient theory as it does to consider a vector outside the context of an ambient vector space. Would it make more sense therefore to have foundational theory?
Is a foundational axiom supposed to mean an axiom belonging to a theory which purports to be a foundation of mathematics, or something along those lines?
I don’t know, that’s why I am asking Toby. Toby has labelled many entries by category: foundational axiom. So I thought we should explain somewhere what this is.
If there is no precise definition, we should still say a bit about the intuition in which sense the axioms listed at category: foundational axiom are “foundational”.
Maybe one can say:
A typical axiom in mathematical practice characterizes a very particular property of a very specific structure in some subfield of mathematics. But some axioms pertain to the very nature of the ambient logic being used, and thus affect mathematics as a whole. These might be called foundational axioms.
?
Toby has labelled many entries by category: foundational axiom.
Oh, I see. Thanks.
I put an entry into that category if it’s about a statement that one might want to adopt as an axiom in a foundation of mathematics.
I don’t know that it would do much good to say this at foundational axiom, any more than it would help to explain other categories at meta, people, or reference. None of these pages are linked to from the respective category’s page list or from the pages in the respective category.
It would be nice if each category’s page list had an editable field to explain what the category is about. That would require changes to Instiki.
I don’t know what you hope to achieve with the page foundational axiom, so I don’t know how to help you with it. I find category: foundational axiom useful, because I can add a page to the category when creating or editing the page and then look through the list, which I teach from the bottom of each listed page. The list at your page is less convenient to reach and less convenient to keep up to date.
ETA: Well, right now the category list is useless, since it’s not actually showing up. But that’s a bug of some sort, which hopefully will be fixed soon.
Hey Toby,
I understand that you are displeased by this move, and we don’t have to follow it up. I didn’t think it would be such a big deal not to create some entry that explains something. Can’t hurt, can it?
So don’t feel pressed to reply if you feel you are wasting your time, but I’ll just briefly comment on what you said:
I don’t know that it would do much good to say this at foundational axiom, any more than it would help to explain other categories at meta, people, or reference.
As soon as I feel the term “people” deserves explanation on the Lab, I will add an entry on it. But the thing is that your use of “category: foundational axiom” is so far the only proposed use of the “category:”-functionality that carries actual content. It is analogous to the floating Context-table of contents that I like to use, such as topos theory - contents. I could have marked these “category: topos theory”. But I feel that the “category:”-functionality does not serve this purpose well, precisely because it does not allow me to combine the full list of keywords with some context.
So topos theory - contents etc. all start with a link to an explanation of what the topic is all about. I think that’s much more useful to the reader than a simple label “category: topos theory” in each entry would be.
When I see your “categories: foundational axiom” I always wondered about the term. So now I asked you. Other readers might wonder to. It doesn’t hurt to explain something, even if it is plain obvious to you.
I certainly don’t mind explaining the term, and I hope that I did (in the first paragraph of #8). Now that foundational axiom is there, I may as well edit it so that it covers the category.
I just don’t see how to make it useful. It could be useful if turned into a table of contents. But we already have foundations - contents, which covers this. (I should have listed that in #2 also.)
You created a stub and asked others (principally me) to fill it, and I have nothing to fill it with. That doesn’t really hurt anything, but I just don’t think that I can help you.
Okay, sorry, I guess I should have just asked you before creating the entry, maybe that was an irritating move to create the entry while posing the question.
By the way, concerning this point here:
The list at your page is less convenient to reach and less convenient to keep up to date.
This is a general issue: instiki “categories:”-functionality is convenient for the editor, but its output is ugly and inconvenient for the reader.
The optimal solution would be if we could make instiki display just the list of items that are currently listed in the left column at the categories:-lists, with all the other clutter removed, so that we could then
[[!include
that list in more contentful pages, as desired.
That would nicely combine the convenience for the editor that you are after with the convenience for the reader that I am after.
In absence of this functionality, I have now tried to at least partially alleviate your concern about “my” list not being up-to date creating foundational axiom - contents and then
[[!include
-ing that into foundations - contents and foundational axiom. This way at least only one list needs to be kept up-to-date manually.
I also finally noticed some curious redundancies in foundational axiom - contents, which look like they originate in different people editing the list without fully appreicating the other’s contribution. I don’t know what exactly happened. Anyway, I tried to remove the redudancy, but I guess the list still needs some polishing.
I figured that the one thing that I could do for foundational axiom was to put in an organised list of every page in that category, since you didn’t have all of them (and also had a few not in the category). Just when I’d gotten my list in, and before I’d done anything to your list, you found it. You moved it all to foundational axiom - contents and combined the lists; there were still a few redundancies under the axiom of choice, so I did one last reorganisation.
Oh, I see. Sorry for the overlap. Thanks for working on this!
I am still mildly interested in the question where foundations end and where non-foundation starts. It’s just a kind of idle thought, not very important, but it keeps coming back to me when I am in need of distraction, it seems.
For instance (if I may bore you all with that example yet again), if we add the axiom of cohesion to homotopy type theory, would it count as a “foundational axiom” to your mind? Probably not, but can you somehow make explicit what it is about that axiom, for instance, that is “non-foundational”?
Adding this axiom to HTT produces cohesive homotopy type theory? This would count, assuming that CHTT is intended as a foundation of all mathematics rather than, say, a foundation of differential geometry.
There is a bigger issue here, which is why things like the univalence axiom are not in the category, which is that I haven’t worked on the HTT articles. Although HTT seems to me very promising as a foundation, I haven’t had the time to really look into it, so what I know is -dimensional (set-theoretic and type-theoretic in the traditional way) foundations.
The real definition of what I’ve been putting in this category is not ‘a statement that one might want to adopt as an axiom in a foundation of mathematics’ but rather ‘a statement that one might want to adopt as an axiom in a set-theoretic foundation of mathematics’ (so not even ordinary type theory gets in, except where they overlap). Which means that either the name is inappropriate or the category should have a lot more entries.
The bottom line about this category is that I created it so that I could find the articles, and it might not suit anybody else’s purposes. I could give up the name ‘foundational axiom’ for it (since that name is really too broad), but I wouldn’t want to give up the category itself.
This would count, assuming that CHTT is intended as a foundation of all mathematics rather than, say, a foundation of differential geometry.
But each of these axioms rules out some mathematics, by definition. The axiom of choice rules out mathematics without choice, so once we adopt it, we no longer have a foundation for all mathematics.
I am aware that this is kind of an annyong remark of mine. I am just trying to get a feeling for how you or others think about these things.
The real definition of what I’ve been putting in this category is not ‘a statement that one might want to adopt as an axiom in a foundation of mathematics’ but rather ‘a statement that one might want to adopt as an axiom in a set-theoretic foundation of mathematics’ (so not even ordinary type theory gets in, except where they overlap). Which means that either the name is inappropriate or the category should have a lot more entries.
The bottom line about this category is that I created it so that I could find the articles, and it might not suit anybody else’s purposes. I could give up the name ‘foundational axiom’ for it (since that name is really too broad), but I wouldn’t want to give up the category itself.
I see. Okay, I would suggest that eventually we should indeed do something like this, i.e. distinguish within “foundations” the “set theoretic foundations” in the Lab structure.
But I won’t further pester you with it for the moment. ;-) I need to concentrate on something else…
The axiom of choice rules out mathematics without choice, so once we adopt it, we no longer have a foundation for all mathematics.
That’s a great point! But traditionally, when people propose a foundation for mathematics, they put in the axiom of choice (or otherwise ensure that this result is provable) because they believe that it’s true, so mathematics without it is incomplete and mathematics that denies it is wrong. I don’t see it that way, but my approach to foundations is largely to study the systems that various true believers have come up with (including their motivations as much as their results), so I still care about the prescriptive approach.
By ‘all of mathematics’, I meant as opposed to specific fields. For example, Abstract Stone Duality is specifically intended as a foundation of topology. (It actually covers sets as discrete spaces, but its set theory is too weak to re-found its topology thereon.)
I added axiom of choice under the section ’axioms of choice’.
Urs may disagree with me, but I wouldn’t be inclined to regard cohesive HoTT as a “foundation for all of mathematics”. On the other hand, one might argue that the notion of one foundation for all of mathematics is wrong-headed anyway; one should use different axiomatic/type-theoretic systems depending on the mathematics one wants to do. (I’m not sure whether or not I would argue that way.)
Also, I don’t think one has to believe the axiom of choice to be ’true’ in order to assume it as a ’foundational axiom’ – one just has to want to work, for some particular purpose, with a sort of mathematics whose foundations does include AC.
Another problem with labeling type-theoretic foundations with ’category: foundational axiom’ is that most aspects of type theory are not called “axioms” but rather “type formation rules” or something of that sort. The univalence axiom is an exception, partly because it has not yet been satisfactorily rephrased in a more type-theoretic way.
Urs may disagree with me,
No, I don’t disagree with it. On the contrary, cohesion is an axiom with a decidedly special-purpose flavor to it. Clearly we don’t want to throw away all toposes that are not cohesive.
I am just trying to get a feel for where “foundations of all of mathematics” ends.
@David: The heading axioms of choice already linked to axiom of choice.
I don’t think one has to believe the axiom of choice to be ’true’ in order to assume it as a ’foundational axiom’ – one just has to want to work, for some particular purpose, with a sort of mathematics whose foundations does include AC.
Once you’re using different foundations for different mathematics, yes. But traditionally (by which I mostly mean the responses to the foundational crisis a hundred years ago, although much contemporary work is in the same line), if you have one foundation for all of mathematics, then you’ll only put an axiom into that foundation if you think that it’s true. At least, that’s why people argued about AC back in the day. I don’t really want to defend that approach; I just think that it’s very common.
I’ll try to further explore your all thoughts on this:
I would like to disregard the historical development of these ideas for the moment, and also disregard any discussion of the Lab entries as they currently are.
Just generally, using the best personal idea about mathematics that you (you Toby, you Mike, etc.) currently have: what do you feel what the best notion of “foundations” actually is?
Or more specifically: suppose, naive layman of formal logic that I are, I went ahead and declared: The definite foundation of maths is intensional dependent type theory. Every other sensible proposal is obtained by adding an axiom (or type formation rule, if you insist) to that.
How weird a standpoint would you find that?
(Of course I may want to have “intensional dependent type theory + univalence” here, but I feel saying this currently still opens a can of worms that distracts from the main point that I would like to explore here. So let’s disregard univalence for the moment.)
So I am thinking:
intensional dependent type theory is so very basic, that one can hardly argue that removing anything from it still is a foundation. It’s really just the most basic stuff but conceived of constructively. In particular “intensional” just says we don’t have some axiom, not that we assume something special.
At the same time it is both efficient and comprehensive as a foundation: comprehensive because by adding axioms, we can get all other reasonable proposals for foundations (right?); efficient because already with no axiom added, it is a sensible foundation.
What’s your all feeling about this?
Do you all feel that “foundations” and “foundational axiom” have forever to remain subjective and arbitrary terms? Or do you think that there is actually progress in formal logic that indicates that we are beginning to see a more objective notion of foundations?
No, the objectively correct foundation of all mathematics is Elementary Function Arithmetic; anything else is unnecessarily strong.
Seriously, while HoTT is great, I don’t believe in any absolute foundation. (That HoTT is far stronger, proof-theoretically, than necessary is just one reason for this.)
Thanks for the reaction. What does this here mean:
far stronger, proof-theoretically, than necessary
Necessary for what?
while HoTT is great, I don’t believe in any absolute foundation.
Could you give examples of theories that you would count as foundations but that are not of the form intensional dependent type theory + further axioms? So that I can get a feeling for what you have in mind.
Necessary for what?
For proving results of ordinary mathematics, such as those in Harvey Friedman’s list (look for the paragraph with all of the quotation marks). Actually, EFA is too weak to prove much of this (although it can state all of it); EFA is the basic foundation to which one adds axioms. (One can also consider weaker things than EFA, but they don’t seem to be able to prove anything interesting. Still, I’m not sure that I’d want to defend EFA specifically; a lot of people go for Primitive Recursive Arithmetic, which is a little stronger than EFA, instead, and maybe EFA is a little stronger than something else that would also be good.) I believe that everything in Harvey’s list can be proved in second-order arithmetic, which is really a kind of set theory. (That’s still rather truncated, but remember that -category theory can be encoded in set theory.)
Could you give examples of theories that you would count as foundations but that are not of the form intensional dependent type theory + further axioms?
Since EFA is proof-theoretically weaker than HoTT, it cannot be expressed as HoTT + further axioms. I expect that SOA can be expressed as HoTT + further axioms, but I’m not sure how to do it. However, if by ‘intensional dependent type theory’ you mean the bare bones of type theory without -types and the rest, so that first-order logic is this plus an axiom forcing everything to be -truncated, then EFA (which is usually expressed as FOL + a type + further axioms, although it need not be) is this plus some other stuff. But notice that this bare bones is itself too weak to support ordinary mathematics without the other stuff.
I don’t usually look at these arithmetic foundations because they are so impractical to use. But it is (at least initially) rather surprising that so much abstract mathematics can be encoded into arithmetic, and then proved using fairly weak assumptions. (The field that studies how weak these assumptions can be is reverse mathematics.) There is a disconnect between this style of foundations and what Paul Taylor has rightly called practical foundations of mathematics (an idea similar to David Corfield’s philosophy of real mathematics). Famously, one cannot discuss practical foundations on the FOM mailing list, the source of Friedman’s list that I linked earlier. But there are known connections, basically via material set theory; for example, SOA is equiconsistent with CZF + separation (pdf), and CZF + separation is equiconsistent with the theory of a well-pointed --pretopos with fullness, separation, and collection (as Mike has shown). And the latter is quite practical.
Thanks, that’s interesting. One quick dumb question while I am still reading: what is “SOA”?
Let me reproduce that list of theorems that Friedman mentions here, for the record:
“every field as a unique algebraic closure,” “the Stone-Wierstrass theorem,” “every continuous function on a compact set is uniformly continuous,” “compact = closed and bounded,” “the intermediate value theorem,” “the maximum value theorem,” “the mean value theorem,” “every monotone function is differentiable almost everywhere,” “ordered fields = real fields”, “every real closed field has a unique real closure,” “every real closed field becomes algebraically closed when i is adjoined,” “the Cauchy-Peano theorem for differential equations,” “the Hilbert basis theorem,” “the Hahn-Banach theorem,” “the Radon-Nikodym theorem,” “the closed graph theorem,” the Baire category theorem,” “the Lebesgue convergence theorems,” “the Riesz representation theorem,” the Riemann mapping theorem,” “Fubini’s theorem,” “Fourier transform theorems,” “power series development of analytic functions,” “Cauchy’s integration theorem,” “zeros of analytic functions and omission of values,” “the open mapping theorem,” “the maximum modulus theorem,” “analytic continuation theorems”, “the Mittag-Leffler theorem,” “the monodromy theorem,” “the no-retraction theorem,” “the Picard theorem,” theorems of Paley and Weiner,” “Mergelyan’s theorem,” “the Brouwer fixed point theorem,” “the Schoenflies theorem,” “Sylow theorems,” “Ulm’s theorem on Abelian p-groups,” “decomposition theorem for Abelian groups,” “subgroups of free groups are free,” “power series are Noetherian,” “Hilbert’s Nullstellensatz,” “Sturm’s theorem,” “volumes stretched by absolute value of determinant,” “Cayley’s theorem,” “theorem on symmetric polynomials,” “fundamental theorem of Galois theory,” “unsolvability by radicals,” “Frobenius and Wedderburn theorems on associative division algebras,” “Zorn’s lemma,” “the Jordan-Holder theorem,” “the Krull-Schmidt theorem,” “invariance of dimensionality,” “the Wedderburn-Artin theorem for simple rings,” “density theorems for rings,” “Artin-Rees and the Krull intersection theorem,” “Artin’s solution to Hilbert’s seventeenth problem,” “metrization theorems,” “simplicial approximation theorem,” “Jordan curve theorem,” “the Euler-Poincare formula,” “the contraction mapping theorem,” “the excision theorem,” “exactness of Mayer-Vietoris,” “Jordan-Brouwer separation theorem,” “implicit and inverse function theorems,” “Tietze’s extension theorem,” “Urysohn’s theorem on normality,” “Stone-Cech compatification,” “Borsuk’s Antipodal theorem,” “Borsuk’s separation theorem,” “Brouwer domain invariance theorem,” “the Hurewicz uniformization theorem,” “fundamental theorem of the local theory of curves,” “the isoperimetric inequality,” “the four-vertex theorem,” “the Cauchy-Crofton formula,” “Gauss’ theorema egregium,” “Gauss-Bonnett theorem,” “triangulation theorems,” “Poincare’s theorem on indices of a vector field,” “the Hopf-Rinow theorem,” “the Hadamard theorems,” “Fenchel’s theorem,” “the Farey-Milnor theorem,” “Jacobi’s theorems on geodesics,” “Hilbert’s theorem on constant negative curvature,” “Dirichlet’s theorem on primes,” “the fundamental theorem of arithmetic,” “Minkowski’s area theorem,” “Chinese remainder theorem,” “Gauss’ law of reciprocity,” “Fermat’s and Wilson’s theorem,” “transcendence of e and pi, and criteria,” “various Diophantine equations,” “Mobius inversion formula,” “the prime number theorem,” Lagrange’s four square theorem,” “Hilbert’s theorem on sums of k-th powers,” “Bertrand’s postulate,” “Minkowski’s theorem,” “Kronecker’s theorem on approximations,”
I don’t quite understand yet what Friedmann’s claim is, precisely, concerning this list. But I gather you are saying that all these theorems can be proven in elementary function arithmetric.
I see that there are differential-geometric theorems in that list, such as the Gauss-Bonnet theorem. Can you give me a rough idea how one formalizes this in elementary function artihmetic? I supose it’s some wildly indirect way via some Gödel-numbering system, right? How does one see which theorems can be proven this way, and which not?
Would you think that other differential-geometric theorems such as the Atiyah-Singer index theorem are provable by arithmetic function arithmetics?
Or what about the Poincaré conjecture? Is this all in there? What is not in there?
@Urs 28: SOA = second-order arithmetic.
You might want to read a little of the Wikipedia article on reverse mathematics, especially the section on use of second-order arithmetic, to get an idea how statements dealing with real numbers are handled. I don’t know that much about it, but it’s not a case of lots of ad hoc encoding by Gödel numbers or anything like that; it’s meant to take a close look at natural mathematical arguments and see how much of them can be expressed in fragments of SOA (in a way more or less preserving ’naturality’).
I gather you are saying that all these theorems can be proven in elementary function arithmetric.
That would surprise me. I’m saying (or at least I gather that Friedman is saying) that they can all be proved in second-order arithmetic (SOA), which is EFA plus another type and some axioms.
I don’t think that one could formalise the Gauss–Bonnet Theorem in the first-order language of EFA, but one should be able to formalise it in SOA. I don’t think that it could begin “Let be an abstract set with the structure of a 2D manifold.” (although since I linked to a paper that claims an interpretation of CZF in SOA, maybe it could, although I don’t understand how); but it could begin “Let be a subset of with the property of being a 2D embedded submanifold.”. (The Whitney Embedding Theorem is not on Friedman’s list and probably could not be. One would also have to argue here that non-second-countable or non-Hausdorff manifolds are an unnecessary generality completely irrelevant to the point of the Gauss–Bonnet Theorem, which I think is defensible. Or even argue that abstract manifolds in the first place are unnecessary generality, so who cares about Whitney’s embeddings, which I think is not so easily defensible.)
Now, a subset of is given by a property of -tuples of real numbers; but since a -tuple of real numbers can be encoded as a single real number, it becomes a property of real numbers. Unfortunately, a real number cannot be encoded as a natural number, but it can be encoded as a set of natural numbers, so the subject of the theorem is certain properties of sets of natural numbers. As second-order arithmetic is about natural numbers and sets of natural numbers, but not sets of sets, this theorem would seem to be really a theorem scheme in SOA, one theorem for every property of sets of natural numbers expressible in the language of SOA, stating that if some formula involving this property is satisfied, then some conclusion follows. This is a little unsatisfying, because it means that we’ve really only stated the theorem for definable 2D (second-countable Hausdorff) manifolds.
But there may be some trick here that I don’t know that makes 2D manifolds first-class objects in the language of SOA. (And this would be necessary for any theorem with a hypothesis that states something about all 2D manifolds, for example.) An analogous trick (which I do know) works for continuous functions (meaning real-valued functions of a real variable). Although arbitrary functions are a third-order concept, a continuous function is given by its values on rational numbers, making it a second-order concept. (So SOA can express a theorem saying something like “If every continuous map has some property, then ….”.) Possibly some similar trick works for embedded submanifolds of , even though no trick could work for arbitrary subsets of .
Toby wrote
There is a disconnect between this style of foundations and what Paul Taylor has rightly called practical foundations of mathematics…
Right, so best avoided ;) . I could convey myself a mile without letting my feet touch the ground and with no equipment, but why would I want to, except to see if I have a high level of determination?
I would be (slightly) more interested in weak systems if Mike was onto something here.
I guess I share David’s sentiment, and probably most of use here do. But I still want to understand some of these foundational things better than I do.
I wish the Lab would offer more explanation of the form that Toby is providing here! (:-)
When looking at Wikipedia for help this morning over breakfast, I am struck that we don’t even have an entry mathematical logic. Well, now we have, a tiny stub. Experts please go there and see if it inspires them to add something. I also expanded the Idea-sentence at theory, please check if it’s okay.
Unfortunately, I really must stop now being distracted by this discussion here, interesting as it is. I must look into something else for the moment.
Hi Toby,
one more comment after all:
The Wikipedia page on Reverse mathematics has:
[..] weak subsystems of second-order arithmetic suffice to formalize almost all undergraduate-level mathematics
(my emphasis).
I am beginning to get a feel for why people find that interesting. But I guess I don’t feel in agreement then with your sentiment of “necessary strength” expressed above. To me, the “necessary strength” of a good foundations of mathematics is that it gives us the deep results about our world, say a formalization and proof of the mass gap conjecture (to name something from differential geometry or related that comes with a special kind of “absolute relevance” attached to it). This does not seem to be included in “almost all undergarduate math”.
Also, while I cannot formalize it at the moment, it seems to me that in a different sense HoTT is much weaker than SOA: namely in terms of “conceptual contrivedness”, or something like this. Its axioms (or type formation rules) are really just the bare essence of thought: there are types, we can take their sum and product, and there are identities. Period. Compared to that elegance, the axioms of SOA are a sad mess. (Or so I feel, without being able to formalize the term “sad mess of axioms” for the moment, but I guess you will, if not agree, see what I mean).
In the writeup of Mike and mine we have a little comment in the introduction, about how differential geometry – not to speak of differential cohomology, the mathematical theories relevant for the tangible world – always seemed to be so many orders of complexity above the foundations. (That’s the issue you are also talking about above re the Gauss-Bonnet theorem in SOA.) And how it is remarkable that with just the simple axioms of HoTT+Cohesion, central theorems in these fields (such as the curvature exact sequence) are provable very directly from the axioms.
This is something I find, if not necessary so at least very desireable for a foundation of mathematics. Which, after all, is then also going to be a foundation of human thought and science in general .
How to sort out topics between logic and mathematical logic is not obvious to me. As it stands, the shift at logic from general idea to
Category-theoretic logic
It turns out that logic is naturally expressed in the language of category theory
seems to me too fast. For one thing, logic is taken by some to include inductive logic. Second, might this category theoretic logic be better placed elsewhere?
Now I read more closely, I can’t say I like
As a discipline, logic is the study of methods of reasoning. While in the past (and often today in philosophical circles), this discipline was prescriptive (describing how one should reason), it is increasingly (and usually in mathematical circles) descriptive (describing how one does reason).
It surely can’t mean that logic describes how the man-in-the-street actually reasons. Perhaps the idea was that, e.g., where once it was a matter of who was right or wrong in the advocacy of constructive reasoning, now one can be interested in the latter without thinking that it should be used in reasoning.
OK, so I’ve made some additions to logic. As I said, I don’t like
As a discipline, logic is the study of methods of reasoning. While in the past (and often today in philosophical circles), this discipline was prescriptive (describing how one should reason), it is increasingly (and usually in mathematical circles) descriptive (describing how one does reason).
as it stands. Could whoever wrote it explain what they meant?
Also I don’t think that category-theoretic logic should be there. Should it not appear in mathematical logic, or be pointed from there?
Re 35, they’re just different senses of foundations. One tries to see how little one needs to assume to be able to prove something, in however convoluted a fashion. The other is about sorting out fundamental concepts. Surely here we follow Lawvere in preferring the latter:
In my own education I was fortunate to have two teachers who used the term “foundations” in a common-sense way (rather than in the speculative way of the Bolzano- Frege-Peano-Russell tradition). This way is exemplified by their work in Foundations of Algebraic Topology, published in 1952 by Eilenberg (with Steenrod), and The Mechanical Foundations of Elasticity and Fluid Mechanics, published in the same year by Truesdell. The orientation of these works seemed to be “concentrate the essence of practice and in turn use the result to guide practice”. (Lawvere 2003: 213)
Lawvere W. 2003, ‘Foundations and applications: axiomatization and education,’ Bulletin of Symbolic Logic 9 (2003), 213-224. Also available at http://www.math.ucla.edu/~asl/bsl/0902/0902-006.ps .
Maybe we’d be better using the word ’principles’.
they’re just different senses of foundations. One tries to see how little one needs to assume to be able to prove something, in however convoluted a fashion. The other is about sorting out fundamental concepts.
Okay, sure. But there is still this issue of Toby’s “necessary”. Quite independently of differing tastes concerning the style of the foundations, it seems it should be possible to agree on what is necessary for something to be called a “foundations of mathematics”. That might help objectivize the relation between the two approaches. I don’t know, maybe not.
Thanks for the quote by Lawvere. I used that together with some introductory paragraphs to try a first little something in the Idea-section at foundations. Everybody please check.
it seems it should be possible to agree on what is necessary for something to be called a “foundations of mathematics”.
Depends what you mean by ’should’. You evidently didn’t participate in the great FOM discussion. We may agree that a foundation of a field should shape its fundamental concepts, but if Friedman or Simpson say ’No’, what are we going to do? The only thing we can do is point to instance after instance where what we take to be foundational work leads to important transformations of a field (Eilenberg-Steenrod for alg. top., Grothendieck for alg. geom., etc.). Even so, someone can say that the primary issue is establishing the strength necessary to prove something.
I’m not so sure we should follow Lawvere’s designation ’ Bolzano-Frege-Peano-Russell-style foundations’. Frege certainly though that his Begriffsschrift would allow the formation of natural, fruitful concepts, i.e., his calculus was designed to be practical as well as secure (gap-free). I wonder if we can think of a different name. it needs to cover reverse mathematics, but also that drive to find a single system strong enough for everything.
You evidently didn’t participate in the great FOM discussion.
I didn’t, but I keep hearing you and Todd and others tell stories of it, so I have a rough idea.
We may agree that a foundation of a field should shape its fundamental concepts, but if Friedman or Simpson say ’No’, what are we going to do?
Sure, but I thought Toby argued for something more concrete, which we can objectively evaluate: he said he would reject HoTT as a foundation because it is proof-theoretically stronger than necessary.
Right now it seems to me that this is only true if “necessary” means “derives almost all undergraduate mathematics”. So I would in principle enjoy see discussion of the following concrete question: is dependent type theory “unnecessarily strong”, proof-theoretically, also for the big geometric theorems, say
Atiyah-Singer,
Pontryagin-Thom,
geometric Langlands,
Galatius-Madsen-Tillmann-Weiss
(to pick some random examples that come to mind)?
What would Friedman say about these theorems? Which foundational system would he prefer in order to prove them?
Just irrespective of taste. I would just like to know how far that game with “weak systems” really goes. If it goes that far, I’ll still not enjoy it, but I’d be impressed and happy to know about it. If it doesn’t go that far, then I would think it is a kind of vain exercise and “foundations of mathematics” a dubious term for it, irrespective of taste of style. (It would then be a bit like those texts we see appear proposing a “foundation of quantum physics” and then when you look at what they write it’s just all about quantum mechanics only.)
I’m not so sure we should follow Lawvere’s designation ’ Bolzano-Frege-Peano-Russell-style foundations’.
Please change it! I just put in there something. You and others here know much more about this than I do. Please improve the entry to your heart’s content. I just wanted there to be some lead-in paragraph.
I’m sure that for any maths you care about, there will some surprisingly weak system in which it can be proved. Evidence is suggesting Fermat’s Last Theorem is provable in something very weak, see McLarty’s paper.
But Fermat’s last theorem is a statement about the integers. SOA is natively speaking integers. From Toby’s comments above, the exercise of proving things in SOA boils down to reformulating every mathematical definition in terms of integers.
But as Toby desribes above, one already has to bend over backwards to formulate something like the Gauss-Bonnet theorem in terms of this, which is about continuous and smooth (not to say cohesive) structures.
Can one even state the Galatius-Tillman-Madsen-Weiss theorem in something like SOA?
Re 40,
Please change it!
OK, I’ve opted for ’proof-theoretic’ foundations.
By the way, speaking of ’practical foundations’, there’s a book being written by Robert Harper at Carnegie Mellon University, called Practical Foundations for Programming Languages. Perhaps you met him when you talked there, since he works on Homotopy type theory.
He also runs a blog – Existential Type. Here’s a post you may enjoy The Holy Trinity.
Oh, just saw you have written a page on him. Still you may enjoy that post.
Thanks for the link! I hadn’t see this. This is nice. We already have all the relevant information on the Lab, but maybe this is a good occasion to bundle it in one entry computational trinitarianism.
Its axioms (or type formation rules) are really just the bare essence of thought: there are types, we can take their sum and product, and there are identities. Period. Compared to that elegance, the axioms of SOA are a sad mess.
It’s interesting that you should say this! When Martin-Löf began lecturing about his type theory, logicians complained that it was a sad mess, compared to the elegance of first-order logic and material set theory (based on a single binary predicate, how elegant is that !?). I find both HoTT and SOA natural, which I think just means that I understand the motivations that went into each of them. (Also, Wikipedia’s list of axioms for SOA is a bit overdetermined; much of these are redundant but helpful to have when you consider weak subsystems.)
By the way, as you know, sums, products, and identities aren’t enough for mathematics; we also need recursion (and ideally corecursion). This requires W-types (and M-types), which I don’t think are quite as elegant as the other constructions. SOA is simply the working out of one particular recursive structure: the set of natural numbers. (And although the history obscures this, ZF is the working out of another particular recursive structure: the initial algebra of the covariant power set functor.) That so much mathematics can be encoded into this, which is a very familiar structure to many people, is interesting, even though it’s not the sort of foundation that I’d really like to work with.
Also by the way, I hope that it’s clear that my endorsement of EFA in #24 is facetious. (And among the weak fragments of SOA, the only thing special about EFA itself is that it was the weakest one that I found in a five-minute search for weak fragments that could still encode nontrivial mathematics.) Obviously HoTT is superior from a practical standpoint. The earnest point of #24 is just that I don’t believe in absolute answers.
To me, the “necessary strength” of a good foundations of mathematics is that it gives us the deep results about our world, say a formalization and proof of the mass gap conjecture
That’s a nice, useful standard.
I don’t know exactly what goes into this conjecture, but looking at the classification of compact simple Lie groups, and knowing that the structures in constructive QFT are distributions, dual to continuous functions, I think that it ought to be possible to formulate this in 3rd-order arithmetic. I’m not so sure about 2nd-order arithmetic; I wouldn’t be surprised, but I don’t know one would do it. (As for whether there’s a proof in any of these systems, if I knew that there was one, then I’d be a million dollars richer.)
For one thing, logic is taken by some to include inductive logic
Well, inductive logic done correctly is simply probability theory.
[ after posting I see that I have been overlapping with 2 further replies – this here was writtn in reaction to #45 ]
Thanks, that’s a very helpful comment, indeed.
I’d still like to hear thoughts on the question: “What kind of theory can formalize the Galatius-Tillman-Madsen-Weiss theorem”? Or similar. While I do appreciate your disbelive in absolute answers, I also believe in constraining the moduli space of admissible answers by using all available data points.
Is the GTMW Theorem the Main Theorem of this paper? Looking at this, I think that the statement is quite concrete and can be encoded easily into SOA, although it would probably take me all day to do it. As for the proof, I don’t know; but in the spirit of Friedman’s grand conjecture (which doesn’t actually apply to second-order statements like this), I would attribute to him the conjecture Yes.
Is the GTMW Theorem the Main Theorem of this paper?
Yes, that’s what I mean.
can be encoded easily into SOA
Hm. Okay. Hm…
It’s probably just historical dumb luck that reverse mathematics is the study of fragments of SOA rather than the study of fragments of something like CZF. I should probably look at that paper cited in #27 that relates SOA to CZF + separation; I’d like to know if the interpretations of each in the other come at all close to preserving meaning. (And then CZF + separation can be replaced with the theory of a well-pointed --pretopos with fullness, separation, and collection.)
Note that CZF is easily capable of writing down the theorems that you’ve been asking about, although (being constructive) it might well be unable to prove them (even the ones with proofs). I just don’t know if its way of writing them down translates into anything like how SOA might write them down. (Adding excluded middle to CZF strengthens it considerably, so using ETCS would be cheating.)
Re #42, McLarty is arguing about the Wiles proof of FLT, so has to capture the EGA/SGA kitback used by him. I don’t think it’s just one of those conservativeness results: if P can be expressed in X, and proved in X+Y, then it can already be proved in X, but I’m never going to do it because the unfolding would render it impossibly long. But I haven’t followed this closely, being a practical foundations kind of person.
Maybe I’m missing something, but I can’t see how this can take precedence over penetrating the conceptual heart of what Grothendieck was up to. Of course, McLarty has worked on this too. But there’s a job to do in seeing whether that conceptual heart is illuminated by homotopy type theory. Then there’s the small matter of whether Mochizuki has struck gold developing Grothendieck’s anabelian geometry.
McLarty has shown that one can define derived functor cohomology of (I think) a ringed topos in a weak set theory which is equiconsistent with finite order arithmetic. More recently he has shown that étale cohomology can be defined for schemes in third order arithmetic via similar set theoretical tricks. He has also given structural versions. This is all very global. The aim is to look at the specific cases when étale cohomology is used in a proof of the relevant part of the modularity theorem and show that less foundations are needed for those cases. For instance, elliptic curves are very far from generic schemes.
This requires W-types (and M-types), which I don’t think are quite as elegant as the other constructions.
I’m surprised to hear you say that. What do you think about inductive types a la Coq, which generalize both W-types and sums, (positive) products, and identity types? And what about impredicative polymorphism like in System F, from which you can define inductive and coinductive types (albeit without a dependent eliminator)?
What do you think about inductive types a la Coq
I think that this is a more elegant approach than Martin-Löf’s, but it would be conceptually simper (if only it were practically possible!) to limit to the constructions that Urs actually listed.
And what about impredicative polymorphism like in System F
I don’t know that very well; I’ve always assumed from the name that it’s terribly strong, but that might not be accurate.
I don’t think System F is all that strong – certainly not as strong as ZF, say. You can prove its consistency with logical relations.
1 to 56 of 56