Skip to the Main Content

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

March 31, 2016

Foundations of Mathematics

Posted by John Baez

Roux Cody recently posted an interesting article complaining about FOM — the foundations of mathematics mailing list:

Cody argued that type theory and especially homotopy type theory don’t get a fair hearing on this list, which focuses on traditional set-theoretic foundations.

This will come as no surprise to people who have posted about category-theoretic foundations on this list. But the discussion became more interesting when Harvey Friedman, the person Cody was implicitly complaining about, joined in. Friedman is a famous logician who posts frequently on Foundations of Mathematics. He explained his “sieve” — his procedure for deciding what topics are worth studying further — and why this sieve has so far filtered out homotopy type theory.

This made me think — and not for the first time — about why different communities with different attitudes toward “foundations” have trouble understanding each other. They argue, but the arguments aren’t productive, because they talk past each other.

After much discussion, Mario Carneiro wrote:

So I avoid any notion of “standard foundations of mathematcs”, and prefer a multi-foundational approach, where the “true” theorems are those that make sense in any (and hence all) foundational systems.

I replied:

One nice thing your comment clarifies is that different people have very different attitudes toward foundations, which need to be discussed before true communication about the details can occur.

Harvey Friedman seems to believe that foundations should be “simple” (a concept that begs further explication) and sufficiently powerful to formalize all, or perhaps most, mathematics. For example, he wrote:

When I go to the IAS and ask in person where the most elementary place is that there is a real problem in formalizing mathematics using the standard f.o.m….

as part of an explanation of his “sieve”.

Most people interested in categorical foundations have a completely different attitude. This is why nothing they do will ever pass through Friedman’s sieve.

First, they — I might even say “we” — want an approach to mathematics that formalizes how modern mathematicians actually think, with a minimum of arbitrary “encoding”. For us, it is unsatisfactory to be told that 3\sqrt{-3} is a set. In ZFC it is encoded as a set, and it’s very good that this is possible, but mathematicians don’t usually think of complex numbers as sets, and if you repeatedly raised your hand and asked what are the members of various complex numbers, you’d be laughed out of a seminar.

Second, when I speak of “how modern mathematicians think”, this is not a monolithic thing: there are different historical strata that need to be considered. There seems to be a huge divide between people like Lawvere, who were content with topoi, and people who are deeply involved in the homotopification of mathematics, for whom anything short of an (,1)(\infty,1)-topos seems insanely restrictive. Homotopy type theory is mainly appealing to the latter people.

Anyone who has not been keeping up with modern mathematics will not understand what I mean by “homotopification”. Yuri Manin explained it very nicely in an interview:

But fundamental psychological changes also occur. Nowadays these changes take the form of complicated theories and theorems, through which it turns out that the place of old forms and structures, for example, the natural numbers, is taken by some geometric, right-brain objects. Instead of sets, clouds of discrete elements, we envisage some sorts of vague spaces, which can be very severely deformed, mapped one to another, and all the while the specific space is not important, but only the space up to deformation. If we really want to return to discrete objects, we see continuous components, the pieces whose form or even dimension does not matter. Earlier, all these spaces were thought of as Cantor sets with topology, their maps were Cantor maps, some of them were homotopies that should have been factored out, and so on.

I am pretty strongly convinced that there is an ongoing reversal in the collective consciousness of mathematicians: the right hemispherical and homotopical picture of the world becomes the basic intuition, and if you want to get a discrete set, then you pass to the set of connected components of a space defined only up to homotopy. That is, the Cantor points become continuous components, or attractors, and so on — almost from the start. Cantor’s problems of the infinite recede to the background: from the very start, our images are so infinite that if you want to make something finite out of them, you must divide them by another infinity.

This will probably sound vague and mysterious to people who haven’t learned homotopy theory and haven’t seen how it’s transforming algebra (e.g. the so-called “brave new algebra”), geometry (“higher gauge theory”) and other subjects. Until the textbooks are written, to truly understand this ongoing revolution one must participate in it.

Again, all this stuff can be formalized in ZFC, but only at the cost of arbitrary encodings that do violence to the essence of the ideas. A homotopy type can be encoded as a topological space, or as a simplicial set, or as a cubical set, or as a globular \infty-groupoid… but all of these do some violence to the basic idea, which is — as Manin points out — something much more primitive and visual in nature. A homotopy type is a very flexible blob, not made of points.

Third, because people interested in categorical foundations are interested in formalizing mathematics in a way that fits how mathematicians actually think, and different mathematicians think in different ways at different times, we tend to prefer what you call a “multi-foundational” approach. Personally I don’t think the metaphor of “foundations” is even appropriate for this approach. I prefer a word like “entrance”. A building has one foundation, which holds up everything else. But mathematics doesn’t need anything to hold it up: there is no “gravity” that pulls mathematics down and makes it collapse. What mathematics needs is “entrances”: ways to get in. And it would be very inconvenient to have just one entrance.

Posted at March 31, 2016 7:43 PM UTC

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

83 Comments & 0 Trackbacks

Re: Foundations of Mathematics

Just in support of your final comment regarding categorical foundations, I feel that indeed many category theorists think in a more ‘modular way’ about foundations: one has a certain kind of category (with products, say), and one explores what one can do in such a category.

Thus one’s structured category (doctrine), is playing essentially the same role as a ‘foundation’, it is just that one is not (usually) claiming that one can formalise all of mathematics in it: one just formalises the little bit one is interested in for a particular purpose.

This reduces a ‘foundation’ to something which allows one to ‘plug in’ one’s modules (i.e. express the notion of a category with products, or whatever). This can be done in any reasonable kind of foundations, whether set theoretic, type theoretic, or even (conceivably) pictorial, so is a more flexible and more robust point of view, rather Unix-like!

Of course, one can take this modular point of view further, and work not just with categories, but with 2-categories, fibred categories, and so on. So perhaps might a 2-categorical modular level in between the categorical one and the foundational level, etc.

Posted by: Richard Williamson on March 31, 2016 8:56 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I agree that this ‘modular’ outlook is fundamental to the categorical way of thinking! Your point is just as important as any of the points I made. It explains why ‘foundations’ is an inappropriate metaphor for the way category theorists want to organize mathematics.

And here’s a related point. I believe many people who like set-theoretic foundations still secretly wish for axioms that are categorical — in a sense that has little to do with category theory. Axioms are ‘categorical’ if all models of those axioms are isomorphic: that is, roughly, the axioms uniquely determine the structure they’re axiomatizing.

Of course, we know that no reasonably powerful axioms of set theory can be categorical. Nonetheless some people still speak of ‘the’ universe of sets, as if there were some unique structure that we are seeking to axiomatize. They also argue, at times, about which axioms are ‘true’.

In geometry, this attitude was made obsolete long ago by the discovery of non-Euclidean geometries. But in set theory, despite Gödel, it persists.

Thanks to the ‘modular’ approach you describe, category theorists have a very different attitude. We are happy with axioms that have many dramatically different models. If we speak of ‘a category with finite products’, or ‘a topos with natural numbers object’, we consider it a feature, not a bug, that these axioms apply to many different structures.

We are not trying to axiomatize ‘the universe’. We are trying to specify a kind of context in which one can do a certain class of interesting things.

Posted by: John Baez on March 31, 2016 9:10 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Yes, there’s a lot of “speaking past each other” on FOM, and amongst those with different opinions about foundations!

However, that said - first, I’m fairly sure that Friedman isn’t a set-theoretic reductionist. My impression is that he’s really a kind of finitist, a bit like Hilbert,

Mathematical reality = FMOFMO.

i.e., all “finite mathematical objects” (of course, then mathematical reality it itself not finite! but one can get around that by treating it as potentially infinite, and not as a “completed infinity”. The result of doing this is probably something close to Solomon Feferman’s predicativism).

Suppose we define set-theoretic reductionism to be the claim,

Mathematical reality = VV.

I.e., the cumulative von Neumann hierarchy VV (or maybe a generalized modification, V(U)V(U), built up over a starting set UU of urelements).

Of course, this implies that 3 is a set. But which one? Hmmm. Set-theoretic reductionists just debunk this question by replying that it doesn’t matter. (See Quine on this; Quine goes structural. I believe Burgess goes structural as well in his recent book, but I’m less sure.)

The second thing is that I also think Friedman advocates, as do many logicians, some kind of Interpretationism,

Mathematical theories which can be interpreted into each other are basically the same theory.

The best example of this I think is that the theories

i) Peano arithmetic: PAPA

ii) ZF with negation of infinity: ZFInf+¬InfZF - Inf + \neg Inf

are interpretable into each other. Richard Kaye and Tin Lok Wong have a nice paper on this, from 2006,

http://www.logic.univie.ac.at/~wongt9/papers/finitesettheory.pdf

In other words, although PA and “finite set theory” are practically very different, it makes no genuine ontological difference whether one believes in numbers, or finite sets, or finite mathematical objects. They can all be “coded” as each other.

The third thing I’d mention is that I think Friedman said sometime ago one could formalize things using many-sorted first-order logic and that this is basically what mathematicians are using, although they don’t quite know it. Many-sorted first-order logic is intimately connected with type theory, although I can’t pretend to be able to state the exact connection. So perhaps Friedman is actually sympathetic to the type theory stuff; he would just express it differently.

Posted by: Jeffrey Ketland on April 1, 2016 10:13 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Mathematical theories which can be interpreted into each other are basically the same theory.

Actually from what he has said on G+ and over the years, I strongly doubt Friedman holds this position: he explicitly wants ‘philosophical coherence’ for his foundational frameworks, and of two frameworks that are equiconsistent, bi-interpretable and so on, the one that is ‘more coherent’ is better – at least I so read his statements that way. In particular, no matter that ETCS+R is exactly equivalent to ZFC, it is ZFC that is ‘superior’, for purely philosophical reasons.

Posted by: David Roberts on April 2, 2016 3:06 AM | Permalink | Reply to this

Re: Foundations of Mathematics

To be honest, it’s really bizarre to me that otherwise sensible mathematicians will proudly declare that they believe in some kind of “unique/objective reality” about sets or anything in mathematics. It sounds like they are still in denial about Godel’s incompleteness theorem, even 85 years afterwards. Is there something to this point of view that I’m missing?

Posted by: Mike Shulman on April 2, 2016 4:10 AM | Permalink | Reply to this

Re: Foundations of Mathematics

It’s possible to believe that the axioms of set theory are abstracting actual truths about the world, rather than thinking of them as simply the sentences of the formal system ZFC. JP Mayberry discusses this a lot in his remarkable Cambridge EOM book “Foundations of Mathematics in the Theory of Sets.” In particular he makes the point that it’s not coherent to identify your foundation of math with a certain first-order logical theory, because to specify what a first-order theory you already need some set theory in place: what exactly is a finite string of symbols? I have no idea whether professional set theorists would assent to this, but it seems like a plausible explanation for continuing belief in one true set theory: some facts are actually true about all sets of objects in the world, and some aren’t, and there’s no problem that we can’t expect any fixed first order theory to encompass all such facts. Of course, it’s a pretty fraught question how we could possibly decide whether e.g. CH or its negation is really true, although I’ve heard Hugh Woodin has ideas that could establish this. But Mayberry also proposes that this is mostly a problem with accepting the axiom of infinity.

Posted by: Kevin Carlson on April 9, 2016 7:29 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Thanks for the pointer! I’m probably not interested enough to go track down and read a book that I’ll almost certainly disagree with, though. (-:O I don’t see how one can reasonably consider statement about infinite sets – in particular, uncountable infinite sets – to have anything to do with collections of objects.

And while it may require some set theory to make sense of the general notion of first-order theory, I don’t think that is true for a specific first order theory whose axioms we can simply list. If we want to talk about the set of all consequences of those axioms, then yes of course we need some set theory, but we can consider the axioms themselves, along with the rules of inference, without any background theory. So statements that refer implicitly or explicitly to that set are nonsense without a background theory, like ‘X is not provable in ZFC’, but theclaim that a particular statement is a theorem, which is what we need for formalizing mathematics in practice, can be established by giving a proof. That is, the general notion of ‘natural number’ may be unclear, but any specific natural number I write down isn’t (unless you are an ultrafinitist!).

Posted by: Mike Shulman on April 11, 2016 7:15 AM | Permalink | Reply to this

Re: Foundations of Mathematics

“That is, the general notion of ‘natural number’ may be unclear, but any specific natural number I write down isn’t”

Can you rewrite that assertion so that the only numbers referenced are specific numbers? If not, then your assertion declares its own “unclearness”. Yet, you presumably understand your own claim, when suggests that it is false.

Posted by: Tyrrell McAllister on May 17, 2016 9:28 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Not really? Many simple statements about unclear things are clear.

Posted by: christopher andrew upshaw on May 25, 2016 9:51 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Mike,

Given that Friedman’s speciality is incompleteness, and delights in finding new formulations of simple-sounding statements about countable objects provable only with large cardinal assumptions, it is clear he is approaching things from a philosophical point of view, where you simply cannot prove any particular view right or wrong. It doesn’t help for a mathematician that a lot of the justification of his views are couched in natural language with the non-formal meaning (eg using “perfect [X/Y/Z]” to describe foundational frameworks or structures, and not in any mathematical sense).

Posted by: David Roberts on April 2, 2016 8:18 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Surely there exist beliefs that can be proven wrong even from a philosophical point of view, like a belief that 0=10=1, or that the Gödel sentence is provable.

Posted by: Mike Shulman on April 2, 2016 10:24 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Gödel himself showed how to prove it. Let SS be a theory extending IΣ 1I \Sigma_1 with finitely many axioms and axiom schemes. If SS is consistent, then SGS \nvdash G. Next, let Tr(S)Tr(S) be what Feferman calls the “ordinary truth theory” over SS. Then Tr(S)GTr(S) \vdash G. For more details, see

Feferman, S. 1991. “Reflecting on Incompleteness”, JSL 56.

http://projecteuclid.org/euclid.jsl/1183743549

Posted by: Jeffrey Ketland on April 2, 2016 4:32 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I assumed it would be obvious that when I said “the Godel sentence is provable” I meant something more precise like “the Godel sentence for theory TT is provable in theory TT, assuming TT is consistent”.

Posted by: Mike Shulman on April 2, 2016 9:50 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Ok, my bad! But the provability of consistency sentences is extremely interesting. E.g., IΣ n+1Con(IΣ n)I \Sigma_{n+1} \vdash Con(I \Sigma_n), and PACon(S)PA \vdash Con(S), for any finitely axiomatized subtheory SS of PAPA. And all kinds of fancy refinements, e.g., involving how much induction is need to prove Con(T)Con(T) (which gives TT’s proof-theoretic ordinal), and how much proofs get shortened in stronger theories (“speed-up”), which is a fine-grained version of incompleteness.

Posted by: Jeffrey Ketland on April 2, 2016 10:42 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I think this is one of the most important, and least appreciated, aspects of the modern approach to “foundations”. As I said on the G+ post, one of my favorite metaphors for “foundations” is that of a programming language: a given language can be interpreted or compiled to many different architectures, and in particular can be translated into many other languages. This point of view doesn’t require category theory, indeed you can do many of the same things with ZFC-like theories; but it just so happens that the interesting “nonstandard” models (like a lot of things in mathematics) tend to arise in practice as categories, so that categorical foundations are more congenial to a modular approach than set-theoretic ones.

Posted by: Mike Shulman on April 1, 2016 9:35 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Thanks a lot for this formulation. It seems to me that now people go to the TT world from the modular (doctrinal) CT world, and I feel it’s a big loss. Another big loss is that CT people beliewe to the logical verification where they could suggest much more modular purely-algebraic one.

Posted by: Osman on April 23, 2016 12:08 PM | Permalink | Reply to this

Re: Foundations of Mathematics

There’s another aspect of the HoTT story that deserves to be mentioned. A lot of the conversation about foundations centers around the formalization of existing mathematics. But a foundation of mathematics can be more than that: it can enable us to do new mathematics that didn’t exist previously. Set theory certainly did that at its inception: why else would Hilbert have said that Cantor created a paradise for mathematicians? The most exciting thing about HoTT for me is not that it can formalize existing mathematics — we already know lots of ways to do that, including in a category-theoretic and modular way — but that it opens up entirely new worlds of mathematics such as synthetic homotopy theory and cohesive homotopy theory. These worlds are certainly inspired and guided by areas of classical mathematics, but they have their own flavor, their own techniques and insights, and their own problems. They are a different way of representing the “homotopified” worlds of modern mathematics, which perhaps captures some of our intuitions that the encoding into ZFC destroys, but at the same time requires us to learn new intuitions as well. We are still beginners in our understanding of these worlds, and I think that’s an exciting time of history to be at.

Posted by: Mike Shulman on April 1, 2016 9:44 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Mike wrote:

Set theory certainly did that at its inception: why else would Hilbert have said that Cantor created a paradise for mathematicians?

I forgot that the verb was created. “Creating a paradise” is a hugely religious metaphor, making Cantor into a god figure.

We are still beginners in our understanding of these worlds, and I think that’s an exciting time of history to be at.

I agree. Logic is the most fun when developing it lets you think new thoughts, not just say old ones more carefully.

Hilbert space, the extension of Euclidean geometry to the infinite-dimensional case, was a great example: Cantor helps make infinity into a precise concept mathematicians can study, then Hilbert says “okay, let’s do geometry in infinite-dimensional space!”

Today, other equally marvelous new worlds are waiting to be explored.

Posted by: John Baez on April 2, 2016 12:07 AM | Permalink | Reply to this

Re: Foundations of Mathematics

According to Wikipedia, the actual word was geschaffen: “to create; to produce; to make; to cause; to establish”.

Posted by: Mike Shulman on April 2, 2016 11:03 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Schöpfen” is the verb that is usually used in the biblical context, but also in artistic context. In everyday context one uses machen. “Shaffen” is somewhere in between these two, I think. It has also an additional meaning, something like “accomplish”.

Posted by: Gejza Jenča on April 2, 2016 1:11 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Mike wrote:

To be honest, it’s really bizarre to me that otherwise sensible mathematicians will proudly declare that they believe in some kind of “unique/objective reality” about sets or anything in mathematics.

I suppose we should find some of these mathematicians and talk to them.

It sounds like they are still in denial about Gödel’s incompleteness theorem, even 85 years afterwards. Is there something to this point of view that I’m missing?

Let me play devil’s advocate here.

The original proof of Gödel’s theorem doesn’t do much to shake the belief that there’s a “standard model” of the natural numbers, and thus an objective truth value to statements in the language of arithmetic, even if these statements are undecidable in PAPA. After all, the Gödel sentence

GG = “I am unprovable in PA”,

while apparently undecidable in PAPA, is still widely agreed to be true. So even though there are models of PAPA where GG is not satisfied, people are happy to consider those models “nonstandard”: not what we really mean when we’re talking about the natural numbers.

So, here’s a challenge. What’s a sentence SS in the language of arithmetic such that:

1) we can prove (using some reasonable assumptions) that SS is undecidable in PAPA, and

2) many mathematicians might be willing to admit SS has no objective truth value.

The second criterion is fuzzy. But here are some examples.

Most mathematicians agree that GG is “true” and that Con(PA)Con(PA) is “true”, so they don’t obey criterion 2 very well.

If we were doing ZFC rather than PA, I’d say that the continuum hypothesis obeys criterion 2. Sure, some mathematicians might argue that that continuum hypothesis is “true”, and definitely some good mathematicians have argued that it’s “false.” But I think a lot of us would say there’s no “fact of the matter” here. We’re about equally happy to study set theory assuming the continuum hypothesis as assuming its negation. It feels more like studying abelian groups versus nonabelian groups: a choice where both alternatives are interesting.

So: what’s a statement in the language of arithmetic where a lot of people might agree there’s no “fact of the matter” as to whether it’s true?

Posted by: John Baez on April 2, 2016 8:02 PM | Permalink | Reply to this

Re: Foundations of Mathematics

After all, the Gödel sentence… while unprovable in PA, is still widely agreed to be true. So even though there are models of PA where G is not satisfied, people are happy to consider those models “nonstandard”: not what we really mean when we’re talking about the natural numbers.

To be honest, I don’t even get this. What is it that makes people believe that there is a “real” set of natural numbers out there? What does that even mean?

Posted by: Mike Shulman on April 2, 2016 10:01 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I didn’t say anything about a set of natural numbers “out there”. Out where? And I don’t think bringing up that question will help, even if you’re trying to ridicule it: it’s a notorious tar pit.

I was trying to push the conversation in a more interesting direction. It seems that many mathematicians believe that a statement like the Gödel sentence, while unprovable in PA, is “true”. After all, it says it’s unprovable, and it is.

Thus, these mathematicians argue, models of PA in which it doesn’t hold can’t be “standard”. In other words, they obey the axioms, but they aren’t what we were trying to talk about when we wrote down those axioms.

One could feel this way and believe there’s a unique “standard” model of PA, or maybe just that some models are obviously “nonstandard”: i.e., weird.

I think the best way to defeat the presumption that there’s a unique standard model is to find some sentences SS that are not only undecidable in PA, but for which intelligent people can easily disagree about whether SS or ¬S\not S is a better axiom to add to PA.

Posted by: John Baez on April 2, 2016 11:14 PM | Permalink | Reply to this

Re: Foundations of Mathematics

You said

The original proof of Gödel’s theorem doesn’t do much to shake the belief that there’s a “standard model” of the natural numbers.

That’s the model I was referring to with “out there”. I’m sorry if the word “real” brought up different connotations than “standard” (though I don’t quite understand the difference). If there’s a “standard” model then where does it live? Is that question somehow less problematic than the question of where the “real” natural numbers might live? Mathematically, any model of a theory must be constructed within some other theory, and certainly within any given model MM of (say) ZFC there is a model of the natural numbers that’s “standard” relative to MM, but that just pushes the question back.

More importantly, even if there were a “standard” model, how could we know anything about it? That’s what I see as the relevance of Gödel’s theorem: no description of “the natural numbers” can be complete, so even if there were some unique standard notion of “the natural numbers”, we wouldn’t have any way of distinguishing it from lots of nonstandard ones — and hence there wouldn’t really be any meaning to calling it “standard”.

Posted by: Mike Shulman on April 3, 2016 4:04 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Mike wrote:

That’s what I see as the relevance of Gödel’s theorem: no description of “the natural numbers” can be complete, so even if there were some unique standard notion of “the natural numbers”, we wouldn’t have any way of distinguishing it from lots of nonstandard ones — and hence there wouldn’t really be any meaning to calling it “standard”.

I completely agree with you, so I wish you’d stop arguing.

I’m trying to push the discussion toward something a bit new. In the language of set theory we can write down sentences SS independent of ZFC such that some mathematicians strongly favor adding SS as an axiom, while other mathematicians strongly favor adding not(S)not(S). An example is the Continuum Hypothesis, but I can rattle off many more.

In such situations people eventually decide that models ZFC+SS and ZFC+not(S)ZFC+not(S) are both interesting, so they eventually stop worrying about whether SS holds in some mythical ‘standard’ model—though this has taken a shockingly long time.

However, I can’t rattle off examples of sentences SS in the language of arithmetic that are independent of PA such that some mathematicians strongly favor adding SS as an axiom while others strongly favor adding not(S)not(S).

Does anyone here know a good example?

For example, consider S=Con(PA)S = Con(PA). It’s independent of PA, but I’ve never heard of someone seriously suggesting that arithmetic would be better off if we supplemented PA by the axiom not(Con(PA))not(Con(PA)). People have certainly studied what would happen if we did… but they tend to do it with a sense of trying something naughty to see what happens.

Harvey Friedman has studied how large cardinal axioms SS allow us to prove seemingly down-to-earth sentences in arithmetic. For example, he’s recently described a fairly natural set that you can’t count using ZFC, but you can count using ZFC+SS for some such axiom.

But I’ve never seen him say “In PA+SPA+S we can prove this simple-sounding set has 6 elements, while in PA+SPA+S\prime we can prove it has 7”, where the set is of some mathematical interest independent of this logic problem, and neither SS nor SS\prime radically conflicts with most mathematicians’ intuitions about arithmetic.

Now, perhaps you think we shouldn’t have any intuitions about arithmetic other than what’s in PA. But sorry, I do! I’m utterly convinced that Hercules will always beat the Hydra, even though it’s unprovable in PA.

So, while I don’t believe in a standard model of PA, I still feel some models are “more standard” than others. I think it will be useful to find examples that really challenge this feeling—examples where we are really torn between alternatives.

Until we find these, I believe lots of mathematicians will believe there’s such a thing as the standard model. It’s like how some people believe there’s such a thing as “their ideal mate” until they can’t decide between two.

Posted by: John Baez on April 3, 2016 4:37 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Sorry, I misunderstood what you intended by your devil’s advocacy. (It’s been a long week here…) I agree it would be nice to have an example like the one you suggest, but I wish we didn’t need one, since finding one seems like a really hard problem!

For what it’s worth, I don’t have a problem with intuitions that go beyond PA (I have them too), or a feeling that some models are more or less standard than others, although I would prefer a less loaded word than “standard”. In other contexts we use words like “well-behaved” for models of axiom systems that accord with our intuition, and “pathological” for those that don’t.

Posted by: Mike Shulman on April 3, 2016 4:55 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Are you suggesting that “pathological” is somehow a less loaded adjective than “non-standard”? ;)

More constructively, I like the term “exotic”; see e.g. exotic spheres.

Posted by: Emily Riehl on April 4, 2016 5:46 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Maybe not according to some absolute measure of “loadedness”, but “pathological” is not loaded with the particular subtext of uniqueness that’s the problem here. Regarding some functions as “pathological” doesn’t imply that there is a unique well-behaved function!

Posted by: Mike Shulman on April 4, 2016 10:07 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Yes, we shouldn’t pathologize the merely exotic!

Sometimes what seems exotic at first may turn out to be ordinary. Nowhere differentiable functions are dense in the continuous functions. Yet when they were first discovered, Charles Hermite wrote:

I turn with terror and horror from this lamentable scourge of functions with no derivatives.

Such a negative attitude! I give him credit, though, for knowing the difference between terror and horror.

Henri Poincaré wrote:

Logic sometimes makes monsters. For half a century we have seen a mass of bizarre functions which appear to be forced to resemble as little as possible honest functions which serve some purpose. More of continuity, or less of continuity, more derivatives, and so forth. Indeed, from the point of view of logic, these strange functions are the most general; on the other hand those which one meets without searching for them, and which follow simple laws appear as a particular case which does not amount to more than a small corner.

In former times when one invented a new function it was for a practical purpose; today one invents them purposely to show up defects in the reasoning of our fathers and one will deduce from them only that.

If logic were the sole guide of the teacher, it would be necessary to begin with the most general functions, that is to say with the most bizarre. It is the beginner that would have to be set grappling with this teratologic museum.

Sometimes the exotic becomes ordinary over time; other times it becomes “exceptional”. Thank god nobody calls E 8\mathrm{E}_8 a “pathological Lie group”.

Posted by: John Baez on April 4, 2016 6:39 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I agree that finding a statement in arithmetic with no clear truth value is a very difficult problem, and as I’m sure you know, none of the “usual” problems with disputed truth values like choice or CH imply any arithmetic truths that ZF does not. I think Harvey’s quest for such a statement is very worthwhile, though I admit I don’t understand any of the actual details of his work.

Of course, consistency of powerful logics are arithmetic statements with non-obvious truth values, and the field of ordinal analysis aims at translating such statements into combinatorial statements which can be, perhaps, looked at through the lens of mathematical intuition.

Unfortunately, the negation of these statements involves subscribing to the belief that such theories are inconsistent, which even if you are a predicativist, seems like a really strong step. And since these are Π 1 0\Pi^0_1 statements, their negations are Σ 1 0\Sigma^0_1 statements, and so it seems weird to assume such a statement without expecting to have a concrete such number in hand.

Posted by: Cody on April 3, 2016 7:59 PM | Permalink | Reply to this

Re: Foundations of Mathematics

There are, of course, a host of natural conjectures in arithmetic that could be undecidable in PA. I think I’ve also heard it said that ‘most’ statements in arithmetic are undecidable in PA, but right now I’m having trouble remembering any precise theorem to that effect. (Is it even true in any sense?)

But it somehow seems hard to find a natural conjecture in arithmetic that can be proved undecidable in PA.

There are some Π 1 0\Pi_1^0 statements like the Goldbach conjecture that might (for all we know now) be undecidable in PA, but unfortunately we can’t prove this without simultaneously being convinced that these statements are ‘true’: if they’re ‘false’, we should be able to exhibit a counterexample and prove it’s a counterexample in PA!

So we need to climb a bit higher up the arithmetical hierarchy.

This, however, is not enough. For example, “every Goodstein sequence is eventually zero” is undecidable in PA. I don’t think that fact alone should convince us that every Goodstein sequence is indeed eventually zero. However, the usual proof of this claim, using transfinite induction up to ϵ 0\epsilon_0, fully convinces me that the claim is ‘true’… and, simultaneously, convinces me that transfinite induction up to ϵ 0\epsilon_0 is not a dubious principle, but in fact a completely believable one! Thus, all the models of arithmetic in which this principle fails have, to me, become ‘nonstandard’.

So we’d have to look harder to find a natural conjecture in arithmetic that’s not only undecidable in PA, but whose truth value seems debatable.

Someone must know a lot more about this than me.

Posted by: John Baez on April 4, 2016 7:07 PM | Permalink | Reply to this

Re: Foundations of Mathematics

There is a very old thread on Mathoverflow on this issue: http://mathoverflow.net/questions/4454

I argued that a positive fraction of arithmetic sentences are provable, because a positive fraction of grammatical arithmetic sentences are of the form “S, or 0=0” for some grammatical sentence S. People pointed out a paper of Calude and Jorgensen which seemed to say the reverse. I am periodically reminded of this thread, and annoyed that we never sorted it out.

Posted by: David Speyer on April 4, 2016 7:56 PM | Permalink | Reply to this

Re: Foundations of Mathematics

John,

I think I’ve also heard it said that ‘most’ statements in arithmetic are undecidable in PA, but right now I’m having trouble remembering any precise theorem to that effect. (Is it even true in any sense?)

Yes. The set of non-theorems of PA is not r.e.

In more detail, the set of theorems of PA is r.e.: i.e,, Σ 1\Sigma_1-definable:

ϕ\phi is a theorem of PA iff there is a Hilbert derivation in PAPA whose final term is ϕ\phi.

Arithmetized, this explicit definition becomes:

Prov PA(x)yProof PA(y,x)Prov_{PA}(x) \leftrightarrow \exists y Proof_{PA}(y,x)

The formula Proof PA(y,x)Proof_{PA}(y,x) (“yy is the code of a derivation in PA of a formula whose code is xx”) is recursive. Its existential quantification is therefore Σ 1\Sigma_1. Sets defined by Σ 1\Sigma_1-formulas are r.e.

The complement AA of the set of theorems of PA is therefore Π 1\Pi_1-definable.

But this set AA is not r.e. No TM enumerates all and only the non-theorems of PA. For if AA were r.e., it would be recursively axiomatizable (Craig’s Theorem) by some axiom system S. Then PA together with S would together yield a decision procedure for PA, which is impossible.

On the broader point, a version of Godel’s first incompleteness theorem is:

(G1) Th L A()Th_{L_A}(\mathbb{N}) is not r.e.

(I.e., the truth set for arithmetic is not r.e.) Also, this version follows from Tarski’s undefinability theorem,

(T) Th L A()Th_{L_A}(\mathbb{N}) is not definable in \mathbb{N}.

And in fact this holds for all “sufficiently rich” structures \mathcal{M}:

(T*) Th L()Th_{L}(\mathcal{M}) is not definable in \mathcal{M}.

(I believe this is the most beautiful diagonalization result in all mathematics. Suppose you have your favourite structure \mathcal{M}. Then the truth about it cannot be defined in it.)

Godel himself later reported that he first found Tarski’s theorem (T), and then he refined it to prove his own incompleteness results. Godel also later said that Tarski’s theorem is the “underlying reason” for incompleteness. I forgot exactly where (a letter, I think) and will try and remember.

Posted by: Jeffrey Ketland on April 4, 2016 9:05 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Gödel’s own explanation for incompleteness was given in his 1931 article:

… [T]he true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of higher types can be continued into the transfinite … while in any formal system at most denumerably many of them are available. For it can be shown that the undecidable propostions constructed here become decidable whenever higher types are added (e.g., of type ω\omega for the system P). An analogous situation prevails for the axiom system of set theory. (Gödel’s 1931, “On Formally Undecidable Propositions …”, footnote 48a.)

Gödel almost certainly knew by then that “the undecidable propositions … become decidable whenever higher types are added” because the relevant truth definition can be given when the higher types are added.

The other reference by Gödel to the “true reason” for incompleteness that I know of occurs in a letter to AW Burks, published in 1966 - where Gödel explained that the “true reason” for the incompleteness of formal systems is the undefinability of truth:

… the theorem of mine that von Neumann refers to is … the fact that a complete epistemological description of a language A cannot be given in the same language A, because the concept of truth of sentences in A cannot be defined in A. It is this theorem which is the true reason for the existence of undecidable proposotions containing arithmetic. (Gödel, letter to A.W. Burks, published in 1966.)

Alfred Tarski made a similar point in the Postscript to his 1936 article “The Concept of Truth in Formalized Languages”:

All sentences constructed according to Gödel’s method possess the property that it can be established whether they are true or false on the basis of the metatheory of higher order having a correct definition of truth. (Tarski 1936, p. 274)

Posted by: Jeffrey Ketland on April 5, 2016 2:53 PM | Permalink | Reply to this

Re: Foundations of Mathematics

John wrote:

I think I’ve also heard it said that ‘most’ statements in arithmetic are undecidable in PA, but right now I’m having trouble remembering any precise theorem to that effect. (Is it even true in any sense?)

Jeffrey wrote:

Yes. The set of non-theorems of PA is not r.e..

Yes. I don’t think this fact has any easy consequences for the question I asked, which concerned the density of the undecidable sentences as a subset of all the sentences of PA.

For example, looking at subsets of \mathbb{N}, I think I can cook up subsets SS \subseteq \mathbb{N} such that neither SS nor S cS^c are recursively enumerable and such that SS has very low density, e.g.:

lim n|S{1,,n}|n=0 \lim_{n \to \infty} \displaystyle{ \frac{ | S \cap \{1, \dots, n\} | }{n} = 0 }

Simply take a set XX \subseteq \mathbb{N} such that neither XX nor X cX^c is recursively enumerable, and say that nSn \in S iff n=2 kn = 2^k and kXk \in X.

David Speyer has just shown that if T nT_n is the set of theorems of PA that are strings of nn symbols, while S nS_n is the set of sentences in the language of arithmetic that are strings of nn symbols, we have

limsup|T n||S n|>0 {\lim \, \sup} \; \displaystyle{\frac{|T_n|}{|S_n|} \; \gt \; 0 }

This eliminates one possible sense in which ‘almost all’ sentences are unprovable.

But I still believe a lot of sentences are undecidable. So, if U nU_n is the set of sentences with nn symbols that are neither provable nor disprovable in PA, I believe that

limsup|U n||S n|>0 {\lim \, \sup} \; \displaystyle{\frac{|U_n|}{|S_n|} \; \gt \; 0 }

This would be nice to show.

Posted by: John Baez on April 5, 2016 5:07 PM | Permalink | Reply to this

Re: Foundations of Mathematics

David wrote:

I argued that a positive fraction of arithmetic sentences are provable, because a positive fraction of grammatical arithmetic sentences are of the form “S, or 0=0” for some grammatical sentence S.

Let’s check, to make sure you’re not making a subtle mistake. Suppose the language of arithmetic has LL symbols and there are F(n)F(n) strings of nn symbols that are well-formed formulae.

If SS has nn symbols then S(0=0)S \vee (0=0) has n+6n+6. There are F(n+6)F(n+6) well-formed formulae with n+6n+6 symbols, and of these, F(n)F(n) are of the form S(0=0)S \vee (0=0). So, you’re claiming that

liminfF(n)F(n+6)>0 \lim \inf \; \frac{F(n)}{F(n+6)} \gt 0

Hmm… so how does the argument go?

Posted by: John Baez on April 5, 2016 2:12 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Since F(n)L nF(n) \leq L^n, we must have F(n+6)L 6F(n)F(n+6) \leq L^6 F(n) infinitely often, so that gives that the limsup is greater than L 6L^{-6}.

To say something about the liminf, we need to know something about our grammar. (For example, if all grammatical sentences have length 0mod50 \mod 5, it won’t be true, but then tagging on (0=0)\vee (0=0) isn’t grammatical.)

If our language is an unambiguous context free grammar, then the Chomsky–Schützenberger enumeration theorem tells us that nF(n)z n\sum_n F(n) z^n is an algebraic function of zz. We should be able to use standard methods for computing asymptotics of power series coefficients to get F(n)χ(n)n α/r nF(n) \sim \chi(n) n^{\alpha}/r^n where rr is the radius of convergence, α\alpha is a real number encoding the order of the branching/poles at the boundary and χ(n)\chi(n) is of the form j=1 ma jexp(inθ j)\sum_{j=1}^m a_j \exp(i n \theta_j) for some real θ j\theta_j (so quasi-periodic). That quasi-periodic function is a nuisance, but I think I can wipe it out given a bit more thought and using that F(n+6)F(n)F(n+6) \geq F(n).

Posted by: David Speyer on April 5, 2016 2:59 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Nice! My mistake was thinking about the lim inf instead of the lim sup. It would be nice to study both.

I didn’t know the Chomsky–Schützenberger enumeration theorem. A nice blend of generating functions and grammar.

Posted by: John Baez on April 5, 2016 5:12 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Can somebody explain k-similarity in Friedman’s paper? (Definition 3.4). I’m finding it a little confusing.

Posted by: Craig on April 7, 2016 6:19 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Let me try to clarify the situation with regard to this crucially important matter for foundations of mathematics.

  1. From the standard set theoretic point of view, we have the so called preferred model of set theory normally written as (V,)(V,\in), where \in is membership.

  2. Set theorists generally believe, or like to wear the hat, that (V,)(V,\in) has an objective reality, and it is NOT to be thought of as some special construction within any more general framework. We can debate if this is the case, and if it is thought to be not the case, then is this “more general framework” really philosophically coherent, or is it a mirage, etcetera…… Not the topic of this post.

  3. Cantor raised his famous continuum hypothesis, usually written CH. Set theorists and others, notably Hilbert, tried to resolve this question within ZFC, and also with ZFC extended by strongly inaccessible cardinals, and measurable cardinals, and large cardinal hypotheses generally, and not only failed, but actually provably failed. In what sense?

  4. In the important sense that people found natural constructions of models of ZFC and more, other than (V,)(V,\in), in which they could prove that CH holds, and others in which they could prove that CH fails.

  5. There is a little bit of a fib in 4. Goedel constructed a very natural model of ZFC in which he showed that CH holds. Cohen constructed a very natural collection of continuumly many models of ZFC in which CH fails. Some refinements pretty naturally construct a countable family of countable models of ZFC in which CH fails. If algebraic models (Boolean valued models) are allowed, then Cohen did construct a single individual natural model of ZFC in which CH fails.

  6. It is apparently impossible to construct a single natural model of ZFC in which CH fails, like Goedel did for CH holding (in the usual sense, not allowing algebraic model). HOWEVER, the family of models of ZFC in which CH fails are ESSENTIALLY ALL EQUIVALENT TO EACH OTHER, AND SO THERE IS A GOOD SENSE IN WHICH COHEN ACTUALLY GAVE “ONE” NATURAL MODEL OF ZFC IN WHICH CH FAILS.

  7. This pattern repeats itself for ALL so called intensely set theoretic statements that we have studied. Namely, there is a natural single model of ZFC in which they hold, and a natural (essentially) single model of ZFC in which they fail. Sometimes we can eliminate “essentially”, but not in the case of CH.

  8. And people have argued in many situations in 7, which model or models do they accept as “correct” or “like the real one (V,)(V,\in)”, etcetera.

  9. I am painting in 1-8 a philosophically coherent picture of what generally is going on, but there are some subtle points known to experts that I have glossed over, and I would like them not to think I am cheating or that I am stupid.

  10. Now let’s come to statements that are not set theoretic, and in fact, reasonably concrete. This notion is subject to analysis in standard f.o.m. normally in terms of the standard complexity measures for mathematical statements. I don’t want to get into this crucially important part of standard f.o.m. in this posting.

  11. Suffice it to say this. First of all, so called arithmetic sentences are way way down lower than the intensely set theoretic statements referred to above, especially CH.

  12. The crucial point is this. IN ALL OF THE NATURAL CONSTRUCTIONS WE KNOW OF MODELS OF SET THEORY, AND ESPECIALLY THOSE THAT WE VIEW AS CANDIDATES FOR THE REAL (V,)(V,\in), WE KNOW A PRIORI THAT THEY ALL SATISFY THE EXACT SAME NON SET THEORETIC STATEMENTS. IN PARTICULAR, WE KNOW THAT THEY ALL SATISFY THE SAME ARITHMETIC STATEMENTS.

  13. So unlike the situation with CH, in dealing with arithmetic statements that might not be decided in ZFC, we are going to have to work with provability with extensions of ZFC, and not, like in the case of CH, go grab and lobby for some model of ZFC being preferred in some way.

  14. OK, so now we are looking at an arithmetic sentence, and its provability in various set theories (or, speaking of the devil, maybe in various alternative foundational frameworks, see below).

  15. So, like CH, maybe we are going to have the following situation. Alice’s set theory proves arithmetic sentence A is true, Bob’s set theory proves A is false. And then people “decide” which, if any, has a correct set theory.

  16. Well, here is what is actually going on. FOR ANY TWO SET THEORIES ANYBODY THINKS ARE NATURAL, WE (GENERALLY) KNOW THAT EITHER EVERY ARITHMETIC SENTENCE PROVABLE IN THE FIRST IS PROVABLE IN THE SECOND, OR EVERY ARITHMETIC SENTENCE PROVABLE IN THE SECOND IS PROVABLE IN THE FIRST.

  17. So the only actual criteria for choosing set theories with regard to arithmetic sentences (and more) that anybody can do anything with, is simply: which proves more of them - mine or yours?

  18. Therefore, given the path that we are on, WE ARE NEVER GOING TO DIFFER IN OUR OPINION OF THE TRUTH VALUE OF ANY ARITHMETICAL SENTENCES. WE WILL ONLY DIFFER AS TO WHETHER WE SHOULD ACCEPT THEM AS HAVING BEEN SETTLED.

  19. This phenom is intimately connected with the matter of INTERPRETATIONS BETWEEN THEORIES. In general, any interpretation of one natural set theory in another also immediately proves that every arithmetic sentences provable in the first is provable in the second.

  20. We have found out that for any two natural set theories, either the first is interpretable in the second, or the second is interpretable in the first.

  21. In fact, there is a stronger observed fundamental phenom. For any two natural set theories, either the first is interpretable in the second, or the first proves the consistency of the second.

  22. FURTHERMORE, seriously alternative foundational frameworks are not going to change this situation at all, as people are and want to continue establishing interpretations between them and roughly ZFC. So whatever good alternative foundational frameworks are, they are not coming to the rescue here.

  23. Another difference between set theoretic statements like CH and arithmetic sentences.

  24. Although there are tons of very natural set theoretic statements known to be independent of ZFC, there isn’t a single natural mathematical arithmetic statement known to be independent of ZFC. (For finite set theory, there are, Goodstein, Paris/Harrington, and pretty much superseded by the Adjacent Ramsey Theorem, and some others). None for ZFC except for one researcher, with the very latest being written up by him/her because the naturalness looks perfect.

  25. This is a very good place for me to stop.

Posted by: Harvey Friedman on April 5, 2016 4:24 AM | Permalink | Reply to this

Re: Foundations of Mathematics

I think this stuff is fascinating. I’m perfectly happy to “believe, or wear the hat, that (V,)(V, \in) has an objective reality”, and try to explore this magnificent structure… or, more realistically, cheer from the sidelines as others do so.

You mention some empirically observed, apparently profound, but I guess still rather mysterious phenomena in set theory, like this:

FOR ANY TWO SET THEORIES ANYBODY THINKS ARE NATURAL, WE (GENERALLY) KNOW THAT EITHER EVERY ARITHMETIC SENTENCE PROVABLE IN THE FIRST IS PROVABLE IN THE SECOND, OR EVERY ARITHMETIC SENTENCE PROVABLE IN THE SECOND IS PROVABLE IN THE FIRST.

and this:

In fact, there is a stronger observed fundamental phenom. For any two natural set theories, either the first is interpretable in the second, or the first proves the consistency of the second.

I’ve heard people say these things before, but I don’t know enough concrete details. Where can I read a nice overview of the results you’re alluding to?

Ideally someday we’d have some theorems that let us understand why — and under what precise conditions — the phenomena you describe occur. The objective reality of (V,)(V,\in) might count as some sort of explanation of these phenomena, but I’d prefer an explanation in terms of theorems, like:

Given set theories TT and TT' such that TT is not interpretable in TT' and the TT does not proves the consistency of TT', then at least one of them is ‘badly behaved’ (in some sense to be specified.)

Is there any hope of a theorem like this within our lifetimes?

Posted by: John Baez on April 6, 2016 7:43 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I always think about this issue. An example of what I mean by a crucial issue in f.o.m. The best prospect is at the moment quantitative, that is to look only at “simple” formal systems cast in a certain way, show that all of the interesting systems are mutually interpretable in a “simple” one, and then show that the phenom is true for “simple” systems. But for crucial issues anything like this, the only tools I am aware of are from heavy duty standard f.o.m. developments. I would be impressed and excited if any of the alternative foundations people could bring anything to the table for issues like this.

Posted by: Harvey Friedman on April 7, 2016 4:18 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I doubt people working on the frameworks I’m interested in — like category theory, homotopy type theory or \infty-topos theory — will contribute to the issues you’re mainly focused on. The reason is that they are thinking about other things. These other things are closer to my heart, because they have direct impact on mathematical physics, geometry, algebra, and topology. In short: as far the questions I usually think about, these other developments give more “bang for the buck”.

But nonetheless, I’m fascinated to learn more about what the quest to clarify our understanding of “the preferred (V,)(V,\in)” through large cardinal axioms and other methods. So I’ll ask again:

Where can I read a nice overview of the results you’re alluding to?

I know a bit of logic, so I can stand a fairly technical overview. But if there’s no good overview of current results readable by ‘ordinary mathematicians’, would you be interested in writing one, e.g. for the Notices of the AMS? (I can’t make unilateral decisions about this, but I do have some clout there.)

Posted by: John Baez on April 7, 2016 6:12 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I would greatly prefer it if people would use phrases like

foundations of applied mathematics foundations of mathematical physics foundations of algebraic topology foundations of category theory foundations of geometry (now this is something I have some unfinished work on) etcetera

than

foundations of mathematics.

I would also be nice if a few things were generally acknowledged:

  1. That by several orders of magnitudes, the most highly developed, deepest, successful, rich, foundations of anything is the standard foundations for mathematics.

  2. 1 is not because people who have developed it are so great (some of them are), but because foundations of mathematics is MUCH EASIER than foundations of physical science, music, etcetera. It is the first, and needs to be the first, being so comparatively trivial.

  3. Despite the fact that real f.o.m. is comparatively trivial, in order to make real progress in the foundations of practically anything else, especially physical science, music, etcetera, the many many long fought painful lessons that were learned and enormous hurdles that were overcome to get to real f.o.m., things that at a higher level we still struggle with and get nowhere, or almost nowhere - promise to eventually help jump start the developments to be in these other foundational efforts. Absorbing at a deep level what worked and didn’t work, and why it took so long to get where we are (roughly 1920 and beyond) could save hundreds of years in wandering around the desert when trying to seriously develop real foundations of other subjects.

  4. Of course, I am not talking about directly applying standard f.o.m., although some of that is certainly going to be illuminating. I’m talking about absorbing the genuine f.o.m. experience.

  5. In fact, I have found various kinds of physicists much more interested in standard f.o.m. than mathematicians. I think it may have something to do with how top physicists realize that at some fundamental level, they are completely lost foundationally. But my impressions here are not to be trusted.

  6. So I am content if it is generally recognized that some of the greatest and most powerful intellectual structures ever created (or discovered), and some of the most shocking revelations ever revealed have come out of standard f.o.m. And the expectation is that there will be yet much more powerful and yet much more shocking things to come in standard f.o.m.

Baez:

“Where can I read a nice overview of the results you’re alluding to?”

There are a number of quite different things that you could be referring to.

A. Taking the view that there is an objective reality (V,epsilon), and getting truth values of various well known problems. Well, the well known problems here are going to be intensely set theoretic, led by CH (continuum hypothesis). In my biased opinion, this is not going well by the grandiose standards I apply to everything. Of course, there is a credible community that legitimately draws salaries, and many are very clever. There is Solovay, Woodin, Martin, and the philosopher Koellner, in no particular order. Woodin already has written for the Notices. If I remember right, he retracted some of the positions he took there. There are also seriously knowledgeable scholars of this line, notably Aki Kanamori. Steel, also in the inner circle, has broken with the objective reality of (V,epsilon), causing a deep fracture. Woodin’s student, Hamkins, has broken even further away, tending to treat models of ZFC as an ordinary mathematical subject like the study of finite groups. I would recommend that you contact these guys to see about materials and the possibility of writing for the Notices. If I remember, there are a number of articles in the Stanford Encyclopedia by Koellner, who works very closely with Woodin. That is probably the best source for this line of taking (V,epsilon) to be the preferred objective reality, with statements like the CH being matter of fact.

B. Focusing on whether ZFC is sufficient to do all that we really care about in normal mathematics. The idea here is that normal mathematics is very far from being intensely set theoretic, and the crucial issue since 1930 is whether ZFC is limited for normal mathematics As a working approximation, I am talking about perfectly natural thematic arithmetic sentences - with an emphasis on Pi-0-1 sentences. At least one person now believes that a revolutionary sea change is brewing in various senses after a very long incremental effort. The goal here is to find examples that are sufficiently shocking to other than mathematical logicians (they are beyond being shocked) so as to create a feeling of being profoundly disturbed. I don’t have a good feel about how profoundly disturbing these brewing developments will be to the typical reflective mathematician. But I have no doubt that by the end of the century, this will have infected the whole of pure mathematics, and will be profoundly disturbing to everybody. Unfortunately, I won’t be here in 2100 to see this.

Posted by: Harvey Friedman on April 8, 2016 4:50 AM | Permalink | Reply to this

Re: Foundations of Mathematics

When people talk about “foundations of X” what do they mean?

To give you a sense of my background so that you could be merciful in your answer: I work in differential geometry and dynamical systems. Sometimes I care about the category of finite sets, which doesn’t exist in ZFC. So I resort to the standard work-arounds.

Posted by: Eugene Lerman on April 8, 2016 2:50 PM | Permalink | Reply to this

Re: Foundations of Mathematics

You might find the variant of ZFC, called NBG (von Neumann Bernays Goedel) class theory, usually with the axiom of choice like ZFC, convenient. Then we have the actual class of all finite sets = class of all finite classes. See, for you, conveniently, the finite classes are exactly the finite sets.

Well, there should be a contemporary philosophical literature on “foundations of X” but I think there isn’t, at least not a sufficiently interesting one.

One reason may be that there really aren’t good successful examples of X’s which have been given a good foundations. Although often the word “foundations” is meant in a comparatively limited informal sense, where it is difficult to codify. Like “important basic information before we really do something interesting and important”.

That’s of course not the sense in which I mean “foundations for mathematics”.

In real foundations, you expect to have

  1. A philosophically coherent description of the concepts of X that are going to be taken as undefined - i.e., as primitive, from which all other concepts are going to be defined.

  2. A listing of fundamental facts involving the primitives in 1 which are to be taken for granted and not derived. There should be a philosophically coherent justification given for these fundamental facts. Of course, this is going to fall short of a proof of these facts, otherwise they would be replaced by facts yet more fundamental.

  3. A philosophically coherent description of how inferences are to proceed. Of course, the universal default is the famous FOL=.

  4. A recasting of a representative sampling of fundamental developments in X in accordance with 1-3, as a test that one has sufficiently captured the essence of X, at least methodologically. In the case of math, ZFC doesn’t do anything with mathematical intuition, mental pictures, formulation of problems and conjectures, etcetera. But it does deal with the formulation of definitions, statements, and presentation of rigorous proofs.

I am completely open to the possibility that there might be genuine foundations which does not take the above exact form 1-4, or maybe some totally new idea of what a foundation is. But the standards for doing that are very high, and the standards for a totally new idea of what a foundation is has to be very very very high.

In particular, ZFC is totally inadequate to deal with quite a number of important mathematical matters, e.g., mental pictures. You can’t even do deep math without having clear mental pictures.

However, there is no chance that anybody is going to do a serious foundation of mental mathematical pictures without incorporating all of the standard f.o.m. that we know, and much more. After all, ZFC itself is based on a reasonably clear mental mathematical picture, and a very powerful and effective one indeed.

Posted by: Harvey Friedman on April 8, 2016 10:09 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I appreciate your response. It’s interesting.

Posted by: Eugene Lerman on April 9, 2016 2:22 AM | Permalink | Reply to this

Re: Foundations of Mathematics

You might find the variant of ZFC, called NBG (von Neumann Bernays Goedel) class theory, usually with the axiom of choice like ZFC, convenient.

Thank you for mentioning NBG. I agree that there are category theory books that try to work within that system. To me it doesn’t feel natural that there only two sorts of collections: sets and proper classes. In the context of category theory it feels more natural to keep taking collections of collections. And after one step or two of doing this, NBG is no better than ZFC.

At some point of my life I was unhappy about this and kept wishing for better foundations than NBG. Your reply makes me think that this is not coming any time soon.

Posted by: Eugene Lerman on April 9, 2016 2:42 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Eugene wrote:

To me it doesn’t feel natural that there only two sorts of collections: sets and proper classes. In the context of category theory it feels more natural to keep taking collections of collections. And after one step or two of doing this, NBG is no better than ZFC.

Of course — I’ll say this just in case someone doesn’t know — category theorists usually deal with this problem using ZFC plus the axiom of universes. A Grothendieck universe is roughly a set UU of sets that serves as a model of ZFC, so we can act like it’s ‘the’ universe of ‘all’ sets. The axiom of universes says that every set is in some universe.

This gives us a universe U 0U_0, a bigger universe U 1U_1 containing U 0U_0, an even bigger universe U 2U_2 containing U 1U_1, and so on. We can say sets in U 0U_0 are ‘small’, sets in U 1U_1 are ‘large’, sets in U 2U_2 are ‘2-large’, etc..

There is then an (n+1)(n+1)-large category of all nn-large categories, and we’re good to go!

It almost always doesn’t require much thought: you just carry around nn as an adjustable parameter (since its value doesn’t affect any interesting theorems in category theory), and increment it by 1 each time you need to say “the category of all the categories we’ve been talking about so far”.

By the way, the existence of a universe (or let’s say an uncountable universe, since some wimps allow the empty set to be a universe, or certain other countable sets) is equivalent to the existence of a strongly inaccessible cardinal. This is almost obvious; they are closely connected ideas.

Posted by: John Baez on April 9, 2016 3:19 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Is there a version of ETCS with with universes?

Posted by: Eugene Lerman on April 9, 2016 5:39 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Eugene: definitely! There’s of course work on universes in toposes (implicitly going back to work of Bénabou on internal toposes), see for instance this paper by Streicher. Given the rest of the axioms of ETCS, take definition 2.1 in the linked paper, and ask that every object is an ‘element of’ a universe. Since the data of a universe includes a generic family El:EUEl\colon E\to U, a set XX being an element of a universe means there is a map 1U1\to U such that the unique map X1X\to 1 is a pullback of ElEl along this map. See page 8 of Streicher’s paper for the idea of a countable sequence of nested universes.

Posted by: David Roberts on April 10, 2016 2:11 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Cool! Thanks.

Posted by: Eugene Lerman on April 10, 2016 2:19 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Speaking of Grothendieck and his axiom of universes, this is a nice summary of Colin McLarty’s work on the axiomatic underpinning’s of Fermat’s Last Theorem:

I’ll quote a chunk:

When Wiles finally proved the theorem in 1994, he used a deep connection between Fermat’s Last Theorem and algebraic geometry, a field in its infancy in Fermat’s time. Modern algebraic geometry was built using extraordinarily powerful tools developed in the mid-20th century by the mathematician Alexander Grothendieck that rely on an extra axiom in addition to those of standard mathematics — so Wiles’ proof did too.

Grothendieck introduced the axiom to deal with a pesky logical problem. His tools got much of their power through being extremely abstract. For example, instead of just considering the set of all whole numbers, Grothendieck also included the spaces defined by equations of whole numbers. (Think, for example, of the circles and parabolas and ellipses defined by equations in two variables). Then he threw in the set of all functions between such spaces, and so on, with one set building on another.

Set theory (that is, the standard axioms of mathematics) puts limits on how far this process can go. For example, there is no set of all sets, because a set of all sets would lead to logical difficulties like the famous Russell paradox: Imagine the set whose elements are precisely those sets that don’t contain themselves. Does it contain itself? Prepare yourself for some brain-twisting here: The answer can’t be yes, because then by its own definition it’s a set that doesn’t contain itself. But the answer can’t be no, either: If the set doesn’t contain itself, then it satisfies its own definition, so it does contain itself. Damned if you do, damned if you don’t!

With his sets built on sets built on sets, Grothendieck wanted to go into territory perilously close to this. So he created a new axiom that would allow him to use these very large sets of sets of sets while still keeping clear of paradox. This axiom posited the existence of a larger type of set called a “universe.” Grothendieck’s approach was fabulously successful, allowing him to prove one major theorem after another and laying the groundwork for modern algebraic geometry, among other fields — all leading to the remarkable success of the proof of Fermat’s Last Theorem. But all this work relies on the axiom of universes. “Everyone sees that this is a quick and dirty fix,” says Colin McLarty of Case Western Reserve University in Cleveland. “But it works.”

Intuitively, many mathematicians thought Grothendieck didn’t need his fancy universes. Ordinary set theory seemed like it should suffice — or even less. In particular, set theory involves axioms about infinity that seem unnecessary for something like Fermat’s Last Theorem, which involves only finite whole numbers. But no one had proved it until now. McLarty recently showed that Fermat’s Last Theorem can be proven using the ordinary axioms of mathematics, and even a bit less. He presented his results at the Joint Mathematics Meetings in San Diego in January.

“This justifies a feeling that lots of people had and I had too,” McLarty says. McLarty showed that a subset of set theory called finite-order arithmetic, which assumes less about the concept of infinity, is sufficient to undergird Grothendieck’s work.

“This is a well-done, major, clarifying first step,” says Harvey Friedman of Ohio State University. Friedman believes the work could be extended to show that Fermat’s Last Theorem requires only axioms relevant to arithmetic, with no use of infinity at all.

The real thing is here:

Posted by: John Baez on April 9, 2016 5:38 AM | Permalink | Reply to this

Re: Foundations of Mathematics

It sounds to me like by “foundations of mathematics” you may mean something different than many people do. What I mean, and what in my experience many mathematicians mean, is nothing more than a formal system that suffices to encode most of mathematical practice.

Of course, there is also interesting philosophy to be done surrounding such foundations. In the case of HoTT/UF, I personally feel that there is a perfectly good description of the undefined concepts (\infty-groupoids), the “rules by which we manipulate them” (in a type-theoretic foundation, I think your “listing of fundamental facts” and “description of how inferences are to proceed” have to be combined into something like this), and a recasting of some fundamental developments in accord with these. A number of homotopy type theorists have tried to explain all this in expository papers.

Maybe you feel that these explanations lack “philosophical coherence”, or just that they weren’t written comprehensibly. I don’t know quite what philosophical coherence means, but it would be great if someone (not me; I’ve filled my quota of expository writing about HoTT for a while) could write such an exposition in terms that would satisfy you.

However, it seems to me that there is an important level of “practical/mathematical foundations for mathematics” that is purely mathematical, and can be recognized for what it is without needing any philosophical support. Maybe you would prefer that the word “foundations” not appear in the name of such a thing. That ship may have sailed; but I would be curious to know what name you would prefer to use for this level?

For what it’s worth, I do absolutely acknowledge that “standard” ZFC-based foundations of mathematics have achieved incredible things. However, I think that of those achievemnets that are (a) purely mathematical (rather than philosophical) and (b) of relevance to most mathematical practice (rather than just the study of ZFC and its variants), most of them are not really very specific to ZFC, but can fairly easily be imported into most reasonable alternative foundations. Thus, much less work may be required to establish a new foundation than was required to establish ZFC; not because the bar is lower, but because we have ZFC’s shoulders to stand on. (This does not, of course, mean that ZFC is logically or conceptually more fundamental than any other foundation; just that it came first historically, and so a lot of the basic work was done in its language first.)

Posted by: Mike Shulman on April 9, 2016 4:54 AM | Permalink | Reply to this

Re: Foundations of Mathematics

“However, it seems to me that there is an important level of “practical/mathematical foundations for mathematics” that is purely mathematical, and can be recognized for what it is without needing any philosophical support. Maybe you would prefer that the word “foundations” not appear in the name of such a thing. That ship may have sailed; but I would be curious to know what name you would prefer to use for this level?”

Framework.

algebraic topology framework categorical framework algebraic geometry framework …

Posted by: harvey Friedman on April 10, 2016 6:07 AM | Permalink | Reply to this

Re: Foundations of Mathematics

There is no point in arguing which of two or more logically equivalent foundations are better. Two logically equivalent frameworks, on the other hand, is another story. I can see how people can feel strongly about their preferred ways of framing their favorite area of mathematics.

Posted by: Eugene Lerman on April 10, 2016 2:48 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I’m not talking here about any specific subject, but about ‘mathematical’ foundations for all of mathematics. Would you still say ‘mathematics framework’? Is this terminology in the literature?

Posted by: Mike Shulman on April 11, 2016 7:18 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Probably the literature is not careful about distinguishing between different kinds of setups for mathematics. I have seen “framework” used episodically, and probably not with any careful meaning.

Category theory is a good example of a framework that is not a foundation. E.g., MacLane in his book Categories for the Working Mathematician defined a category as a SET of objects together with … .

Category theory is obviously a VERY useful and important framework.

Posted by: Harvey Friedman on April 12, 2016 1:53 PM | Permalink | Reply to this

Re: Foundations of Mathematics

If category theory is an example of what you mean by a “framework”, then your “frameworks” are not what I mean by a “mathematical foundation for mathematics”. As I said, what I mean is

a formal system that suffices to encode most of mathematical practice.

Category theory is not such a thing, because among other things it is not a formal system. ZFC is, as are ETCS, and MLTT, and HoTT, and so on.

Posted by: Mike Shulman on April 12, 2016 5:51 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Category Theory, as made into a formalization by Lawvere and others some time ago. I think ETCS is what I am referring to here. E.g., I saw http://math.stackexchange.com/questions/432172/developing-category-theory-inside-etcs

Posted by: Harvey Friedman on April 12, 2016 6:49 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Okay, ETCS is a mathematical foundation in my sense. But it’s wrong to refer to ETCS as “category theory”. Category theory is a mathematical subject that, as you point out, is usually defined using concepts from set theory. ETCS is, like ZFC, a particular first-order theory involving undefined terms — in the case of ZFC the undefined terms are “set” and “membership”, while for ETCS they include “set” and “function”. We usually informally express the axioms of ETCS by saying that “sets and functions form a category with such-and-such properties”, but that is just a use of the ideas of category theory as an organizing principle (“framework”?); the axioms as stated stand on their own.

Posted by: Mike Shulman on April 12, 2016 8:28 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I have no strong opinion on how the words “foundation” or “framework” ought to be used.

But I think Mike’s point about ETCS is an important one. ETCS is a set theory in just the same sense that ZFC is. It can be stated with zero categorical terminology, and in particular, does not depend on the concept of category. I made a big deal of this point here:

Tom Leinster, Rethinking set theory. American Mathematical Monthly 121 (2014), no. 5, 403–415.

This is addressed explicitly under “Three misconceptions” (bottom of p.404/top of p.405), but really the whole paper is intended to make clear the elementary nature of ETCS.

Posted by: Tom Leinster on April 13, 2016 12:38 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Hey, that’s a really nice paper, Tom! For some reason I’d never seen it. I should have given it to my category theory students last quarter.

Posted by: John Baez on April 13, 2016 4:39 PM | Permalink | Reply to this

Re: Foundations of Mathematics

I don’t intend to participate in the “framework vs foundations” discussion, but I want to point out that ETCS is a formalization of set theory not of category theory. It is merely phrased in the language of category theory.

Posted by: Karol Szumiło on April 13, 2016 3:00 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Oh, I guess Tom already mentioned that…

Posted by: Karol Szumiło on April 13, 2016 3:01 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Thank you for that extensive and very interesting discussion!

Personally, though, my question was about your point (2) (the objective reality of (V,)(V,\in)), which you specifically declined to talk about. Can you say anything about how this belief is justified?

Posted by: Mike Shulman on April 7, 2016 3:01 AM | Permalink | Reply to this

Re: Foundations of Mathematics

The objective reality people on (V,epsilon) are currently on the defensive, at least somewhat. The most unequivocal of the diehards are Robert Solovay, Hugh Woodin, and Peter Koellner. Donald Martin also has a more nuanced unequivocal view.

I don’t find such positions convincing. In fact, I am rather agnostic on such issues, finding no position convincing. The late Hilary Putnam had similar sentiments in that he published a famous piece called “Philosophy of Mathematics: Why Nothing Words”.

I am a philosophical and foundational whore. I am interested in obtaining substantial results that are suggested by the relevant foundational debates. They are designed to attack or defend any even unreasonable point of view that lends itself to such results.

In a way, this is very Goedelian. His famous Incompleteness Theorems have been used to attack or defend a huge variety of views in the philosophy and foundations of mathematics.

So I would recommend that you ask Solovay, Woodin, Koellner, Martin (in no order). However, I should warn you that you probably won’t be satisfied, but that is just my personal biased opinion.

Posted by: Harvey Friedman on April 7, 2016 4:30 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Ok, thanks. Something you said on the G+ discussion had given me the impression that you believed in the objective reality of (V,)(V,\in), but now I can’t find what it was, and evidently I was mistaken in that conclusion.

Posted by: Mike Shulman on April 7, 2016 8:03 PM | Permalink | Reply to this

Re: Foundations of Mathematics

One thing I find myself wondering is whether “standard-ness” follows the same kind of progression as (say) the performance of algorithms for matrix multiplication.

To wit, there exists no (asymptotically) “optimal” algorithm for matrix multiplication; merely an infinite series of algorithms each faster by a yet more infinitesimal margin than the last (…and with correspondingly nastier constant factors).

My question, then, is this: How convinced should one be that set theory doesn’t follow the same line, by which the addition of yet more (still consistent) axioms permits proving more theorems, with each axiom expanding the power of the theory by a yet more infinitesimal margin?

Posted by: Alex Elsayed on March 13, 2017 12:03 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Isn’t that essentially what the incompleteness theorem says must be the case? Any consistent recursive axiom system is incomplete, i.e. it can always be augmented by further consistent axioms that hence permit proving more theorems.

Posted by: Mike Shulman on March 13, 2017 4:39 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Indeed, we know that it’s always possible to strengthen set theory by adding extra axioms, at least if it’s consistent (which we don’t know).

Gödel showed not only do extra axioms let us prove new theorems: extra axioms can also be found that allow us to dramatically shorten the proofs of existing theorems.

It’s called Gödel’s speed-up theorem and the idea of the proof is simple. Consider this statement:

This statement cannot be proved in ZFC in fewer than a googolplex symbols.

If ZFC is consistent, that statement cannot be proved in ZFC in fewer than a googolplex symbols. But it’s a theorem of ZFC, so it can safely be added as an axiom without destroying consistency, and it shortens the proof of itself by almost a googolplex symbols.

Posted by: John Baez on March 13, 2017 5:47 PM | Permalink | Reply to this

Re: Foundations of Mathematics

John Baez

I will make substantial posts here in reply to what I see and offer some independent ones on foundations of mathematics at a nontechnical level if invited, where there would be a serious chance of a productive interchange.

Posted by: Harvey Friedman on April 3, 2016 12:23 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Great! This comment contains a challenge you might enjoy addressing, and there’s a more light-hearted challenge here.

Posted by: John Baez on April 3, 2016 4:55 AM | Permalink | Reply to this

Re: Foundations of Mathematics

John -

I have some comments about nonstandard models of arithmetic and other theories. It ideally should go on your Azimuth, but that has gotten so involved structurally, that I just don’t know a good place to put it. Perhaps you can copy this and stick it in there somewhere.

The “standard” view of nonstandard models has not been very well represented on the Azimuth thread. Here is the hard line version.

  1. As far as PA (first order Peano arithmetic) is concerned. The “standard” view is that there is absolutely no such thing as a nonstandard integer. The phrase arose for purely technical reasons connected with PA Incompleteness and technical tools and technical questions and technical dreams that have been unrealized.

  2. A nonstandard integer is not anything at all, but a point in a model of PA infinitely many predecessors in that model. Thus nonstandard integers live only in so called nonstandard models of PA. These are the models of PA that are not of order type omega. There is only one model of PA of order type omega up to isomorphism.

  3. To date, there has not been any reasonable preferred nonstandard model of PA ever presented - but I am not quite sure about something decades ago, which I will mention below. Hopefully somebody reading this can clarify.

  4. There is a reasonably preferred and interesting category of closely related such. These are the ultra powers of the standard model via any non principal ultrafilter on omega.

  5. However, this construction is not very satisfactory for two reasons. One is that these ultra powers are not isomorphic to each other (I don’t know how much the isomorphism types of these have been studied). Secondly, all of these ultra powers satisfy the same sentences as the standard model of PA.

  6. So this renders these nonstandard models prima facie useless for independence results from PA. In contrast, in set theory, one does have a lot of interesting ways of constructing models which differ greatly in what sentences hold and fail, thereby getting lots of interesting Incompleteness from ZFC.

  7. There have been some people, including Nelson and later Sanders, and others, who are attracted to the idea that the standard/nonstandard distinction should be viewed as fundamental, and can provide an alternative f.o.m. that has some degree of serious radicality.

  8. As I said before, I am a foundational whore, and have played with this also. As usual, whores don’t like to endorse anything.

  9. However, this approach of taking the standard/nonstandard integer idea seriously, has the major problem of losing one of the great impressive features of standard f.o.m., adding greatly to its coherence and robustness. And that is the strong internal categoricity properties of standard f.o.m.

  10. There was a development I think attributed to Kochen and Kripke, maybe late 1970s, which purported to give an at least somewhat preferred model of PA plus the negation of the 1-consistency of PA. Thus it would satisfy a false Pi-0-2 sentence. I think it was by a restricted ultra power construction, where the ultra filter only applies to some sets. I’m not sure how preferred this model was, and I don’t remember the details.

  11. In any case, it doesn’t come close to fulfilling the technical dream of being able to manipulate models of PA to get independence results with anything like the flexibility and power that one has for ZFC.

  12. As a technical tool, I have been using models of ZFC with nonstandard integers for almost 50 years. I have to, in order to get perfectly natural arithmetic independence results from ZFC.

  13. Sanders also emphasizes his use of nonstandardism as a technical tool in addition to being something allegedly foundational.

Posted by: Harvey Friedman on April 7, 2016 4:54 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Prof. Friedman, would you be so kind to tell us what “philosophical coherence” is precisely, regarding that in the thread on Google+ which prompted this post and thread you put such a hi stake on the satisfaction of that criterium and that neither wikipedia nor simple google search seem to give nothing useful. Good standard reference will be appreciated as well.

Posted by: Zoran Skoda on April 26, 2016 3:48 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Ok, I have a question. You requested several times for a “philosophically coherent” explanation for HoTT, and I’m getting a progressively better idea of what you mean by that. Can you give us a specific reference for a similarly “philosophically coherent” exposition of ZFC set theory? I suspect that such an exposition will further clarify what you want. Also, what do you expect to be the reaction to such a piece by a mathematician from the 19th century who has no exposure to the concept of “set” or the fully general idea of “function”?

Posted by: Itai Bar-Natan on April 11, 2016 5:56 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Since Prof. Friedman is actively watching this thread, I might as well ask him this question here: I am a bit confused by your definition of k-similarity in “Impossible Counting”. There are 2 or 3 separate ways I could see it interpreted.

Do you mean that *:D^2 -> D and *’:D’^2 -> D’ are k-similar iff there is f:D -> D’ such that for all E a k-subset of D, and for all e,e’ in E, f(e * e’) = f(e) *’ f(e’)?

How would that be different from * and *’ being isomorphic?

Or do you mean that once you pick E, you can find an k-subset E’ of D’, and an isomorphism from E U (E*E) to E’ U (E’ *’ E’) that respects the multiplication?

Or do you mean something involving the set of conjugacy classes of bop isomorphism that appear once you look at the k-restrictions?

Posted by: Craig on April 7, 2016 7:44 PM | Permalink | Reply to this

Re: Foundations of Mathematics

We have binary operations *:D^2 into D and *’:D’^2 into D’.

We look at restrictions of * to k element subsets of D (actually their Cartesian squares).

We look at restrictions of *’ to k element subsets of D’ (actually their Cartesian squares).

For k-similarity, we require that every such restriction of * is isomorphic to some such restriction of *’, and vice versa.

Isomorphism between two such restrictions is taken to mean an isomorphism between their graphs, as sets of triples.

E.g., the 1-similarity relation between bops has exactly 4 equivalence classes.

Posted by: Harvey Friedman on April 7, 2016 10:38 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Thank you, that helps a lot.

So basically, you can also imagine this as first classifying all binary operations from size-k sets up to isomorphism – the number of which is bounded from above by something like k^{C k^2} – and then asking which subsets can appear as restrictions of larger binary operations. So that latter number – your \theta(k) – is bounded from above by something like 2^{k^{C k^2}}.

The last thing that confuses me is why this number should be different if we restrict to finite binary operations – that is, why \theta’(k) is different from \theta(k).

(And I’d love to see the proof of Thm 3.3, that ZFC cannot compute \theta(12); that just blows my mind.)

Posted by: Craig on April 8, 2016 3:20 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Sorry, those upper bounds should be k^{C k^4} and 2^{k^{c k^4} respectively. And I think C is 1/2 + \epsilon

Posted by: Craig on April 8, 2016 3:30 AM | Permalink | Reply to this

Re: Foundations of Mathematics

I think that Craig thinks that

every binary op is k-similar to a finite binary op.

This is false. Consider (N,f), where binary f is one-one. All of its 4-restrictions are one-one.

Consider (A,g), where A is finite and has at least two elements. It has a 4-restriction that is not one-one.

So f is not 4-similar to any finite bop whose domain has at least 2 elts. And for trivial reasons, f is also not 4-equiavlent to any bop whose domain has fewer than 2 elts.

I’m afraid I have higher priorities right now, but your request is duly noted. I construct a set of 12 sized gadgets such that “there is a bop that omits all isomorphic copies of these” is equivalent to the consistency of ZFC. You can use this main Lemma to show that ZFC can’t possibly make the exact count, assuming ZFC is consistent (I think I may have used ZFC is 1-consistent for this, but I think it also can be reduced to just consistency.)

I am in the business of trying to “blow people’s minds” as you say, where I use phrases like “deeply disturbing”. So it would be useful to know what your areas of expertise are, and maybe something about why this “blows your mind”. So I can do more of this…

Posted by: Harvey Friedman on April 8, 2016 6:22 AM | Permalink | Reply to this

Re: Foundations of Mathematics

Ah! Thank you! That does make things much clearer – I didn’t realize that particular subset of k-size multiplication table equivalence classes a) naturally occurs when you start thinking about infinite size bops, and b) can’t occur in any bop on a finite set.

As to my background – I’m currently a software engineer, but I have some mathematical logic background and read both Cohen’s and Smullyan/Fitting’s books on the continuum hypothesis about 5 years ago (and even understood the vast majority of them :-)

It blows my mind because the set of 12x12 multiplication tables, up to relabelings, is something that you can easily picture in your head, and you could even conceive of working out the sum by hand (at least if you knew the Bell numbers up to B_{144}).

Furthermore, you can conceive of trying to assemble those cosets into consistent subsets again by hand, if you had infinite time. If I were to do so, I’d probably start by making a weighted graph, whose vertices are the cosets and whose edges are labeled by the maximum m such that the two cosets have an isomorphic m-restriction. This would then give me restrictions on what triples of vertices can show up as k-restrictions of any bop.

But now, with your example, I get an idea of why this program would not work – if I were to try and assemble a bop out of that 1-to-1 coset alone, I’d be able to create a multiplication for any finite size, but I’d never be able to close it. And I can (now) imagine that the assembly of a sufficiently complex subset of cosets would translate into a sentence unprovable in ZFC.

Again, thank you.

Posted by: Craig on April 8, 2016 3:35 PM | Permalink | Reply to this

Re: Foundations of Mathematics

Investigating the foundation of mathematics is a rather undefined task. Probably several foundations exist. A foundation must necessarily be very simple and it must extend to a large part of mathematics. This extension must be restricted.

A similar investigation of the foundation of physical reality has a much smaller target. Again here the foundation must be very simple and its extension must be restricted. There will exist a great chance that this foundation is already discovered and as a similar structure added to mathematics. The foundation is not accessible to observation. Thus its existence cannot be verified by experiments. This sins against the physicist’s scientific method. So the mathematicians have an advantage here. They can investigate the foundation without any reluctance and test the extensibility of the foundation. A possible candidate is the orthomodular lattice. It extends into a separable Hilbert space, which is a favorite tool of quantum physicists. However, this road is crippled by the fact that the Hilbert space is in essence no more and no less than a structured storage medium for dynamic geometric data. It cannot explain why physical reality features dynamical coherence. The structure of the Hilbert space cannot prevent that its content represents a dynamic chaos. Thus the targeted foundation must be aided by mechanisms that ensure dynamic coherence. The orthomodular lattice was named “quantum logic” by its discoverers Garret Birkhoff and John von Neumann. However, this is in conflict with the fact that in their introductory paper the duo showed that the set of closed subspaces of the separable Hilbert space had exactly the relational structure of an orthomodular lattice. So, if the elements of the lattice are no logical propositions, what is then the proper interpretation of these elements?

Posted by: Hans van Leunen on July 18, 2016 9:35 PM | Permalink | Reply to this

Post a New Comment