@TimothyChow Exactly. If an inconsistency in ZFC is discovered in the future, it obviously and trivially can be used to construct Russell's set again. So saying "ZFC overcomes all the paradoxes" and "those paradoxes indeed do not manifest themselves in ZFC" clearly implies consistency of ZFC. Failure to realize that is clearly causing confusion to Sergei and whoever reads his post. One cannot expect to get an answer to a question that isn't phrased correctly...

Which introductory book on logic will be best for an Undergraduate? I mean discussed everything clearly

@TimothyChow As for NBG and MK, I understand the concern to be whether there is a known inconsistency in MK, which isn't answered by the lack of known inconsistency in ZFC. And concerning NBG, do you know roughly what is required to prove that it is conservative over ZFC? It is obviously (even to PA) conservative if we only have normal AC (rather than global AC), but I'm not sure whether set theory is needed to show the same for global choice.

Godel/Rosser incompleteness theorems with computability-based proofs

@UnknownMathMan If you have some background with basic undergraduate such as group theory, then you might like Hannes' notes, linked from the post I just pinned on the star-board.

Yes, I have covered group theory, linear algebra, number theory etc.

@user21820 Is there any good online course in logic?

@UnknownMathMan I have not found any that I really like, so if you go through any of those texts I recommend you can ask questions here.

Ok

@TimothyChow Tim, you told that there are proofs of, how to say, "mutual relative consistency of ZFC, NBG and MK"?

@MaliceVidrine Malice, how should I formulate my question correctly in you opinion?

@SergeiAkbarov: MK proves the consistency of ZFC. NBG is consistent if and only if ZFC is, if and only if ZF is. But the consistency of ZFC is a weaker assumption than the consistency of MK.

@user21820 You're right about MK being stronger than ZFC of course. In terms of what is needed to prove that NBG is conservative over ZFC (or that NBG and ZFC are equiconsistent), in principle you need almost nothing. When thinking through how the proof goes, one of course reasons set-theoretically, but the final claim is just that "every theorem of X is a theorem of Y" and this syntactic statement doesn't need strong metatheoretical assumptions to prove.

@SergeiAkbarov This MathOverflow question may be useful to you as far as Morse-Kelley is concerned. mathoverflow.net/questions/87238/… The equiconsistency of NBG and ZFC goes back to von Neumann himself. I don't have a reference offhand but this should be easier to find than an explicit statement that ZFC contains no known contradictions.

@TimothyChow: I think that it is also possible to define an interpretation of NBG in ZFC, so that we have a proof theoretic argument for their equiconsistency

but I am not certain at the moment ...

No, I think I am just not thinking clearly.

@TimothyChow @CarlMummert: So is any of you saying that PA |− Con(ZFC)⇒Con(NBG), where NBG has global choice?

And while we're on this topic, does PA |− Con(ZF)⇒Con(ZFC)?

I think the answer to the last question is yes, by interpreting in L, which works if Con(ZF) is true? If so, can the same trick work to get GC in L and hence interpret NBG in L in ZFC?

@user21820 may I ask from where the ⇒? Are you copy paste it?

@Holo I use a script that allows me to press certain keys to input some symbols that I commonly use.

@user21820 is the script public use? It sounds convenient as not always there is Mathjax

@Holo It's my own GreaseMonkey script, but arguably a better way for just symbols would be to use AutoHotkey so that it works throughout Windows. AHK is easy to set up, and very very powerful. I even use it to implement my own mouse driver on top of the default one:

@user21820 Yes, those relative consistency results are provable in PA.

@user21820 thanks! I will look into it