Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: community: general

Topic: Projective Determinacy


view this post on Zulip Todd Trimble (Jul 19 2024 at 23:38):

Today I began watching this lecture by Hugh Woodin, and came across this extraordinary and gnomic slide:

Projective Determinacy is True
Claim
Projective Determinacy is the correct axiom for Second-Order Number Theory just as the classical Peano axioms are the correct axioms for Number Theory

And then below in the same slide:

Thus we now have the axioms for
P(N),+,,.\langle P(\mathbb{N}), +, \cdot, \in\rangle.
It just took us a while to find and validate the axioms.

I don't understand this at all, but "validate the axioms" and "PD is true" sound like such hard-core expressions of Platonistic belief, when these go so far beyond ZFC (it's something connected with the existence of infinitely many Woodin cardinals, whatever those are). Validate the axioms! What could that mean, I wonder?

view this post on Zulip Kevin Carlson (Jul 19 2024 at 23:41):

I don't know anything about projective determinacy in particular, but Woodin is known to have been interested in finding the "correct" axioms for a long time, as opposed to some kind of multiverse-ish viewpoint (which seems more sensible to me.)

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 20 2024 at 02:56):

This doesn't surprise me. It aligns with Woodin's beliefs and the philosophical tradition he follows. When Woodin discusses truth, he sees himself as making predictions about the physical world, including his infamous

In the next 10,000 years there will be no discovery of an inconsistency in [ZFC + "There exist infinitely many Woodin cardinals"]. [1]

He justifies the notion of truth for abstract mathematical axioms by the usefulness and the truth of the physical predictions they make, in line with the following opinion of Gödel:

There might exist axioms so abundant in their verifiable consequences, shedding so much light upon a whole discipline, and furnishing such powerful methods for solving given problems (and even solving them, as far as possible, in a constructivistic way) that quite irrespective of their intrinsic necessity they would have to be assumed at least in the same sense as any established physical theory. [2]

This view falls under realism and logical anti-exceptionalism. Woodin considers certain axioms true, and compares the truth of competing axioms, by the way they clarify the discipline, their use in problem-solving, and the degree to which their physical predictions hold up.

You ask: "Validate the axioms! What could that mean, I wonder?" I think he refers to projective determinacy meeting Gödel's and Woodin's criteria.

NB. I don't find this a convincing argument, and don't expect others would either. I am just trying to summarize Woodin's beliefs. I can't be impartial; to be honest, whenever I read about Woodin and his supposedly-impressive track record of physical predictions, the Nostradamus keyword in Girard's glossary [3] comes to mind:

Abduction has made a lot of progress in recent years; for instance in 1937, a Mr. Ruir was able to predict the Spanish Civil War by an abductive reading of Nostradamus. Now, with computer-aided abduction, it has been possible, in 1998, to read back the death of Princess Diana in the verses of Nostradamus... unfortunately, after the accident took place.

[1] H. Woodin, The Transfinite Universe, in Matthias Baaz (ed.), Kurt Gödel and the foundations of mathematics: horizons of truth. New York: Cambridge University Press (2011)
[2] K. Gödel. What is Cantor's continuum problem? The American Mathematical Monthly, 54(9):515-525, 1947
[3] J-Y. Girard, Locus Solum. From the Rules of Logic to the Logic of Rules. In: Fribourg, L. (eds) Computer Science Logic. CSL. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. (2001)

view this post on Zulip Eric M Downes (Jul 20 2024 at 03:30):

Okay dumb question.

The “empirical/practical” approach to truth seems fine so long as one is prepared to encounter: axioms manifestly useful in one field, may not be in another, in fact may be undesirable.

Specifically. What I find puzzling is his (seeming) assertion that LEM must hold in each universe in the “multiverse” of set universes reachable by forcing, expressed around ~16:30 concluding from his informal definition of multiverse around 15:00.

“ψ either does or does not hold” is a direct quote by Woodin.

Isn’t this explicitly something one cannot assume in an arbitrary topos? The internal language used to express whether ψ is true or false is intuitionistic unless certain conditions are met, which wrt c=?20\frak{c}\overset{?}{=}2^{\aleph_0} are manifestly not satisfied!

What am I missing here?

view this post on Zulip John Baez (Jul 20 2024 at 07:59):

Woodin is not doing topos theory! He's studying extensions of ZFC in the framework of classical first-order logic!

Woodin probably doesn't give a shit about more general topoi.

view this post on Zulip Todd Trimble (Jul 20 2024 at 10:40):

Zoltan, you brought in the phrase "physical predictions" twice and "predictions about the physical world" once. This confuses me. For example, I wouldn't call "In the next 10,000 years there will be no discovery..." a prediction about the physical world per se; I'd just call it a prediction. Are there other "physical predictions" besides those of the sort "a contradiction with ZFC will not be found" (I assume he accepts ZFC as "true")?

Or maybe he and others view mathematics as part of the physical world? In that case I would wonder how I should view Euclidean vs. non-Euclidean geometry, whose axioms are in conflict. Is one of them an "incorrect theory"?

view this post on Zulip Eric M Downes (Jul 20 2024 at 10:49):

John Baez said:

Woodin is not doing topos theory! He's studying extensions of ZFC in the framework of classical first-order logic!

Woodin probably doesn't give a shit about more general topoi.

Right, I get that he emphatically isn't doing topos theory. Maybe I misunderstood what is meant by multiverse. In classical logic there are unprovable statements, and the continuum hypothesis or its falsity is one of them, so the assertion that either a given ψ\psi holds or it doesn't seems incongruous. He could mean "is provable" by "holds" but the examples he lists are those of tautologies or trivially self-contradicting statements in ZFC.

view this post on Zulip John Baez (Jul 20 2024 at 11:38):

As far as I can tell set theorists like Joel Hamkins who advocate taking the multiverse seriously think of it as the class of all models of ZFC, and they study it using classical logic. Hamkins is basically unconcerned with intuitionistic logic, constructivism, topos theory, etc.

I don't associate Woodin with the "multiverse" approach: I think of him as trying to learn more about the "one true universe" - the one "best" model of ZFC in the framework of classical logic.

So, I will have to listen to the video to guess what Woodin means by saying that "LEM must hold in each universe in the “multiverse” of set universes reachable by forcing". This sounds so obviously true from that it's a weird thing to say! For a classical set theorist the law of excluded middle holds in every set universe, not just those reachable by forcing.

view this post on Zulip John Baez (Jul 20 2024 at 11:46):

Okay, I listened and Woodin didn't actually say that.

view this post on Zulip Eric M Downes (Jul 20 2024 at 11:47):

Apologies, the words not in quotes are my (possibly poor) summary of his words, not his. I think my confusion arises because it seems like he is asserting that LEM should apply to provability, not just truthiness, so if a statement like the continuum hypothesis is unprovable but seems useful and like "it should be true", then we must have got the wrong axioms... Equally likely I just don't understand ZFC and formal logic well enough to actually get what he is doing.

view this post on Zulip John Baez (Jul 20 2024 at 11:48):

What he said around 15:00-16:30 of his talk was extremely interesting and nontrivial: I believe what he was trying to say is something roughly like this:

For each sentence ϕ\phi of ZFC and for each model VV of ZFC there is an algorithm for constructing a sentence ϕ\phi^* of ZFC such that ϕ\phi^* is satisfied in VV iff ϕ\phi is satisfied in all models VV' obtained by forcing from VV.

view this post on Zulip John Baez (Jul 20 2024 at 11:49):

He didn't say "algorithm", but as a foil he presented a silly way of defining ϕ\phi^* that can't be constructed using any algorithm, and he basically "I don't mean something like that".

view this post on Zulip Eric M Downes (Jul 20 2024 at 11:51):

Is this method of constructing ϕ\phi^*, whether we call it an algorithm or not, constructive? I think so? If so, I would expect results pertaining to constructivist logic to apply. Hence my confusion.

view this post on Zulip John Baez (Jul 20 2024 at 11:52):

He also didn't say "all models obtained by forcing from VV"; he said "universe in the generic-multiverse generated by VV". I don't exactly know what the means, but (for example) it might also include models from which VV can be obtained by forcing. He drew a little graph where vertices are models and edges are forcing constructions, so he may have been talking about a connected component of that graph.

view this post on Zulip John Baez (Jul 20 2024 at 11:56):

Eric M Downes said:

Is this method of constructing ϕ\phi^*, whether we call it an algorithm or not, constructive? I think so? If so, I would expect results pertaining to constructivist logic to apply. Hence my confusion.

I think bringing constructivism into this conversation is only confusing until we understand what Woodin was trying to say. It's like trying to translate a poem into French before you even have a clue about what it means in English.

What I meant by "algorithm" is this: I'm guessing there's some systematic method of getting ϕ\phi^* from ϕ\phi, just by looking at the symbols in ϕ\phi and doing some syntactical stuff - but the method might be rather technical, and Woodin thought it would be too big of a digression to explain it in detail.

view this post on Zulip Eric M Downes (Jul 20 2024 at 11:57):

Thanks, I appreciate your time. Great point re just sticking with the source.

view this post on Zulip John Baez (Jul 20 2024 at 11:58):

Maybe this is your confusion:

He could mean "is provable" by "holds"

No, "holds" is relative to a model, and "holds in V" means "is satisfied in the model V", and he was talking about that concept.

view this post on Zulip John Baez (Jul 20 2024 at 11:59):

He was stating that if you hand him a sentence ϕ\phi, he can cook up a sentence ϕ\phi^* such that ϕ\phi^* holds in VV iff ϕ\phi holds in every model in the "generic-multiverse generated by VV", whatever that is.

view this post on Zulip John Baez (Jul 20 2024 at 12:00):

So the point is, we can tell which sentences are satisfied in all models (aka universes) in the generic-multiverse generated by VV, just working within VV.

view this post on Zulip John Baez (Jul 20 2024 at 12:02):

This is some theorem that he says Cohen could easily have proved right after he invented forcing.

view this post on Zulip Eric M Downes (Jul 20 2024 at 12:02):

And the "generic-multiverse generated by VV" does include the connected component containing VV where edges are forcing operations, as far as you can tell?

view this post on Zulip Eric M Downes (Jul 20 2024 at 12:05):

Seems like he has written a book on this. I'll try to find it and see if the definition can be parsed.

view this post on Zulip John Baez (Jul 20 2024 at 12:11):

Eric M Downes said:

And the "generic-multiverse generated by VV" does include the connected component containing VV where edges are forcing operations, as far as you can tell?

He was being pretty vague, but I think he was trying to say that the "generic-multiverse generated by VV" includes the connected component containing VV where edges are forcing operations - and he may even have been saying they're the same thing!

view this post on Zulip John Baez (Jul 20 2024 at 12:12):

If I was just listening to this uncritically, being my usual self, I would have assumed they're the same thing.

view this post on Zulip Eric M Downes (Jul 20 2024 at 12:13):

Ok found the article from that book; if anyone wants it lemme know.

Woodin

The generic-multiverse of sets. Let the multiverse (of sets) refer to the collection of possible universes of sets. The truths of the Set Theory are the sentences which hold in each universe of the multiverse. The multiverse is the generic-multiverse if it is generated from each universe of the collection by closing under generic extensions (enlargements) and under generic refinements (inner models of a universe which the given universe is a generic extension of).

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 20 2024 at 12:22):

@Todd Trimble: Yes, Woodin most definitely views consistency statements as facts about the physical world. The very next sentence in [3], after the part I quoted earlier, continues as follows:

In the next 10,000 years there will be no discovery of an inconsistency in [ZFC + "There exist infinitely many Woodin cardinals"]. This is a specific and unambiguous prediction about the physical universe. Further it is a prediction which does not arise by a reduction to a previously held truth (as for example is the case for the prediction that no counterexample to Fermat’s Last Theorem will be discovered).

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 20 2024 at 12:27):

This doesn't mean that Woodin views all mathematical utterances themselves as facts about the physical universe - but certainly as things whose truth would have consequences about the physical universe.

view this post on Zulip John Baez (Jul 20 2024 at 12:33):

Woodin's attitude here about the physical universe reminds me of that great short story by Greg Egan called Luminous. I'll quote a bit:

It all started out as a joke. Argument for argument's sake. Alison and her infuriating heresies.

"A mathematical theorem," she'd proclaimed, "only becomes true when a physical system tests it out: when the system's behaviour depends in some way on the theorem being true or false.

It was June 1994. We were sitting in a small paved courtyard, having just emerged from the final lecture in a one-semester course on the philosophy of mathematics - a bit of light relief from the hard grind of the real stuff. We had fifteen minutes to to kill before meeting some friends for lunch. It was a social conversation - verging on mild flirtation - nothing more. Maybe there were demented academics, lurking in dark crypts somewhere, who held views on the nature of mathematical truth which they were willing to die for. But were were twenty years old, and we knew it was all angels on the head of a pin.

I said, "Physical systems don't create mathematics. Nothing creates mathematics - it's timeless. All of number theory would still be exactly the same, even if the universe contained nothing but a single electron."

Alison snorted. "Yes, because even one electron, plus a space-time to put it in, needs all of quantum mechanics and all of general relativity - and all the mathematical infrastructure they entail. One particle floating in a quantum vacuum needs half the major results of group theory, functional analysis, differential geometry - "

"OK, OK! I get the point. But if that's the case... the events in the first picosecond after the Big Bang would have 'constructed' every last mathematical truth required by any physical system, all the way to the Big Cruch. Once you've got the mathematics which underpins the Theory of Everything... that's it, that's all you ever need. End of story."

"But it's not. To apply the Theory of Everything to a particular system, you still need all the mathematics for dealing with that system - which could include results far beyond the mathematics the TOE itself requires. I mean, fifteen billion years after the Big Bang, someone can still come along and prove, say... Fermat's Last Theorem." Andrew Wiles at Princeton had recently announced a proof of the famous conjecture, although his work was still being scrutinised by his colleagues, and the final verdict wasn't yet in. "Physics never needed that before."

I protested, "What do you mean, 'before'? Fermat's Last Theorem never has - and never will - have anything to do with any branch of physics."

Alison smiled sneakily. "No branch, no. But only because the class of physical systems whose behaviour depend on it is so ludicrously specific: the brains of mathematicians who are trying to validate the Wiles proof."

"Think about it. Once you start trying to prove a theorem, then even if the mathematics is so 'pure' that it has no relevance to any other object in the universe... you've just made it relevant to yourself. You have to choose some physical process to test the theorem - whether you use a computer, or a pen and paper... or just close your eyes and shuffle neurotransmitters. There's no such thing as a proof which doesn't rely on physical events, and whether they're inside or outside your skull doesn't make them any less real."

view this post on Zulip Todd Trimble (Jul 20 2024 at 12:42):

So okay. Any guess as to how Woodin would respond to my question about Euclidean vs. non-Euclidean geometry? They can't both be "physically true"; their axioms collide.

(I suddenly have an urge to give Woodin a copy of Mathematics: Form and Function, by Saunders Mac Lane.)

view this post on Zulip John Baez (Jul 20 2024 at 12:48):

I think Woodin is someone on the track of his own personal vision - some very interesting intuition about set theory which I don't really understand - and trying to teach him more philosophy of mathematics, or even take his philosophy of mathematics seriously, would be missing the point. His work reminds me of outsider art: it's sort of wacky but it's sort of cool, and I wouldn't want to talk people out of doing it.

view this post on Zulip John Baez (Jul 20 2024 at 12:52):

So please don't make him read that book, @Todd Trimble. :upside_down:

(I have decided I'm going to continue using that emoticon. For your benefit I will define it. It means: "please don't take the preceding utterance seriously to the point of letting it annoy you.")

view this post on Zulip Todd Trimble (Jul 20 2024 at 12:52):

is somehow missing the point

This was a question out of curiosity. The gnomic utterances are fascinating but quite alien to my way of thinking.

view this post on Zulip John Baez (Jul 20 2024 at 12:55):

Yes, they're alien to me too, hence the "outsider art" idea. I think he's been immersed in ZFC for so long, with such depth, that's he's evolved some intuitions about it that are beyond my comprehension. It's mildly annoying that he thinks these intuitions point toward the "true" model of ZFC, but on the other hand that delusion may be a great way to come up with interesting new axioms.

view this post on Zulip Todd Trimble (Jul 20 2024 at 13:01):

Yes. I'm still wondering how he might react to the Euclidean geometry question, if he thinks mathematical truths are physical truths. It just sounds like a basic category error to me.

Ultimately, if I ever wanted to understand projective determinacy, I would be determined to ignore the talk about "truth". It's also fun to treat the whole thing as a game. (The axiom of determinacy is all about games!)

view this post on Zulip John Baez (Jul 20 2024 at 13:09):

I bet he would answer your question in some unsatisfying way, like saying obviously there are different kinds of geometry and only experiment can tell which one our world obeys.

view this post on Zulip Todd Trimble (Jul 20 2024 at 13:30):

That would of course miss the point of the question, because I'm trying to get at "if he thinks mathematical truths are physical truths". If one form of geometry is not "physically true", then apparently it's not mathematically true, which to me is kind of nonsensical, an error in reasoning. Of course one basic problem is the word "true".

For me, axioms are provisional starting points. Maybe he also feels that way sometimes about some theories, but for the sacred important foundational theories like set theories, there it's a matter of Truth with a capital T?!

view this post on Zulip John Baez (Jul 20 2024 at 13:43):

I'm quite sure that any conversation you had with Woodin about these issues would leave you tearing your hair out in frustration. As for me, I follow Elvis Costello on this:

I used to be disgusted
Now I'm just amused

I believe Woodin thinks you can get to understand mathematical structures and figure out what axioms they obey by a slow process of discovery. For example, at 12:59 his slides say

Claim: Projective determinacy is the correct axiom for second order number theory just as the classical Peano axioms are the correct axioms for number theory.

This claim is sloppy in a number of ways, even given his philosophy where axioms can be "correct". What does he mean by "the" correct axiom - aren't there others? By "classical Peano axioms" does he mean the first-order axiom system PA? Peano's original axioms were second-order.

Anyway, he seems to believe the process of discovering "correct" axioms is a search for consilience (though he doesn't use that word): when you've got enough good theorems it's evidence that your axioms are correct. But I don't think he's enough of a philosopher to state his philosophy in a clear way.

view this post on Zulip Todd Trimble (Jul 20 2024 at 14:02):

Nah, you've got me all wrong. I would also be amused. But I am curious about how he'd react, hence my questions.

Thanks for teaching me a new word! I had to click on the link to learn more.

By "classical Peano axioms" does he mean the first-order axiom system PA? Peano's original axioms were second-order.

I also wondered about that.

Anyway, it is interesting speculating on what makes him tick, and you seem to have some good ideas on that.

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 20 2024 at 14:09):

@Todd Trimble:

You ask: any guess as to how Woodin would respond to my question about Euclidean vs. non-Euclidean geometry?

Like John, I can't predict it, apart from suspecting that I'd find it unsatisfying.

However, I personally do find it imaginable that number theory, or, say, logic, might be physical in a sense that geometry is not.

For example, when geometers teach their subject, they acknowledge early on the fact that a square drawn in the sandbox is not technically the square. On one hand the drawing has some extraneous physical properties that ideal abstract squares of geometry don't have, like color. On the other hand (and more importantly) it fails to have some key properties that an ideal mathematical square would have, such as 4 sides of exactly equal length.

Whereas, say, a sequent proof tree printed in a book sure has some extraneous properties, but I don't see any property it lacks that I'd expect the abstract, ideal proof object to have. One could argue that in some sense, the printed tree is a proof, or that it at least contains a proof. This point-of-view gets messy (what about a circular proof printed on the surface of a cylinder), but having thought a lot about the philosophy of logic, it's still not clear to me that there's no way to make it work. So perhaps, if Woodin wanted to, he could justify the claim that predictions about consistency have a certain physical import that predictions about geometry simply don't have.

view this post on Zulip Ryan Wisnesky (Jul 21 2024 at 06:09):

this is probably naive, but could he be saying, that since there is a single model of second order arithmetic (under full, not Henkin, semantics), if you want to approximate its theory in first order ZFC, which will have many models, you are better off adding projective determinacy as an axiom than say V=L or other axioms? and that the meaning of his claim about 'projective determinacy being correct for 2nd order number theory' is the claim that that axiom is the 'best' one can add to zfc for this purpose, in some sense?

view this post on Zulip John Baez (Jul 21 2024 at 06:59):

This is a good introduction to many things Woodin was talking about, but not alas projective determinacy: