Colin McLarty
|
Registered User
|
|
|
Apr 24 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different @Andrej, Yes, you see yourself as building categories of sheaves at a level like ZFC or HOTT but not using any specific metatheory. This makes it transparent that the two kinds of reals can differ in models of relatively strong (but 'intuitionistic') formal theories like IZF. This is like Cohen presenting forcing as building forcing conditions in ZFC. But Cohen also notes a fragment of arithmetic suffices as metatheory to formalize the reasoning and verify the (non-)deducibility of AC or CH from ZF axioms. I think there is room to talk about both formal systems and ideas. |
|
Apr 24 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different The models are models of different things. Noah says the Dedekind and Cauchy reals can differ in a model of $RCA_0$, while Andrej shows they can differ in models of any of the far stronger background theories he lists. Noah says computability considers can block the proof of equivalance while Andrej notes continuity conditions can. As far as the meta-theoretic assumptions of the two proofs, those are probably identical. |
|
Apr 21 |
comment |
Needless axiom for Grothendieck topologies? I'll just add that Grothendieck probably thought of this as analogous to saying a topology on a set $S$ always has $S$ itself as an open subset. |
|
Apr 19 |
awarded | ● Popular Question |
|
Apr 16 |
comment |
Does any lower bound on proofs of FLT improve Shepherdson 1965? $T^0_2$ does include Robinson's $Q$, right? Specifically, it includes $x=0\vee \exists y(x=Sy)$? |
|
Apr 16 |
awarded | ● Nice Question |
|
Apr 16 |
comment |
Does any lower bound on proofs of FLT improve Shepherdson 1965? Last. I had never seen FLT used to mean Fermat's Little Theorem until you put me on the track of it and I found a cryptography oriented website acunix.wheatonma.edu/bbloch/crypto/…'s.Little.Theorem.pdf using it that way. |
|
Apr 14 |
awarded | ● Good Question |
|
Apr 14 |
awarded | ● Mortarboard |
|
Apr 14 |
awarded | ● Nice Question |
|
Apr 14 |
comment |
Does any lower bound on proofs of FLT improve Shepherdson 1965? I'll mention Hajek and Pudlak in Metamathematics of First-Order Arithmetic (1998) discuss Shepherdson's result without saying his independence results in 1965 extend to any larger fragment. Rather, they say Shepherdson's technique here is so different from the techniques for stronger fragments that they will not go into it. |
|
Apr 14 |
asked | Are there refuted analogues of the Riemann hypothesis? |
|
Apr 13 |
asked | Does any lower bound on proofs of FLT improve Shepherdson 1965? |
|
Apr 11 |
awarded | ● Yearling |
|
Apr 10 |
comment |
What metatheory proves $\mathsf{ACA}_0$ conservative over PA? Nice. And this will also do for the proof that $\mathsf{GB}$ is conservative over $\mathsf{ZF}$, right? |
|
Apr 10 |
asked | What metatheory proves $\mathsf{ACA}_0$ conservative over PA? |
|
Apr 10 |
comment |
Interpretability and consistency strength I have commented above on a proof theoretic result of Friedmana nd Visser. |
|
Apr 2 |
comment |
Interpretability and consistency strength And consistency must be \emph{cut free consistency}. Visser has shown how sequentiality needs to be fine tuned in EA. Visser gave a clear example to show that if we need PA to prove "if $A$ is cut free consistent then so is $B$", then the result does not follow: PA proves both that $I\Sigma_1$ is (cut free) consistent and that $I\Sigma_2$ is cut free consistent, yet the first does not interpret the second. |
|
Apr 2 |
comment |
Interpretability and consistency strength Thanks to all for comments. Phil Ehrlich pointed me the right way privately. Friedman and Visser have shown the implication from mutual interpretability to eqiconsistency is reversible on a certain subtle condition. We can hastily state the theorem as: If $A$ and $B$ are finitely axiomatized and sequential and consistency of $A$ implies consistency of $B$, then $A$ interprets $B$. The sequentiality addresses Simon Thomas's point. The subtlety is the conditions must be provable in EA, arithmetic with $\Delta_0$-induction plus the axiom that exponentiation is total. |
|
Mar 30 |
comment |
Interpretability and consistency strength I would not be surprised if the result is for first order theories that interpret Robinson Arithmetic or something like that. |
|
Mar 30 |
asked | Interpretability and consistency strength |
|
Feb 23 |
comment |
Notation for upperbound power sets. I suspect the notation $\mathrm{ZF}[n]$ comes from Harvey Friedman, in the context of saying that theory has the strength of order n+2 arithmetic. That is where I got it. I have seen it, likely on FOM, but I can't search it by Google since Google refuses to believe I want the square brackets! It gives me pages where virtually every variant possible of ZF by dropping some axiom has been named with a 0 somehow. |
|
Feb 23 |
comment |
Notation for upperbound power sets. That could work as a notation. But it seems odd to invoke cardinal successor in a context where we do not have choice, and especially to invoke the cardinal successor of a set, $\beth_n$, which the theory proves cannot have one. |
|
Feb 21 |
asked | Notation for upperbound power sets. |
|
Feb 3 |
answered | When must it be sets rather than proper classes, or vice-versa, outside of foundational mathematics? |
|
Jan 20 |
comment |
axiom schema versus inference rule This is not a research level question. A more careful reading of the Wikipedia article should clear up your first question entirely and help you understand the second. You could also look at the references in the Wikipedia article. |
|
Dec 29 |
awarded | ● Nice Question |
|
Dec 29 |
comment |
Why is the identity element of a group denoted by $e$? Well, Weber surely popularized the term. But his friend Dedekind used "einheit" before him to mean either a unit in a field, or a unit measure in geometry, and I'll bet if you look in his work you'll find it for groups. Probably if you dig into the 19th century you can find a series of earlier and earlier, vaguer and vaguer, uses of the term for a group identity. |
|
Dec 29 |
asked | Authorship of Grothendieck universes |
|
Dec 28 |
awarded | ● Nice Question |
|
Dec 28 |
revised |
How to measure the strength of Zermelo over bounded Zermelo? Added that my version of Mathias's result assumes choice. |
|
Dec 28 |
comment |
How to measure the strength of Zermelo over bounded Zermelo? Ah, in the absence of choice I should not use $\aleph$s so freely. Mathias shows: Bounded Zermelo proves there are transfinite sets, and any finite list of them can be lengthened, but does not prove the quantified statement "for every $n$ there is a set of $n$ transfinite sets each larger than the last." I would not call it a failure of induction. It is just that induction is stated for subsets of $\mathbb{N}$, and the above statement is not bounded and does not define a subset of $\mathbb{N}$. |
|
Dec 27 |
asked | How to measure the strength of Zermelo over bounded Zermelo? |
|
Dec 19 |
comment |
What is the status of Cantor-Schroder-Bernstein in Reverse Math? If countablity is necessary to to prove CSB in $\mathsf{ATR}_0^{\mathrm{set}$, that would help me know how to direct my efforts. And $\mathsf{B}_0^{\mathrm{set}}$ supports a considerable theory of ordinals. It might prove enough of CSB for me. This is for work in progress and I do not know `how much' of CSB I would need. For now, I wonder what versions of it are available. |
|
Dec 19 |
comment |
What is the status of Cantor-Schroder-Bernstein in Reverse Math? The constructibility theories include global choice, but I am looking at things like $\mathsf{B}_0^\mathrm{set}$ or $\mathsf{ATR}_0^\mathrm{set}$. |
|
Dec 19 |
asked | What is the status of Cantor-Schroder-Bernstein in Reverse Math? |
|
Dec 10 |
comment |
Factoring objects in a category Your question seems worded for tensor product factorization in monoidal categories in general. But you refer to cones and a universal property, which suggests specifically cartesian product factorization. |
|
Dec 8 |
comment |
Why the choice of pairing function in Subsystems of Second Order Arithmetic? Ah, and if I am not missing something, a key point is that the proof $\frac{n^2+n}{2}$ exists uses only bounded quantification. So there cannot be an issue of quantifier complexity. |
|
Dec 8 |
asked | Why the choice of pairing function in Subsystems of Second Order Arithmetic? |
|
Dec 7 |
accepted | Finite order arithmetic and ETCS |
|
Dec 5 |
comment |
Finite order arithmetic and ETCS Yes it is nice. This is subtle stuff and the published terminology is not at all as uniform as I would wish. There is some category theory of middling-weak arithmetic, but much of it is constructive as it is intended for computer programming semantics, and I have not worked on it much. |
|
Dec 5 |
comment |
Finite order arithmetic and ETCS The simple theory of types (including infinity, or plus infinity, depending on author) includes comprehension, and not replacement. This is also $Z_2$ in the references I use - notably Takeuti Proof Theory and Simpson Subsystems of Second Order Arithmetic. I'm not sure what you mean by a Peano-style definition. What is a reference on it? |
|
Dec 4 |
comment |
Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? I agree it is not a bad trap. |
|
Dec 4 |
comment |
Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? Yes, but you can draw conclusions more quickly when one side of the bi-interpretation is a conservative extension, as $\mathsf{ATR}_0^{\mathrm{set}}$ is a conservative extension of $\mathsf{ATR}_0$. Axiom Beta posits precisely that certain transfinite recursions can be done in set theory, corresponding by design to arithmetic transfinite recursion as a subsystem of $Z_2$. |
|
Dec 4 |
comment |
Finite order arithmetic and ETCS For Takeuti, simple type theory is not that, as it does not have Peano axioms. What I call finite order arithmetic is such a union |
|
Dec 4 |
comment |
Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? You can prove an independence claim in the arithmetic by citing one in set theory. I do not understand what you mean is accidental. $\mathsf{ATR}_0$ and $\mathsf{ATR}_0^{\mathrm{set}}$ are bi-interpretable by design. |
|
Dec 4 |
comment |
Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? It is p. 271, with a concise proof. I think my systematic error was not keeping in mind that hereditary countability includes existence of transitive closures, and so proves a lot of things usually proved by replacement. |
|
Dec 4 |
asked | Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? |
|
Dec 4 |
comment |
Finite order arithmetic and ETCS For Takeuti, "simple type theory" is synonymous with "higher (finite) order predicate logic," and does not include an axiom of infinity (though I think for most people simple type theory does include infinity). this is my favorite reference on simple type theory. So I call simple type theory with infinity "finite order arithmetic." |
|
Dec 3 |
comment |
Finite order arithmetic and ETCS Yes. More than knowing ETCS has the strength of bounded Zermelo (which equals the strength of bounded Zermelo with choice) we have many published proofs. I did not look at Jensen or Lake. I could not get Jensen here at home. And I always like to read Mathias. ETCS is actually bi-interpretable with certain variants of bounded Z with choice, meaning they not only have the same strength but prove exactly the same theorems. The main issue there seems to be existence of transitive closures. |
