User colin mclarty - MathOverflowmost recent 30 from http://mathoverflow.net2013-06-19T04:58:48Zhttp://mathoverflow.net/feeds/user/22809http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/131657/why-did-bourbaki-ignore-the-theory-of-categories/131769#131769Answer by Colin McLarty for Why did Bourbaki ignore the theory of categories?Colin McLarty2013-05-24T20:32:48Z2013-05-24T20:32:48Z<p>These are good answers and I have nothing to add on the particular reasons. To sum it up I would say it was impossible to write a comprehensive Elements of Mathematics based on category theory, because it is impossible to write a comprehensive Elements of Mathematics at all. The brilliant attempt was very good for mathematics, I will maintain, but it could not really be done. </p>
<p>Categories and functors in the 1950s were developed only for immediate applications, and not as a general theory of structure. It was very much easier for Bourbaki to develop a general theory that did not work, than to unify a sprawling mass of working methods into one theory. And nothing was really going to work for their vast project anyway.</p>
<p>So far as I know no one talked about a general theory called "category theory" before biologist Robert Rosen in works like "A relational theory of the structural changes induced in biological systems by alterations in environment" Bull. Math. Biophys. 23 1961 165–171.</p>
http://mathoverflow.net/questions/127456/does-any-lower-bound-on-proofs-of-flt-improve-shepherdson-1965Does any lower bound on proofs of FLT improve Shepherdson 1965?Colin McLarty2013-04-13T12:34:00Z2013-04-16T15:37:21Z
<p>In 1965 Shepherdson proved that FLT is independent of the fragment of PA that uses only open induction and signature $0,S,+\times$. Indeed $2x+1\neq 2y$ is independent of that fragment. Schmerl gives a good general criterion for independence from that fragment in ``Diophantine equations in a fragment of number theory'' in the book Computation and Proof Theory, Springer Lecture Notes in Mathematics Volume 1104, 1984, pp 389-398.</p>
<p>Is FLT currently known to be independent of any larger fragment of PA?</p>
http://mathoverflow.net/questions/127520/are-there-refuted-analogues-of-the-riemann-hypothesisAre there refuted analogues of the Riemann hypothesis?Colin McLarty2013-04-14T09:26:40Z2013-04-14T17:28:21Z
<p>The classical Riemann Hypothesis has famous analogues for function fields and finite fields which have been proved. It has by now very many analogues, many of them still open. Are there important analogues that are now known to be false?</p>
http://mathoverflow.net/questions/127080/what-metatheory-proves-mathsfaca-0-conservative-over-paWhat metatheory proves $\mathsf{ACA}_0$ conservative over PA?Colin McLarty2013-04-10T12:06:42Z2013-04-10T12:26:37Z
<p>Simpson's book shows <code>$\mathsf{ACA}_0$</code> is conservative over <code>$\mathsf{PA}$</code> in the natural way by model theory using definable subsets. Of course, <code>$\mathsf{ACA}_0$</code> being conservative over PA is interesting even apart from consistency strength. So one might not be explicit about the metatheory. And I am sure it is not a strong one. </p>
<p>But I am curious to know the exact logic of this argument. </p>
http://mathoverflow.net/questions/126002/interpretability-and-consistency-strengthInterpretability and consistency strengthColin McLarty2013-03-30T12:09:41Z2013-03-30T14:33:13Z
<p>I have heard there is some fairly recent result showing that whenever theories $T$ and $T'$ have the same consistency strength, then each can interpret the other. I suppose it refers to first order theories, and I do not know exactly what kind of interpretability it uses or what measure of consistency strength.</p>
<p>Can anyone give me the result, or point me in a good direction?</p>
http://mathoverflow.net/questions/122548/notation-for-upperbound-power-setsNotation for upperbound power sets.Colin McLarty2013-02-21T16:54:58Z2013-02-23T02:05:44Z
<p>There is a standard notation $\mathrm{ZF}[n]$ for Zermelo Fraenkel set theory with the power set axiom restricted to saying the set of natural numbers has $n$ successive power sets $\beth_0\dots\beth_n$. </p>
<p>Is there a similarly standard notation for the extension of $\mathrm{ZF}[n]$ by an axiom saying every set has an hereditary embedding in $\beth_n$? </p>
http://mathoverflow.net/questions/120598/when-must-it-be-sets-rather-than-proper-classes-or-vice-versa-outside-of-fou/120679#120679Answer by Colin McLarty for When must it be sets rather than proper classes, or vice-versa, outside of foundational mathematics?Colin McLarty2013-02-03T16:30:47Z2013-02-03T16:30:47Z<p>Proper classes come up when you exhaust the means of forming sets. You need a set when you need to know the means of set theory have not been exhausted -- for example when you want to go on and form a colimit of the structures you have formed so far. Exactly when the means are exhausted, depends on what means of forming sets you have. </p>
<p>First take an example that exhausts second order arithmetic but does not exhaust Zermelo set theory (or simple type theory): the etale fundamental group of an arithmetic scheme. There is no universal cover like the ones for topological spaces and this is not a logical or set theoretic problem but inherent in the situation. (The scheme has etale covers of any finite degree, so a universal cover could have no finite degree.) So Grothendieck and others formed the colimit of all symmetries of the (non-universal, actually existing) etale covers. Second order arithmetic suffices to give the symmetry group of any one etale cover, but because we want the colimit of all these, we need an uncountable group. Second order arithmetic will not produce that. Third order will.</p>
<p>Grothendieck and Dieudonne often found they wanted colimits sort of like this, over all cases of some structure, but not just all that exist in second order arithmetic. Naively put, they wanted all that exist in set theory. Maybe all algebras over some ring, or all finitely generated algebras. They knew there is a big difference between those examples, since there is not even a set of all algebras over a ring up to isomorphism (in any set theory they considered). Choosing one countably infinite set of generators will give you a set of all finitely generated algebras over that ring up to isomorphism. But in either case they did not want to bother with such details. And they were all the more eager to avoid analogous details in more complex cases. </p>
<p>If you really want to talk about all sets, or all natural weak equivalences of functors from Top to Top, or all generalized normal subobjects of $S^2$ in the homotopy category then you are exhausting the means of set theory (though the last two cases are less obvious than the first). </p>
<p>Grothendieck and Dieudonne appreciated the point perfectly. They knew workarounds to fit some of their larger constructions into ordinary set theory, and they were confident other workarounds could be found. But they were not interested in that. They saw that when they used all sets etc., it was not "all" in any metaphysical sense. It was all those constructed by the ordinary means of set theory, so they posited one non-ordinary means of constructing sets: each set is contained in a universe. At any point they work inside some universe, so what would be proper classes in ordinary set theoretic accounts are sets in the next larger universe.</p>
http://mathoverflow.net/questions/112651/how-many-well-orderings-of-aleph-0-are-thereHow many well orderings of $\aleph_0$ are there?Colin McLarty2012-11-17T05:56:42Z2013-01-20T07:06:34Z
<p>What is known about the set of well orderings of $\aleph_0$ in set theory without choice? I do not mean the set of countable well-order types, but the set of all subsets of $\aleph_0$ which (relative to a pairing function) code well orderings. And I would be interested in an answer in, say, ZF without choice. My actual concern is higher order arithmetic.</p>
<p>I would not be surprised if ZF proves there are continuum many. But I don't know.</p>
<p>At the opposite extreme, is it provable in ZF that there are not more well orderings of $\aleph_0$ than there are countable well-order types?</p>
http://mathoverflow.net/questions/117517/authorship-of-grothendieck-universesAuthorship of Grothendieck universesColin McLarty2012-12-29T14:32:16Z2012-12-29T14:32:16Z
<p>Universes seem to first appear in Grothendieck's work in SGA 1, which is credited to Grothendieck, and a lengthy discussion is in the chapter on Prefaisceaux (presheaves) in SGA 4. That chapter is credited to Grothendieck and Verdier. The appendix on them there is credited to N Bourbaki. </p>
<p>Is there any known evidence of who actually wrote the appendix?</p>
http://mathoverflow.net/questions/117371/how-to-measure-the-strength-of-zermelo-over-bounded-zermeloHow to measure the strength of Zermelo over bounded Zermelo?Colin McLarty2012-12-27T23:48:58Z2012-12-28T18:50:57Z
<p>Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so Zermelo proves it is consistent. And Mathias proved a paradigmatic example of the difference: Even if we add choice, Bounded Zermelo proves $\aleph_0$ exists, and every $\aleph_{\alpha}$ has a successor cardinal $\aleph_{\alpha+1}$, while BZ does not prove the quantified statement "for every $n\in \mathbb{N}$, there exists $\aleph_n$." </p>
<p>But is there some more quantitative measure of its strength? For example, do Zermelo and bounded Zermelo have meaningful proof theoretic ordinals? I have heard that proof theoretic ordinals do not work well for theories strong enough to prove existence of power sets.</p>
http://mathoverflow.net/questions/116788/what-is-the-status-of-cantor-schroder-bernstein-in-reverse-mathWhat is the status of Cantor-Schroder-Bernstein in Reverse Math?Colin McLarty2012-12-19T13:58:48Z2012-12-19T20:26:22Z
<p>I'd like to know which of the set theories in SOSOA prove what versions of Cantor-Schroder-Bernstein? For my own purposes I can use arbitrarily high quantifier complexity, but I wonder how little transfinite recursion will suffice.</p>
http://mathoverflow.net/questions/115806/why-the-choice-of-pairing-function-in-subsystems-of-second-order-arithmeticWhy the choice of pairing function in Subsystems of Second Order Arithmetic?Colin McLarty2012-12-08T16:36:50Z2012-12-08T16:36:50Z
<p>Simpson's book uses a pairing function $\langle i,j\rangle = (i+j)^2+j$. Is that choice of function simply unimportant, or does it have expository advantages over the Cantor pairing, or does it have real advantages over the Cantor pairing in terms of quantifier complexity of proofs using it?</p>
http://mathoverflow.net/questions/115351/does-pi1-infty-comprehension-imply-atr-0Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?Colin McLarty2012-12-04T03:18:33Z2012-12-04T03:43:25Z
<p>$\Pi^1_{\infty}\text{-}\mathsf{CA}_0$ proves existence of models of ATR$_0$. But I think it does not imply ATR$_0$, because Axiom Beta is a kind of replacement axiom. Is that right?</p>
http://mathoverflow.net/questions/115207/finite-order-arithmetic-and-etcs/115239#115239Answer by Colin McLarty for Finite order arithmetic and ETCSColin McLarty2012-12-03T03:16:30Z2012-12-03T03:23:52Z<p>Ah, Thomas Forster's 1998 paper "Weak systems of set theory related to HOL" is available on-line at various places including <a href="https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps" rel="nofollow">https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps</a></p>
<p>He says it is proved in</p>
<p>Jensen RB "On the consistency of a slight (?) modification of Quine's NF" Synthese 19 1969 pp 25--63.</p>
<p>Lake J "Comparing Type theory and Set theory" Zeitschrift fur Matematische Logik 21 1975 pp 355-56. </p>
<p>For a fanatically detailed proof and discussion see Mathias at <a href="https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf" rel="nofollow">https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf</a></p>
http://mathoverflow.net/questions/112751/subscript-0-in-reverse-mathematicsSubscript 0 in Reverse MathematicsColin McLarty2012-11-18T09:44:52Z2012-11-18T20:45:08Z
<p>What does the subscript 0 mean on terms like $\mathsf{ATR}_0$? Does it mean the same thing in $\Pi^1_k\text{-}\mathsf{CA}_0$?</p>
<p>If I frame higher order analogues of these, should I change that subscript?</p>
http://mathoverflow.net/questions/112079/what-is-godels-pairing-function-on-ordinalsWhat is Gödel's pairing function on ordinals?Colin McLarty2012-11-11T15:16:34Z2012-11-11T19:17:38Z
<p>I find many references to Gödel's pairing function on ordinals but I have not found a definition. What is it?</p>
http://mathoverflow.net/questions/111898/seeking-name-for-an-order-raising-operator-in-higher-order-arithmeticSeeking name for an order raising operator in Higher Order Arithmetic.Colin McLarty2012-11-09T14:29:59Z2012-11-09T14:29:59Z
<p>Any class $X$ of order $j$ in HOA is in bijection with the order $j+1$ class built up from singletons <code>$\{x\}$</code> of natural numbers $x$ just the way that $X$ is built up from the numbers $x$. And of course this can be iterated any number of times.</p>
<p>Is there a standard, or at least published, name for this order raising operation?</p>
http://mathoverflow.net/questions/111361/can-second-order-arithmetic-make-aleph-1l-countableCan second order arithmetic make $\aleph_1^L$ countable?Colin McLarty2012-11-03T10:47:40Z2012-11-05T02:40:39Z
<p>Simpson's book Subsystems of Second Order Arithmetic shows $Z_2$ can interpret some fragments of ZF strong enough to give good theories of constructible sets and formalize statements like "there is a countable ordinal $\gamma$ such that $\gamma=\aleph_1^L$", Forcing in ZF shows this is independent of ZF and so certainly independent of $Z_2$. But can the independence be proved in some set theory interpretable in $Z_2$?</p>
<p>I ask because I expect it can.</p>
<p>But a positive answer would mean $Z_2$ implies consistency of a fragment of ZF with global well-ordering and existence of $\aleph_1$, obviously without power set. I don't know if that is possible. </p>
http://mathoverflow.net/questions/111176/what-ordinals-are-definable-relations-in-peano-arithmeticWhat ordinals are definable relations in Peano Arithmetic?Colin McLarty2012-11-01T16:56:11Z2012-11-01T17:22:44Z
<p>I am not asking which order types PA proves are well ordered. That would be all up to $\epsilon_0$. Rather I mean, assuming a stronger ambient theory such as Zermelo set theory, which ordinals have the order type of some relation on $\mathbb{N}$ that is defined by a formula of PA (not requiring that PA prove the relation is a well ordering).</p>
http://mathoverflow.net/questions/110487/terminology-for-sequences-and-countabilityTerminology for sequences and countabilityColin McLarty2012-10-23T22:48:48Z2012-10-24T06:27:36Z
<p>This is just a question about terminology. I had thought that "enumerable" is a synonym for "countable," and you could call a set "enumerated" to mean it comes with some specific ordering of type $\omega$ (or an initial segment, if finite). Is that standard or is there another concise terminology for the distinction? </p>
<p>The point is I want a concise way to express the fact that, while ZF does not prove every countable union of countable sets is countable, Zermelo set theory is already more than you need to prove countability of every countable union of sets where each set is given with a specified listing as a sequence. </p>
http://mathoverflow.net/questions/109535/generalizing-feferman-levyGeneralizing Feferman - LevyColin McLarty2012-10-13T14:46:58Z2012-10-15T19:10:58Z
<p>The Feferman - Levy model makes $\aleph_1$ singular by a cardinal collapse $\aleph_1 = \aleph_{\omega}^L$. Unless I've got something wrong, the same thing would work to make any well-orderable cardinal $\alpha$ cofinal in its well-ordered cardinal successor. Is that right?</p>
<p>The Feferman -Levy model also makes the continuum a countable union of countable sets. Does that generalize to Beth numbers, in the sense of successive power sets starting with $\omega$? For each finite $n$, are there models where $\beth_{n+1}$ is a union of $\beth_{n}$ many sets each smaller than or the same size as $\beth_{n}$? </p>
http://mathoverflow.net/questions/109680/does-zf-bound-countable-unions-of-countable-setsDoes ZF bound countable unions of countable sets?Colin McLarty2012-10-15T04:45:14Z2012-10-15T09:21:33Z
<p>ZF proves that whenever a countable union of countable sets can be well ordered then its cardinality is at most $\aleph_1$. But what if it cannot be well ordered? The Feferman-Levy model shows the continuum can be a countable union of countable sets. Is there a ZF proof that a countable union of countable sets must be smaller than or equal to that in size?</p>
http://mathoverflow.net/questions/102372/show-that-a-cartesian-closed-need-not-imply-aj-is-cartesian-closed/104806#104806Answer by Colin McLarty for Show that $A$ cartesian closed need not imply $A^J$ is cartesian closed. Colin McLarty2012-08-16T03:02:38Z2012-08-16T16:22:11Z<p>I think it will not be easy to find an example with $J=2$. Since a cartesian closed category has finite products, the result cited in David White's answer shows the category $A$ for such an example must not have equalizers. So it cannot be a preorder, and so (having binary products) it cannot be finite. It is not hard to find infinite cartesian closed categories without equalizers -- but I have not found one with a specific pair of functors that I can show have no exponential.</p>
<p>The best example that occurs to me has $J$ the poset with bottom element $0$ and a countable infinity of objects right above $0$, with no arrows to each other. That is the partial order on the natural numbers with $x\leq y$ if and only if $x=0$. And for $A$ the category of finite sets (hereditarily finite, if you like ZF foundations and want a small category). The result follows since the functor assigning the empty set to $0$ and the two element set to every other object of $J$ has infinitely many natural transformations to itself (uncountably many).</p>
http://mathoverflow.net/questions/104494/product-operation-name-and-notation/104509#104509Answer by Colin McLarty for product operation: name and notationColin McLarty2012-08-11T18:53:48Z2012-08-11T18:53:48Z<p>Probably $\langle f, g\rangle : C \to A \times B$ is most often just called the arrow to the product. You are right it should not be called a product arrow. People who want a specific name for the operation have called it the "pairing arrow."</p>
<p>I would write $\langle f_i\rangle_{i \in I} : C \to \prod_{i \in I} A_i$ without curly brackets in the angle brackets and i would call it the arrow to the product. A more specific name for the operation could be "tupling arrow."</p>
http://mathoverflow.net/questions/103835/does-higher-order-arithmetic-interpret-the-axiom-of-choiceDoes higher order arithmetic interpret the axiom of choice?Colin McLarty2012-08-03T02:55:58Z2012-08-03T03:49:03Z
<p>By second order arithmetic I mean the axiomatic theory $Z_2$, that is Peano arithmetic extended by second order variables with the full comprehension axiom, and not defined semantically using power set in ZF. By third order arithmetic I mean that extended by third order variables and the comprehension axiom. And so on. Does each of these have an inner model which also satisfies the axiom of choice in each order, using constructibility? If not, do such inner models exist if we also extend induction to a higher order axiom? Is there a good reference on it? </p>
http://mathoverflow.net/questions/103658/why-does-aleph-omega-have-more-than-aleph-omega-countable-subsetsWhy does $\aleph_{\omega}$ have more than $\aleph_{\omega}$ countable subsets?Colin McLarty2012-08-01T05:07:45Z2012-08-01T05:54:45Z
<p>I believe $\aleph_{\omega}$ has more than $\aleph_{\omega}$ countable subsets but I do not see the proof. I fear it is obvious, but not to me today.</p>
http://mathoverflow.net/questions/103448/what-is-known-about-size-restricted-power-set-axiomsWhat is known about size-restricted power set axioms?Colin McLarty2012-07-29T13:32:53Z2012-07-29T21:59:50Z
<p>What is known about ZF without powerset but with an axiom "every set
has a set of all its countable subsets"?</p>
<p>This seems stronger than positing that the set of natural numbers has
a powerset, though I do not know a proof that it is.</p>
<p>More generally, for any definable cardinal $\alpha$, what about the
axiom "every set has a set of all smaller-than-$\alpha$ subsets"?</p>
http://mathoverflow.net/questions/103258/is-there-a-typical-example-of-nisnevich-coversIs there a typical example of Nisnevich covers?Colin McLarty2012-07-27T01:37:32Z2012-07-27T18:26:45Z
<p>There is a popular (and I think helpful) example of etale covers, namely covers of Riemann surfaces with ramification points removed. Is there a similarly accessible example to motivate Nisnevich covers? </p>
http://mathoverflow.net/questions/102463/ideals-of-etale-structure-sheaves/103142#103142Answer by Colin McLarty for Ideals of etale structure sheavesColin McLarty2012-07-26T01:21:26Z2012-07-26T01:28:10Z<p>I must apologize for posting a false answer. in writing up a proof i discovered a gap which grew to a counterexample.</p>
<p>In fact not every sheaf of ideals of an etale structure sheaf is finitely generated. I have added a counterexample to the end of my ArXiv paper on cohomology in second order arithmetic arXiv:1207.0276v2. Intuitively, an etale ideal can hold information about arbitrarily high degree extensions which is not reducible to information about any fixed degree so the ideal is not finitely generated. </p>
<p>The counterexample shows that given any non-zero element $x$ of an algebraically closed field $k$ a single etale sheaf of ideals on the punctuated line $k\0$ can pick one $2^n$-th root of $x$ for every $n$. The example has $x=1$ but rescaling $k\0$ takes 1 to any other $a\neq 0$.</p>
http://mathoverflow.net/questions/102463/ideals-of-etale-structure-sheavesIdeals of etale structure sheavesColin McLarty2012-07-17T15:58:40Z2012-07-26T01:28:10Z
<p>Is it known whether or not every sheaf of ideals of the etale structure sheaf of a Noetherian scheme is generated by finitely many of its sections? Of course it is trivially true for some widely used special cases. But is it known one way or the other, in this generality?</p>
http://mathoverflow.net/questions/131657/why-did-bourbaki-ignore-the-theory-of-categories/131738#131738Comment by Colin McLartyColin McLarty2013-05-25T18:41:36Z2013-05-25T18:41:36Z@quid Well, yes Weil was a huge influence on all of modern pure mathematics. But his most important contributions are very hard to grasp even today, and he is utterly underrated by people who only know his low level ideas as in Bourbaki. He was also a brilliant collaborator to people he respected. But I know myself that to call him acerbic is an understatement. He and Grothendieck eventually could not stand each other. http://mathoverflow.net/questions/131657/why-did-bourbaki-ignore-the-theory-of-categories/131738#131738Comment by Colin McLartyColin McLarty2013-05-25T17:03:34Z2013-05-25T17:03:34Z@quid. You can research and write this history. As to when Grothendieck spoke of "Verflachung" you need no rhetorical question: I give the date with the quote, and I give a footnote saying where he got the term. In the Grothendieck Serre correspondence you must have noticed their complaints about Weil, and I will say I doubt that actually came from Serre though he goes along with it. Serre understood (and understands) Weil very well. I think it came from Grothendieck. I am sure you are right that Grothendieck was also pulled away by his own projects. http://mathoverflow.net/questions/131657/why-did-bourbaki-ignore-the-theory-of-categories/131738#131738Comment by Colin McLartyColin McLarty2013-05-25T14:01:01Z2013-05-25T14:01:01Z@quid. Why is it hard to reconcile Weil being (far) the strongest voice in the group with him following his own rule on retirement? Of course we have much more from the Bourbaki archives now than when I wrote what I did. But it remains that Bourbaki wrote up a theory of structures following what Weil said in 1951 he got from Mac~Lane, while the theory did not actually do what Mac~Lane (or Cartan or Chevalley or Grothendieck) wanted. I am not clear what position Eilenberg took on it.http://mathoverflow.net/questions/128569/a-model-where-dedekind-reals-and-cauchy-reals-are-different/128585#128585Comment by Colin McLartyColin McLarty2013-04-24T15:54:11Z2013-04-24T15:54:11Z@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. http://mathoverflow.net/questions/128569/a-model-where-dedekind-reals-and-cauchy-reals-are-different/128585#128585Comment by Colin McLartyColin McLarty2013-04-24T14:00:16Z2013-04-24T14:00:16ZThe 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. http://mathoverflow.net/questions/128077/needless-axiom-for-grothendieck-topologiesComment by Colin McLartyColin McLarty2013-04-21T00:22:10Z2013-04-21T00:22:10ZI'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.http://mathoverflow.net/questions/127456/does-any-lower-bound-on-proofs-of-flt-improve-shepherdson-1965/127705#127705Comment by Colin McLartyColin McLarty2013-04-16T21:11:44Z2013-04-16T21:11:44Z$T^0_2$ does include Robinson's $Q$, right? Specifically, it includes $x=0\vee \exists y(x=Sy)$?http://mathoverflow.net/questions/127456/does-any-lower-bound-on-proofs-of-flt-improve-shepherdson-1965Comment by Colin McLartyColin McLarty2013-04-16T12:44:01Z2013-04-16T12:44:01ZLast. 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
<a href="http://acunix.wheatonma.edu/bbloch/crypto/day24-25.Fermat" rel="nofollow">acunix.wheatonma.edu/bbloch/crypto/…</a>'s.Little.Theorem.pdf
using it that way.http://mathoverflow.net/questions/127456/does-any-lower-bound-on-proofs-of-flt-improve-shepherdson-1965Comment by Colin McLartyColin McLarty2013-04-14T11:22:29Z2013-04-14T11:22:29ZI'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.http://mathoverflow.net/questions/127080/what-metatheory-proves-mathsfaca-0-conservative-over-pa/127084#127084Comment by Colin McLartyColin McLarty2013-04-10T12:35:14Z2013-04-10T12:35:14ZNice. And this will also do for the proof that $\mathsf{GB}$ is conservative over $\mathsf{ZF}$, right?http://mathoverflow.net/questions/126002/interpretability-and-consistency-strength/126020#126020Comment by Colin McLartyColin McLarty2013-04-10T11:48:35Z2013-04-10T11:48:35ZI have commented above on a proof theoretic result of Friedmana nd Visser.http://mathoverflow.net/questions/126002/interpretability-and-consistency-strengthComment by Colin McLartyColin McLarty2013-04-02T11:45:59Z2013-04-02T11:45:59ZAnd 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.http://mathoverflow.net/questions/126002/interpretability-and-consistency-strengthComment by Colin McLartyColin McLarty2013-04-02T11:42:30Z2013-04-02T11:42:30ZThanks 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. http://mathoverflow.net/questions/126002/interpretability-and-consistency-strengthComment by Colin McLartyColin McLarty2013-03-30T15:25:03Z2013-03-30T15:25:03ZI would not be surprised if the result is for first order theories that interpret Robinson Arithmetic or something like that. http://mathoverflow.net/questions/122548/notation-for-upperbound-power-setsComment by Colin McLartyColin McLarty2013-02-23T14:35:22Z2013-02-23T14:35:22Z 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.