revised
$\mathbf{P} = \mathbf{NP}$, what's the problem?
edited title
Loading…
revised
Loading…
comment
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
@FrançoisG.Dorais: Are you saying that the linked post is wrong about the strength of CIC being above Z set theory? If not, why did you say that a weak subsystem of Z2 "is the right ballpark"?
comment
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
@FrançoisG.Dorais: It seems that most people use "CIC" to refer to the calculus of inductive constructions with an infinite hierarchy of universes and impredicative Prop, in which case it is way above MLTT. In other words, MLTT is not that strong because it only has a single impredicative notion via W-types, something like how Π[1,1]-CA0 is essentially ATR0 plus a single impredicative notion of closure under monotonic operators. In contrast, CIC with the impredicative Prop far outstrips this kind of impredicativity because it is truly impredicative; we cannot even approach it from below.
comment
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
@TimCampion: Pending clarification of what exactly "CIC" means there, this answer asserts that even without LEM and Choice, CIC is already way stronger than Z, though still weaker than ZFC.
comment
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
@TimCampion: I am also interested in this question, but don't have the expertise to help. Does this article by Rathjen and this post imply that CIC is stronger than MLTT which is stronger than Σ[1,2]-CA+BI? If so, then CIC would be well into impredicativity, far above ATR0.
awarded
comment
Unnecessary uses of the axiom of choice
@TomLeinster: You're not missing anything at all. $ℝ$ and $ℂ$ are very special; you don't need AC to prove that $ℂ$ is an algebraic closure of $ℝ$ either! What is more interesting is that any arbitrary countable field (e.g. $ℚ(t)$ where $t$ is an indeterminate) has an algebraic closure (i.e. an algebraic extension that is closed under algebraic extension), without relying on choice.
Loading…
revised
Loading…
comment
Is true arithmetic + $\lnot Con (TA)$ consistent?
Do you mind taking a look at this question? Thank you!
comment
What "forces" us to accept large cardinal axioms?
And I can't understand why you keep evading the question of whether you believe ZFC has an ω-model, since that is the first question we would have to answer even before talking about the smallest large cardinals. That really is my point; belief in arithmetical soundness matters a lot, and I see absolutely no reason it will ever be "obsolete".
comment
What "forces" us to accept large cardinal axioms?
I think you completely missed my point. If you believe ZFC is consistent, you must believe that ZFC+¬Con(ZFC) has a model. But you have absolutely no reason to study models of ZFC+¬Con(ZFC), because it is meaningless precisely based on your belief.
comment
What "forces" us to accept large cardinal axioms?
Sorry I don't understand how your comment addresses mine. I agree that we should separate consistency and existence, but are you trying to say that your statement "the question of belief becomes obsolete" is only about consistency? Also, I can't understand how large cardinal axioms would be meaningful unless you believe ZFC has an ω-model, and that's why I asked you why you believe it. That is, there does not seem to be much meaning in asking the question "Is ZFC+A consistent?" as a foundational concern if we already believe ¬A.
awarded
revised
Are there infinitely many primes of the form $\lfloor e x\rfloor$ for $x\in\mathbb{Z}^+$?
edited tags; edited title
Loading…
comment
Is a paraconsistent and provably non-trivial foundation for math possible?
@JohannesHahn: I can't make any sense of your comment. To the last sentence, how can a proof that assumes axioms of ZFC lend any credence to consistency of ZFC? To the first two sentences, how can reflection support consistency of ZFC, since it would be meaningless if ZFC is inconsistent, and since it is trivial to extend any theory that interprets PA− to one that proves every finite fragment consistent?
comment
What "forces" us to accept large cardinal axioms?
I believe that your belief that the question of belief is obsolete is false. Here's why. It's possible that ZFC is consistent but has no ω-model (e.g. proves itself to be Σ[k]-unsound for some fixed k, or proves itself to be arithmetically unsound). In that case, sufficiently large cardinals simply don't exist. So you at least have to believe that ZFC has an ω-model. But why do you believe that? Are you sure that unbounded specification plus replacement do not cause it to prove some false arithmetical sentence, and why?
comment
Solutions to the Continuum Hypothesis
@PeterLeFanuLumsdaine: Ah. Well, you said "there is one true world of mathematics, so statements like CH have some actual to-be-determined truth value", which would be based on the (in my opinion) wrong assumption that a platonic mathematical world implies that CH is a meaningful statement. If ZFC is not meaningful, then CH as a set-theoretic statement loses its meaning as well unless you provide an alternative expression of CH within an alternative system.
comment
Solutions to the Continuum Hypothesis
@PeterLeFanuLumsdaine: Your comment seems completely off. As JDH said, more logicians are platonist concerning statements of arithmetic than set theory. Why? Obviously because there is an intended real-world interpretation of arithmetical sentences that yields a real-world structure (at least at human scales) in which every arithmetical sentence has a truth-value. There is no such interpretation of many higher set theories such as Z, not to say ZFC. Therefore almost all normal mathematicians would be platonic about ACA, less about ATR0, less still about Z2, dropping faster beyond that.