I hope it's ok that I mentioned this chatroom in connection with a question asked in MathOverflow chatroom, for the full context see here: chat.stackexchange.com/transcript/9369/2018/11/26

Hello @user21820 can you come to basic mathematics room?

Wanted to know a probability question which is best suited for that room

@CarlMummert: What's the strength of ATR+ defined as ATR where the induction schema is replaced by a transfinite induction schema, namely that for every 1-parameter sentence Q we have the axiom "∀W⊆N ( W encodes a well-ordering of N ∧ ∀k∈N ( ∀m∈N ( W(m,k) ⇒ Q(m) ) ⇒ Q(k) ) ⇒ ∀k∈N ( Q(k) ) )"?

@AndrésE.Caicedo: Hello! =)

@user21820: that system is called Pi^1_\infty-TIo by Simpson, he has some info in his book. Every countable coded beta model satisfies ATRo and the full transfinite induction So Pi^1_1-CAo can prove the consistency of the transfinite induction scheme.

@CarlMummert Oh I see thanks for the reference! So what's the proof-theoretic ordinal of Π[1,∞]-TI0?

I'm curious because I read that ATR has p.t.o. Γ[ε0], but it occurred to me that the same justification for ATR over ACA (you can construct a set by transfinite recursion along any proven well-ordering) applies to ATR+ too, just on the meta-level.

I don't know that ordinal - the bound from Pi^1_1 comprehension makes me think it might be known, but I am not an expert in that kind of proof theory.

@CarlMummert I see. Do you know whom I can ask?

Steve Simpson may well know, otherwise you would need to ask a proof theorist.

Oh I was hoping there was someone on Math SE or Math Overflow that I can ask.

I think Henry Towsner is sometimes active on Math Overflow, but an email would probably be more efficient.

@CarlMummert Oh ok thank you!

Got to run - have a good morning / day

Re: user21820's question: when I say that ZFC is sound - which is rarely - I'm operating in a context where there is a (posited) "distinguished" $\{\in\}$-structure M, and "sound" means "doesn't prove any statement false in M." There's nothing special about ZFC here: when I say a theory T in a language L is sound, I'm working in a context with a distinguished L-structure M, and "sound" means "doesn't prove anything false in M."

When I say something like "arithmetically sound," I'm restricting attention to the class of sentences considered and shifting attention to a different distinguished structure: "ZFC is arithmetically sound" means that ZFC doesn't prove any false arithmetic sentences - that is, ZFC doesn't prove any sentences in the language of arithmetic which are false in the "actual" natural numbers.

Again, this does involve positing a distinguished structure of the appropriate type; however, by restricting the class of sentences I care about, I don't need a whole $\{\in\}$-structure, but rather just a structure for the more limited context.

I believe that Andres' usage of "sound" coincides with my usage of "arithmetically sound."

@NoahSchweber Yup, I get that, but which particular distinguished structure do you mean, when you say ZFC is sound? Minimal transitive model? Or something else?

I mean "the" universe - the (posited) actual universe V of sets. In particular, generally the minimal transitive model of ZFC would not be appropriate since it satisfies "there is no transitive (set) model of ZFC." Of course, all of this requires a belief in V in the first place, and - while it's often convenient to adopt that mindset - this isn't something I ever do with a straight face.

This is all extremely circular, and relies at some point on "nontrivial mathematical faith" which is already problematic at the level of the natural numbers, so I don't tend to talk this way - but it is sometimes useful to adopt this viewpoint, or at least pretend to adopt it.

@NoahSchweber Haha that's exactly the problem I have with "ZFC is sound"; I cannot understand what it is supposed to mean, because there is no actual description of V.

@user21820 Yeah, I'm not a Platonist - my response to all your objections is "yup." But the term still is a good one to have, because if we're working within a strong enough theory it actually does make sense: e.g. MK is strong enough to talk about truth within its "set part," and this serves as a good notion of V. So e.g. if M is a model of MK in which CH holds, then M thinks that ZFC+$\neg$CH is unsound.

This is perfectly meaningful since it's all "internal to a theory," and the "Platonic shorthand" is a useful framework for thinking about it.

@NoahSchweber Aha, so one must work within a meta-system that already has (internally) a distinguished entity serving as the intended model of ZFC.

There's also a more perverse argument for allowing it. One of the most fascinating things about mathematics in my opinion is how what I consider to be unwarranted Platonistic assumptions don't generally cause mathematical problems - indeed, they often serve as useful inspiration. And similarly for all the other philosophies: math survives all ontological perspectives, and even benefits from them.

So I actively want terminology "native to" each of these perspectives, even to the extent that I find them unwarranted.

@user21820 "Aha, so one must work within a meta-system that already has (internally) a distinguished entity serving as the intended model of ZFC." Yes, exactly - or make a genuine Platonist commitment.

@NoahSchweber I can't buy that last disjunction, since I don't see any non-circular way of describing a Platonistic V. =)

Although actually this is selling a third approach short: the idea that, without positing a mathematical reality, there are still principles which are meaningfully preferable to their negations. If I have my terms right, this is called "mathematical realism." I think there's a lot of interesting philosophical content here, and this enables a weak notion of soundness which isn't model-specific, but I do think this is a "secondary" aspect.

(@user21820 Incidentally, my comment above also extends to "perverse Platonism" - I occasionally find it useful to posit that (a) a "true" universe V exists and (b) it's a pointwise-definable model (arxiv.org/abs/1105.4597)! Despite this being kinda bonkers.)

@NoahSchweber Interesting. How does that apply to AC? AC is something that I am doubtful makes sense if the intended universe is very unwieldy, but something that I have no problems with if the intended universe is countable.

But AC is a blanket universal statement that seems not clearly preferable to its negation.

@NoahSchweber Lol... any example where it is useful to assume pointwise-definability?

@user21820 I think Penelope Maddy has some writings on this ("Believing the axioms," maybe?). I tend to agree with you, though, on this, at least to the weak extent of "seems not clearly preferable to its negation"

@user21820 "any example where it is useful to assume pointwise-definability" My notion of "useful" may be disappointingly weak :P. But one thing I really like is the idea that the set/class barrier is significant (by contrast, lots of large cardinal principles can be interpreted as basically suggesting that it's not - that "class-like" behavior occurs at the level of sets already). (cont'd)

Specifically, ZFC of course proves that any model of ZFC containing (say) all the reals has undefinable elements. So saying "reality is pointwise-definable" amounts to positing a kind of emergent phenomenon about the universe: the only way it's possible is to "cross the set/class threshold," since we have truth predicates for set-sized structures. So there's real philosophical content there, in my opinion, and I can even argue in favor of it (but that's for another time)! (cont'd)

But here's a specific mathematical application: "It is consistent with ZFC that there is a length-$\omega_1$-chain in the degrees of countable ordinals under uniform hyperarithmetic reducibility" (never mind what that means for now). This isn't a deeply (or at all :P) interesting result, but it is purely mathematical and the only proof I know uses pointwise definability. (cont'd)

Now, you can object that what it's really using is that many levels of L are pointwise definable, not the idea that reality might be pointwise definable, but thinking about pointwise definable reality was what led me to the proof.

Hi. I think it is best to think of all of this within context, so that soundness is with respect to the set-theoretic (or number-theoretic) universe granted by your metatheory, or if you wish, you work within a model, and soundness is with respect to it, so that what the model thinks is sound may very well not be.

@AndrésE.Caicedo Yea, but my question was more philosophical in that we have a rather concrete intended model of PA, so arithmetical soundness is kind of fixed by our reality, whereas soundness of an ∈-structure doesn't seem to have any canonical meaning. We can't even define soundness in terms of truth in V, so as Noah said we need to internally have some distinguished ∈-structure. We can do that in MK, but then we still cannot describe what "MK is sound" means.

@NoahSchweber Interesting. Pointwise definability indeed sounds like an L-like assumption.

But there are those that even object that there is a concrete intended model of PA, although I assume (hope?) all three of us agree this much. :-)

@AndrésE.Caicedo "although I assume (hope?) all three of us agree this much. :-)" You underestimate the contradictory perspectives of which I am full. :P But, mostly yes.

Once I was talking with Mike Oliver about ... hmm... omega_1-trees, I believe, and there was a question about the existence of some such trees with some properties. Anyway, I said that there was no problem here, because one could always force them, and Mike objected that this didn't mean they existed in the true universe of sets, over which of course there are no genuine generic extensions. It was amusing to see that there was someone with a stricter platonism than mine was at that point.

@AndrésE.Caicedo Heheh... sometimes I'm a slight finitist (I believe PA is 100% consistent but not necessarily have a real-world classical model).

I have to bow out now - have a good day, both of you!

@NoahSchweber Okay thank you and see you next time! =)

@AndrésE.Caicedo Interesting. I have talked to some set theorists and recursion theorists who also believe all the currently not-known-to-be-inconsistent large cardinal axioms to be literally true.

I didn't want to poke and ask what exactly "true" meant, though.

I think I've softened with age, though. When I talk of what is true in V (which is much more than what the axioms buy us) what I mean is what is true, according to our current conventions, which is not quite just mathematical but also says something about the current mathematical culture of active set theorists.

I see.

With respect to large cardinals, I have a position which I thought was unique but then talking with others it turns out they shared it with me (in fact, they assumed that of course that was the position to have). For instance, "obviously" there is a proper class of, say, huge cardinals in V. But I do not quite buy that there are strong cardinals. Naturally, there are strong cardinals in inner models, and there are many stages that satisfy that there is a proper class of supercompacts.

It is also possible to simply take $V$ to be some model of set theory which satisfies enough axioms, without worrying about whether there might be some other choice. Then, by reasoning about this $V$ we can show that various things are provable in our metatheory, essentially by using the completeness theorem WRT our metatheory.

In other words, if we call our metatheory Tmeta, instead of showing Tmeta \vdash \phi we assume we have a model V of Tmeta and show that V \models \phi.

But I have some discomfort "believing" in large cardinal properties that are not Sigma_2. In any case, don't take this too literally; I haven't thought seriously about it for a while. If I did, probably I would have to reexamine my position.

@CarlMummert Yes, I think that is the sort of thing I was suggesting when saying that notions such as soundness should be taken in context.

@Andrés: forcing over the universe is a nice example how different forms of platonism can disagree

I agree with that viewpoint of soundness - it is relative to a choice of V

@CarlMummert That's why I like some results better than others. For instance, it is better to prove that any model of MA with such and such property satisfies blah (as long as MA+such and such is consistent, of course), than to prove that it is consistent to have a model of MA + blah. The latter is a forcing result, the first is just a fact. :-)

@AndrésE.Caicedo That's very interesting. I've been quite often saying that I don't buy (the naive justification for) the unbounded replacement schema of ZFC. Bounded seems fine (non-circular), and I've read that there are ways to justify Π1-replacement and hence Σ2-replacement. I don't understand though why you would believe existence of some kind of cardinal in inner models but not in V.

@CarlMummert Or, to prove that a forcing axiom is consistent with blah, I think it is better to show that we can force over any model of the forcing axiom to preserve it and add blah, than to start from large cardinals and force the forcing axiom + blah.

@user21820 The inner models don't need to be correct.

@user21820 For instance, even if there are no inaccessibles, there may be inner models with all sorts of large cardinals, and L may have transitive models of supercompactness and more.

@user21820 (I think the point is that it is more significant what mice we have than what explicit large cardinals; it is the former that actually capture the large cardinal strength of the universe.)

@AndrésE.Caicedo Yes of course the inner model may be completely different from the universe, but I guess I just don't see why one shouldn't think that if an inner model has a large cardinal, then the universe has no good reason to fail to have the same kind of large cardinal?

@user21820 I think (thought?) the universe is "too wide" to satisfy the sort of reflection principles that a strong cardinal buys you (via, say, appropriate versions of Laver functions). Inner models, on the other hand, are thin.

@AndrésE.Caicedo Hmm I see so you don't think V is or should be "as wide as it can be". More like L?

Anyway I've to go now. I'll read whatever you say later, thanks! =)

@user21820 No no, the opposite. V is too wide and therefore it cannot possible be that a stage V_kappa knows all that V_kappa knows about V if kappa is strong. (This is all probably too naive to be taken seriously, anyway. And, as I said, is an old position I haven't reexamined critically in years.)

@AndrésE.Caicedo Oh oops I misread.

@user21820: if we think we can force over V then it can never be as wide as it could be

Even before forcing, Zermelo recognized that V can never be as tall as it could be, because as soon as we see how tall it is, there will be a longer universe as well.

@CarlMummert Um isn't that contrary to what @AndrésE.Caicedo just said? He thinks/thought that V is too wide to satisfy too-strong reflection principles?

Unless you think that it is as wide as forcing still permits it to be...

Does ω[2] even exist... lol

I think it is consistent with what he said, in some sense, depending on what we mean by V

Hi all!

Is it correct if I say for (b), $\varphi= (\forall y)(\exists x)(xy=y=yx)$, and for (c), $\sigma= (\forall y)(xy=y=yx)$,

@LeylaAlkan (b) they mean "whose only free variable is x"

and in your answer, "x" isn't a free variable

also "xy" isn't defined

oh well you swapped (b) and (c)

also "xy=y=yx" doesn't make sense

Oh, I copied wrongly

define what

what I mean is that you should write f(x,y) instead of xy

for b, you mean something like this: $\varphi= (\forall y)(f(x,y)=f(y)=f(y,x))$ ?

f(y) doesn't make any sense

yep :/