29

Many students' first introduction to the difference between classes and sets is in category theory, where we learn that some categories (such as the category of all sets) are class-sized but not set-sized. After working with such structures, we discover that it is still worthwhile to sometimes treat them as if they were set-sized. But we can't always do so, without running into contradictions. A natural solution to this problem is the "Axiom of Grothendieck Universes". We then work not with the category of all sets, but the category of sets inside some given universe. This type of framework has been used by many notable mathematicians and seems very ubiquitous. For instance, it was an assumption in my universal algebra textbook. I would venture to say that most modern set theorists look at such an axiom as a very tame assumption.

My first question concerns the possible dangers of such an assumption, which are not often raised when first learning about this axiom. One obvious danger is that this axiom might lead to an inconsistency. In other words, ZFC might be consistent but ZFC+Universes might be inconsistent. I don't personally subscribe to this belief, but it is certainly a possibility (without further, even stronger, assumptions).

What really concerns me is the possibility of another danger: Could such a system proves false things about the natural numbers? In other words, even if we assume that ZFC+Universes is consistent, could it be the case that it proves false arithmetic statements?

The motivation for this question came from reading some of the work of Nik Weaver at this link, which argues for a conceptualist stance on mathematics. In particular, if we reject the axiom of power set, we are led to situations where all power sets of infinite sets are class-sized. Nik puts forth the idea that ZFC might prove false things about the natural numbers. Is this a real possibility? I suppose so, since it is possible that ZFC is inconsistent but the natural numbers aren't. But is it still possible even if ZFC is consistent? More generally:

Could treating the power set of the natural numbers as a set-sized object, rather than a class, force us to conclude false arithmetic statements (even if such a system is consistent)?

Even if the answer to this question is yes, I'm having a hard time seeing how we could recognize this fact, since according to the answers to this linked question it is difficult to state precisely what we mean by the natural numbers.

A second motivation for this question comes from what I've read about the multiverse view of set-theory. When creating a (transitive) model $M$ of ZFC, the set $P(\mathbb{N})$ can often be thought of as some "bigger" power set of the natural numbers intersected with the model. Moreover, via forcing, it seems that one can (always?) enlarge the power set of $\mathbb{N}$. This does seem to suggest that $P(\mathbb{N})$ is not completely captured in any model. Thus, in its entirety, perhaps $P(\mathbb{N})$ should be treated as a class-sized object.

Added: I believe that the current proof we have of Fermat's Last Theorem uses the existence of a(t least one) Grothendieck universe. However, my understanding is that this dependence can be completely removed due to the fact that Fermat's Last Theorem has small quantifier complexity. I imagine that proofs of statements with higher quantifier complexity that use Grothendieck universes, do not necessarily have a way of removing their dependence on said universes. How would we tell if such arithmetic statements are true of the natural numbers? [Some of this was incorrect, as pointed out by David Roberts and Timothy Chow.]

2nd addition: There are some theories that we believe prove false arithmetic statements. Assuming the natural numbers can consistently exist (which we do!), then both PA+Con(PA) and PA+$\neg$Con(PA) are consistent, but the second theory proves the false arithmetic sentence $\neg$Con(PA).

My question then might be rephrased as:

What principles lead us to believe that "Universes" is a safe assumption, whereas "$\neg$Con(PA)" is not safe, regarding what we believe is "true" arithmetic? (Next, repeat this question regarding the axiom of power set.) Is any theory that interprets PA "safe", as long as it is consistent with PA, and PA+Con(PA), and any such natural extension of these ideas?

Another way of putting this might be as follows:

Is the assumption Con(PA) a philosophical one, and not a mathematical one?

This ties into my previous question that I linked to, about describing the "real" natural numbers.

Pace Nielsen
  • 18,047
  • 4
  • 72
  • 133
  • 2
    @jon The "category of all categories" runs into similar paradoxes as the "set of all sets", whereas the "category of all $U$-small categories" doesn't. We'd like to freely work with the standard categories (of groups, sets, monoids, etc...) as if they (together) can form a new collection which forms the object set of a category, and morphisms between them are functors. The standard way this is done is by working with the $U$-small categories instead. For this and other examples, look where textbooks make use of the axiom of universes. – Pace Nielsen Jun 19 '19 at 18:49
  • 4
    I don't understand the question in the box -- in most of mathematics, $P(\mathbb N)$ is treated as a set and not a class. So it sounds like you're simply asking whether ordinary mathematics can prove false arithmetic statements. But I get the impression from the surrounding discussion that you're trying to ask something specific about Grothendieck universes... I don't know what you're asking though. – Tim Campion Jun 19 '19 at 19:05
  • 2
    @TimCampion In most of mathematics $P(\mathbb{N})$ is treated as a set, but not in conceptualist mathematics. In (at least) one of the linked paper's by Nik Weaver, it is claimed that ZFC might prove false things about the natural numbers. I'm trying to get an idea of what that would mean---apart from the obvious point that if ZFC is inconsistent then it proves all things. You can think of the boxed question as a refinement of the question about Grothendieck universes, to the context of conceptualist mathematics vs. "ordinary mathematics" (as you put it). – Pace Nielsen Jun 19 '19 at 19:21
  • @TimCampion I added a paragraph at the end of the question that I hope illuminates things further. – Pace Nielsen Jun 19 '19 at 19:33
  • 8
    Ok. So there are two things going on in your question: 1.) You're asking whether "conceptualist mathematics" might prove different arithmetical statements then ZFC, say -- a mathematical question. 2.) You're asking whether there are reasons to think that the arithmetical consequences of one theory are more "true" than another--a philosophical question. To answer either question would require a much more precise specification of which theories, exactly we're discussing. FWIW I've never heard of "conceptualist mathematics" but generally restricting the powerset axiom is called "predicativism". – Tim Campion Jun 19 '19 at 19:34
  • 1
    @TimCampion Thank you for that distinction. In the context of ZFC vs. ZFC+Universes, the answer to #1 is no (assuming ZFC+Universes is consistent), but I am indeed interested in knowing the answer in the context of conceptualist (or predicativist) mathematics. I'm not knowledgeable enough to know if it just boils down to consistency issues. – Pace Nielsen Jun 19 '19 at 19:43
  • On question #2, I'll post an addendum to my question to clarify things. – Pace Nielsen Jun 19 '19 at 19:45
  • 2
    Just some remarks. 1) By using second-order ZFC, the internal power set operation coincides with the external one (this is essentially why models second-order ZFC and Grothendieck universes are the same thing). 2) Consistency of PA is certainly a philosophical question. It boils down to whether the standard model is really a model. Now, universes are $V_{\kappa}$'s (for $\kappa$ strongly inaccessible) and these models are usually considered the intended models of ZFC when you think about a cumulative hierarchy. They have nice properties such as a "true" power set operation. – user40276 Jun 19 '19 at 20:47
  • 3
    "my understanding is that this dependence can be completely removed due to the fact that Fermat's Last Theorem has small quantifier complexity." No, the use of Grothendieck universes can be removed because they are unnecessary for treating the necessary topos theory for relatively small sites, not due to the complexity of the statement of FLT. – David Roberts Jun 20 '19 at 01:23
  • 2
    Also, since others mentioned reflection, in terms of provability, ZF and ZF + "there exists a universe" are not really that different. Indeed, one can canonically add a new constant symbol which mimics the universe (this is due to Fefferman). This new theory is a conservative extension of ZF. One can iterate this a countable number of times and still get something conservative. – user40276 Jun 20 '19 at 02:40
  • 1
    @jon étale cohomology (of a given scheme) is the derived functor cohomology of the étale topos attached to that scheme. Colin McLarty proved that relatively weak axiomatic systems equiconsistent with higher-order arithmetic can construct the relevant derived functors: https://arxiv.org/abs/1102.1773 "We formalize the practical insight by founding the theorems of EGA and SGA, plus derived categories, at the level of finiteorder arithmetic" (see also https://arxiv.org/abs/1207.6357) – David Roberts Jun 20 '19 at 06:58
  • 1
    @jon I should point out the lower bound with current technology: https://arxiv.org/abs/1207.0276 "The cohomology of coherent sheaves and sheaves of Abelian groups on Noetherian schemes are interpreted in second order arithmetic by means of a finiteness theorem. This finiteness theorem provably fails for the etale topology even on Noetherian schemes." – David Roberts Jun 20 '19 at 07:06
  • How is "could be inconsistent" a different danger than "could prove false things about natural numbers"? – Hagen von Eitzen Jun 20 '19 at 10:30
  • 4
    @HagenvonEitzen Consistency and truth are two different things. For instance, $PA + Con(PA)$ and $PA + \neg Con(PA)$ are both consistent, but at most one of them can be true -- after all, one of them asserts $Con(PA)$ while the other asserts $\neg Con(PA)$! Depending on your philosophy, you might deny that it is ultimately meaningingful to ask whether / assert that a mathematical theory is "true". But in this case, you can still "model" the situation as follows: when somebody makes such assertions, interpret them as being relative to some (unspecified) "ultimate metatheory". – Tim Campion Jun 20 '19 at 13:31
  • 1
    For a meatier example, ZF + AD and ZFC are both consistent, but at most one of them can be true, because they contradict each other. If you subscribe to some kind of mathematical pluralism, the way to think of it is that they can't both be true in the same context -- because they contradict each other! – Tim Campion Jun 20 '19 at 13:32
  • 3
    Even before the philosophical issues concerning universes, we would have to deal with those for ZFC. See this post. And not all logicians are convinced that even just full second-order arithmetic is arithmetically sound, since after all there is no solid ontological basis for impredicative second-order comprehension. So if you are feeling philosophically suspicious, you would really have to examine your views on the powerset of the naturals very carefully, and perhaps you might decide that ZFC is not even the first dangerous point... – user21820 Jun 20 '19 at 13:42
  • 1
    You make it sound as if students are being taught Ferge's set theory. I've never seen a course, as dull (in set theory) as it was where they didn't at least mention Russell's paradox. – Asaf Karagila Jun 20 '19 at 15:06
  • 4
    Re: Fermat's last theorem, you're conflating the issue of universes (which can only be removed by actually looking at the proof - no general metatheorem applies) with choice (where we have a metatheorem, namely absoluteness, which automatically removes choice based purely on the syntactic complexity of the theorem itself). – Noah Schweber Jun 21 '19 at 02:50

4 Answers4

22

For what it's worth, the reason I made that comment was because when I gave talks expressing skepticism about the philosophical basis of ZFC, I would often get the reaction "but as long as it's consistent, what's the problem?" Some version of this attitude is also quite prevalent in the philosophical literature on the subject. I wanted to make the point that just being consistent isn't good enough: ZFC might well be consistent yet still prove, for example, that some Turing machine halts when in fact it does not. If you're a skeptic about sets but not about numbers, this could be a concern.

As for the "safety" of assuming ZFC is arithmetically sound, it is clear that as long as ZFC is consistent, no weaker system could prove that it is unsound. So for predicativists like me, who generally work in much weaker systems than ZFC, it seems unlikely that we could ever establish unsoundness. In that sense I'd say it's pretty "safe" to assume it is sound.

However ... I regard the Peano axioms as expressing intuitively evident truths about the natural numbers, so I have no problem affirming Con(PA). Whereas I regard ZFC as what you get when you realize that full comprehension leads to inconsistencies, so you replace it with a hodgepodge of instances of comprehension which appears to be weak enough to block any paradoxes. (Edit. In case my meaning isn't clear: the axiom of pairing is an instance of full comprehension, the axiom of unions is an instance of full comprehension, the axiom of power sets is an instance of full comprehension ... Basically what you're doing is throwing in a bunch of unrelated instances of "for any property $P$ there is a set of all $x$ such that $P(x)$.") It seems to me quite ad hoc and unmotivated, so although we might (or might not) be confident that ZFC is consistent, there is little reason to expect it to be (or not to be) arithmetically sound.

(I should add that I regard the "iterative conception" which is supposed to justify ZFC as utterly unconvincing. Sets are said to be built up in stages, and then it is parenthetically added that they are, of course, timeless abstract objects so they aren't really "built", nor do they really "appear" in "stages" --- it's all just a "metaphor". Thus "any conviction that the iterative conception may carry is made to depend on metaphorical details that are dismissed as inessential to it." (I. Jane))

Nik Weaver
  • 42,041
  • +1 Thanks for the background! – Pace Nielsen Jun 20 '19 at 00:30
  • You're very welcome. Thank you for the interest! – Nik Weaver Jun 20 '19 at 01:20
  • 1
    “Hodgepodge”?? The instances we take are every class intersected with every set! This isn’t NF! – Monroe Eskew Jun 20 '19 at 06:11
  • 4
    As you stated, we’d never be able to come across a reason that it’s unsound. So the only way we’d get “no reason” to believe in soundness is if we are radical and dismiss the intuition of the vast majority of mathematicians as having no import. I know that’s your whole schtick but I want to point out that it’s radical. – Monroe Eskew Jun 20 '19 at 06:19
  • 2
    Do the inductive constructions in type theory strike you as less of a hodgepodge? – Andrej Bauer Jun 20 '19 at 06:58
  • @AndrejBauer: I do, but in that setting there are circularity issues that haven't been appreciated; see Sections 10 and 11 of this paper of mine. – Nik Weaver Jun 20 '19 at 10:48
  • 3
    Your claim "as long as ZFC is consistent, no weaker system could prove that it is unsound" seems to be blatantly false. If someone does manage to construct a proof within ZFC of ( ZFC is inconsistent ), then we definitely can conclude that ZFC is unsound, even from the perspective of a very weak meta-system, because we can verify that ( ZFC proves ¬Con(ZFC) ) purely mechanically. In fact, we do not even need that much. It suffices if anyone constructs a ZFC proof of ( ZFC is Σ[n]-unsound ) for any fixed n. – user21820 Jun 20 '19 at 13:24
  • On the Turing Machines front, if a TM halts (on a given input) then Peano proves it, the proof being simply to write out the computation up to halting; the same goes for does not halt before time t. So I guess the only possibility left is that you are worried ZFC+Universes might prove that a given 'really' non-halting TM halts but the proof does not give any bound on the halting time? But this still implies ZFC+Universes is inconsistent, though this time the argument is not intuitionistic (unsurprisingly)..! – user36212 Jun 20 '19 at 13:46
  • @user36212: fair point, of course I meant "any weaker system which is known to be sound". – Nik Weaver Jun 20 '19 at 14:08
  • It is easy to sit on a high chair and make claims that this or that theory is unmotivated. We all do that from time to time. That's just how being a human being works. But I can tell you that once you start working with ZFC and do set theory, rather than using set theory to construct the real numbers "and more or less that's it", the motivation become much clearer. The same can be said about chasing large cardinal axioms, weak choice principles, or reverse mathematics, or any other theory. If you're far away, the technical details will seem fuzzy, and confusing. – Asaf Karagila Jun 20 '19 at 15:15
  • 7
    @AsafKaragila I don't think your criticism is apropo. Nik has done lots of serious work with set theory, including writing a treatise on forcing for the regular mathematician, using diamond principle to solve problems in algebra, etc... – Pace Nielsen Jun 20 '19 at 15:35
  • 19
    @AsafKaragila: Your point is fair, but in the converse direction, it’s easy to get Stockholm syndrome: Once you’re deeply familiar with the consequences of some definition, they shape your intuition, and so the definition feels natural because it matches this intuition so well. So even when some definition is terribly ad hoc, its adherents will find it natural. Most arguments about foundations come down in large part to these two effects: people overlook kludges in the systems they’re most familiar with, and are disproportionately conscious of them in other systems. – Peter LeFanu Lumsdaine Jun 20 '19 at 16:30
  • @Peter: And who's to say thar Nik doesn't have Stockholm Syndrome towards predicative mathematics? – Asaf Karagila Jun 21 '19 at 03:24
  • 2
    @Asaf: absolutely, I didn’t mean to direct that admonition just at ZFC-ists — I think most of us who care about foundations are guilty of it to a grease or lesser extent :-) – Peter LeFanu Lumsdaine Jun 21 '19 at 07:01
  • 1
    @MonroeEskew: You're just wrong, because PA+Con(ZFC) certainly proves Con(ZFC). In any case, that is irrelevant since I never said anything about proving Con(ZFC). The proof of my claim is quite trivial: (Work within ATR.) If ZFC proves ( ZFC is inconsistent ), then either ZFC is inconsistent and thus unsound, or ZFC is consistent and thus unsound because it proves a false Σ1-sentence. Even just ACA can easily prove ( If ZFC proves ( ZFC is inconsistent ), then ZFC is Σ1-unsound ) where "Σ1-unsound" is encoded. So it is wrong for Nik to say weaker theories could not prove unsoundness of ZFC. – user21820 Jun 21 '19 at 07:26
  • 5
    @Pace: I'm not here to trash Nik or his knowledge of set theory, and I think he's well versed in what he's saying. But I think that people are the product of their views. I find it almost disparaging to call ZFC "hodgepodge", and double-down by saying that the iterative concept is "utterly unconvincing". I found it very convincing. I don't find statements like "true" and "false" convincing, though, I mean, who made you the king of everything that you can know what is true and what is false. So what? – Asaf Karagila Jun 21 '19 at 07:40
  • 4
    @user36212 : Let M be the Turing machine that, on empty input, searches for a contradiction in ZFC. It could be the case that M does not halt, yet ZFC proves $\neg$Con(ZFC) and hence that M halts. This would not by itself show that ZFC is inconsistent. – Timothy Chow Jun 21 '19 at 20:04
12

This answer repeats some of the material in other answers but I think it is not entirely redundant.

As you seem to have realized, the assertion that a theory is consistent is a much weaker statement than the assertion that the theory does not prove false arithmetical statements (or is "arithmetically sound", to use the standard terminology). So the answer to your question about whether it could be the case that ZFC + universes is consistent but not arithmetically sound is yes, but for perhaps a trivial reason: ZFC + universes could be consistent and yet ZFC itself could fail to be arithmetically sound. Probably what you really wanted to ask was, if ZFC is arithmetically sound, and ZFC + universes is consistent, does it follow that ZFC + universes is arithmetically sound? The answer is no. For example, it is conceivable that under these hypotheses, ZFC + universes could prove $\neg$Con(ZFC). (EDIT: This was a typo. I meant that ZFC+universes could prove $\neg$Con(ZFC+universes). Thanks to Noah Schweber for catching this—see the comments.)

Any feeling that universes are a "safe" assumption must come from a direct assessment of the universes axiom itself. The reasons are similar to the reasons that we have for believing that ZFC is arithmetically sound.

The ability to remove Grothendieck universes from the proof of Fermat's Last Theorem cannot be deduced from some simple abstract fact like "Fermat's Last Theorem has low quantifier complexity." No meta-theorem of this sort is known. Eliminability must come from careful examination of the nitty-gritty details of the proof.

Your question about whether Con(PA) is philosophical or mathematical needs clarification. Offhand, it sounds like a false dichotomy to me, predicated on dubious assumptions about the meaning of the words "philosophical" and "mathematical." Can you define precisely what you mean by a "mathematical" assumption? Are you implicitly assuming that "mathematical" assumptions are rock-solid while "philosophical" ones are not? If so, that in itself is a dubious assumption IMO.

Timothy Chow
  • 78,129
  • 1
    "For example, it is conceivable that under these hypotheses, ZFC + universes could prove ¬Con(ZFC)." That's definitely false: ZFC + universes proves Con(ZFC), so if ZFC + universes is consistent it can't prove $\neg$Con(ZFC). – Noah Schweber Jun 21 '19 at 02:43
  • Whoops! I mean that ZFC + universes could prove ¬Con(ZFC+universes). – Timothy Chow Jun 21 '19 at 02:44
  • 6
    "No meta-theorem of this sort is known" Or, indeed, possible, since Con(ZFC) is a $\Pi^0_1$ statement already! – cody Jun 21 '19 at 12:55
  • @TimothyChow Thank you for this answer. Would you have a good reference where I can learn more about (and the explicit definition of) arithmetical soundness and/or soundness in general? – Pace Nielsen Jun 21 '19 at 15:54
  • 2
    @PaceNielsen : I would suggest Torkel Franzén's book Inexhaustibility: A Non-Exhaustive Treatment, especially Chapter 7, which gives a detailed explanation of arithmetical truth. – Timothy Chow Jun 21 '19 at 17:17
  • 1
    By the way, in case you missed it, this MO question might interest you: https://mathoverflow.net/questions/331441/do-grothendieck-universes-matter-for-an-algebraic-geometer/331887#331887 – Timothy Chow Jun 24 '19 at 15:04
7

There's a lot going on in this question; let's break it down:

Is the assumption Con(PA) a philosophical one, and not a mathematical one?

I suppose it depends on what you mean by "the assumption Con(PA)":

  • If you're writing a mathematical proof, then either the foundations you're assuming prove Con(PA) or they don't, and it's a mathematical question which is the case. You'll be mathematically justified in assuming Con(PA) in the former case. In the latter case, there are contexts where "assuming Con(PA)" is mathematically justified -- for example, if you're trying to prove a statement of the form $Con(PA) \Rightarrow P$ for some $P$, then you're allowed to argue by assuming Con(PA) and proving $P$. But probably that's not what you mean.

  • If you're just asserting "PA is consistent" in a non-mathematical context, then your statement requires some philosophical unpacking to make precise, and moreover to determine to what extent it is justified. In this sense, it's a philosophical statement.

What principles lead us to believe that "Universes" is a safe assumption, whereas "¬Con(PA)" is not safe, regarding what we believe is "true" arithmetic?

There is an extensive philosophical literature discussing justifications for large cardinal axioms. You might start here. I'm not an expert, but I'm not aware of arguments which specifically argue that one should accept the arithmetic consequences of large cardinal axioms without arguing that one should accept the axioms outright. I would be interested to see such an argument. I once asked this question with related motivations.

I think the relevant thing to say is that I've never heard of similar sorts of justifications for $\neg Con(PA)$, and I don't expect I will.

(Next, repeat this question regarding the axiom of power set.)

Restrictions on powersets are studied in predicative mathematics. For some discussion of predicativism, one might start here or here. For some arguments for impredicativism, one might start here.

Is any theory that interprets PA "safe", as long as it is consistent with PA, and PA+Con(PA), and any such natural extension of these ideas?

By "safe", I take it that you continue to mean that the theory's arithmetic consequences are "true". There is a large body of literature discussing truth in mathematics. You seem to be particularly interested in the hierarchy obtained by passing from $T$ to $T + Con(T)$ iteratively. This hierarchy appears to be discussed from a philosophical perspective here. I think most logicians would probably agree that ascending this hierarchy adds relatively little consistency strength. And I'm not aware of serious attacks on the common-sense idea that if one believes $T$ is true, then one should also believe that $T + Con(T)$ is true.

Again, I'm not an expert, but it seems to me that most of the time when trying to justify stronger axioms from weaker assumptions, one appeals to some sort of reflection principle. This concept seems to be relevant to several of the questions you're asking.

You might also be interested in Reverse mathematics, where the "strength" of a mathematical theorem is calibrated by finding just how weak of a foundational theory can prove the theorem. One can interpret this as finding how "safe" a theorem is -- if you can prove it in a weaker theory, then it will continue to be true even if stronger theories are inconsistent, or simply "false".

Tim Campion
  • 60,951
  • Regarding your second-to-last paragraph, on "truth" in mathematics, how would you interpret the wikipedia article on Goodstein's Theorem, as it asserts that this is "a true statement that is unprovable in Peano arithmetic". What do they mean by "true" in this context? I think my comment about "safe" means "consistent with anything that we naturally would take to be true"---but I'm also a little confused at what things we take to be true! – Pace Nielsen Jun 20 '19 at 00:37
  • 4
    That statement makes sense if you don't read too much into it: if a statement is provable in ZFC, then it's standard mathematical practice to regard it as true. So the statement isn't that different from saying "Goodstein's theorem is a theorem of ZFC but not of PA". (Of course, Goodstein's theorem can presumably be proven using less than the full strength of ZFC, but that's beside the point.) – Tim Campion Jun 20 '19 at 03:41
  • 3
    @TimCampion : I've met people who are comfortable accepting the 1-consistency of a large cardinal axiom but not the large cardinal axiom itself. Roughly speaking, they're suspicious of set theory and so don't want to endorse an actual set-theoretic axiom, but they're comfortable with arithmetic and are willing to accept "inductive evidence" that a set-theoretic axiom is 1-consistent. I don't know that anyone has tried to make this argument formally, though. – Timothy Chow Jun 21 '19 at 20:17
  • @TimothyChow I'm not sure what you mean by "1-consistent" -- do you mean that the theory doesn't prove all arithmetic sentences? But then it follows that the theory is consistent, so 1-consistency comes out the same as consistency! I can see how there would be space to believe that large cardinals are consistent without believing that they're true. What I would find exotic would be the view that the arithmetic consequences of large cardinals are true, but the large cardinals themselves are not. – Tim Campion Jun 21 '19 at 20:27
  • 3
    @TimCampion : 1-consistency is a standard technical term meaning that all $\Sigma_1^0$ consequences are true, or if you like, that every Turing machine that it claims halts really does halt. So it's a weak form of your "arithmetic consequences are true." Most of if not all of Harvey Friedman's "necessary uses of large cardinals" are combinatorial statements that are equivalent to the 1-consistency of a large cardinal axiom (and are provable by a slightly stronger large cardinal axiom). I know people who are willing to accept the combinatorial statement but not the large cardinal axiom itself. – Timothy Chow Jun 22 '19 at 00:39
6

Let us abbreviate ZFCU = ZFC + "Every set is contained in a Grothendieck universe." Here is why ZFCU is a "safe" assumption. Suppose it actually is consistent. Then it cannot possibly prove any arithmetical statement that contradicts an arithmetical theorem of, for example, $n^{th}$-order PA for any $n$. This is because it proves that $n^{th}$-order PA has an "internally standard" interpretation, and so everything that it proves about the naturals is true of the "standard" model (i.e. within the theory ZFCU), and thus agrees with everything "true" (true according to ZFCU).

If we further assume that ZFCU has an actually standard model, then this means that all its arithmetical theorems are actually true. But this kind of begs the question, I think. We would like to know about some kind of coherency between various theories at a syntactical level, that they don't prove contradictory arithmetical statements (or other statements about "standard objects").

The idea, I believe, is that if we can organize them linearly in a "standard interpretation hierarchy," then we are fine as long as we believe in the consistency of the strongest theory under consideration. To be more precise, we look at theories $T$ which have a "natural numbers object" $\mathbb N^T$, which should at least satisfy PA. If $S$ is another such theory, and $T$ proves that $S$ has a model $\frak A$ such that $\mathbb N^{\frak A} = \mathbb N^T$, then $T$ and $S$ cannot disagree about what their respective natural numbers object satisfies.

I don't at present have an all-encompassing definition of "standard model," but here are some examples to illustrate the idea.

Example: ZFC proves that for all $n<\omega$, $\mathbb N$ satisfies $n^{th}$-order PA.

Example: ZFCU proves that for each $n<\omega$, there is a standard model of $I_n = $ ZFC + "There are exactly $n$ inaccessible cardinals." This should be the least rank $V_\alpha$ satisfying this theory, so that it is definable. Although the $I_n$ are mutually inconsistent and inconsistent with ZFCU, whatever $I_n$ proves, ZFCU proves it holds in $I_n$'s standard model. $I_n$ has a standard model of $I_m$ for $m<n$. Iterating the operation of taking standard models "commutes" in some sense.

Non-example: ZFCU proves the consistency of $I_1$ + $\neg Con(I_2)$. However, it proves that this does not hold in the standard model.

Monroe Eskew
  • 18,133
  • 1
    I think by "safe" I mean not just consistent with PA, but consistent with all arithmetic true we would naturally accept. This would include Con(PA) as well as Con(PA+Con(PA)), etc... It might also include deeper things like Goodstein's theorem. – Pace Nielsen Jun 20 '19 at 00:39
  • 1
    @PaceNielsen well it proves all of the statements you mention... – Monroe Eskew Jun 20 '19 at 06:06
  • 1
    @MattF. I meant to allow more general examples like for example comparing mutually inconsistent theories in a “standard interpretation” hierarchy. For example comparing $ZFC$ to $ZFC^- +$ “There are exactly 3 infinite cardinals.” I want to say their arithmetical theories are compatible while their general theories need not be. – Monroe Eskew Jun 20 '19 at 20:35
  • 2
    There is a standard way to say that! "ZFC + Universes is conservative over ZFC for arithmetical statements." –  Jun 20 '19 at 21:35
  • 2
    @MattF. But it’s not. The former proves Con(ZFC). – Monroe Eskew Jun 21 '19 at 04:51
  • 1
    Indeed. So it would help to clarify the answer. –  Jun 21 '19 at 10:49
  • 1
    Whoever is downvoting should explain what is wrong with what I said. I would like to know. – Monroe Eskew Jun 22 '19 at 09:05