Can ‘concrete’ statements be undecidable?

[u/Lehatan]

Let me preface by saying that, while I’m a mathematician, I am not a logician. I’m simply curious about the field. This post is about things that have always bugged me about undecidability.

I’ll take the Collatz conjecture (CC) as an example. Suppose the CC is undecidable in ZFC. Then, if we believe ZFC is consistent, we cannot find a counterexample. If we did, this would contradict it being undecidable. This is strange to me: we would have a statement for which we can’t show its truth while knowing we cannot find a counterexample.

Compare this with the continuum hypothesis (CH), the statement people usually refer to as example of undecidable statement. If we choose it to be true, we know there is a subset S of the real numbers which has cardinality between countable and the continuum. CH being undecidable implies that if we believe ZFC is consistent, we will not stumble into such an S by construction (say with schema specification, etc.). If we did, this would contradict ZFC. But that’s ok, because not every subset of the reals can necessarily be obtained ‘constructively’ through schema specification etc. (I am being informal here, but I believe there is a formal way to say this). So us not being able to produce a counterexample of CH does not mean that one cannot exist.

To me, this seems like a different flavour to CC. There, it seems that any counterexample would be constructive (it’s just a natural number!), and hence, if CC is undecidable, such a counterexample cannot exist.

I informally define ‘concrete’ statements are ones which are about ‘constructive’ objects. Thus any counterexample to a ‘concrete’ statement would be constructive, and hence undecidability of a ‘concrete’ statement would ‘say’ that no such counterexample exists (otherwise we would be able to construct it!).

I am left with the question: should we expect ‘concrete’ statements, such as CC, to be decidable? Maybe there is a formal answer to this question, by formalising what a ‘concrete’ statement is, and showing that such statements are decidable. Though, to me, this seems unlikely to be possible, by Gödel.
Moreover Gödel’s incompleteness theorem holds just under Peano Arithmetic, and so it seems to be saying there is a priori no difference between a statement about the natural numbers such as CC and a statement about cardinalities such as CH. But my intuition cannot help but telling me these are of different nature. Am I wrong to assume this?

A more general version of my question is, why as mathematicians do we expect the questions we are working on to be decidable? We get a sense that a proof or counterexample exists, and it seems that outside of certain ‘non-constructive’ parts of mathematics, we never run into such issues.

[u/shuai_bear]

It might help to distinguish the different kinds of undecidability/independence and how the independence phenomenon happens with different undecidable statements:

CH: this is independent of ZFC as you know, proven that we can't disprove it false (Godel constructed a minimal universe of sets where 2^(N_0) = N_1, that is consistent with ZFC) and proven that we can't prove it true (Cohen showed that by forcing, we can enlarge the continuum as much as we want up to Aleph_omega edit - any cardinal of uncountable cofinality, thanks RIyehDreams showing we can create a universe that disagrees with CH but is also consistent with ZFC). CH is independent, but not an example of a true but unprovable arithmetical statement in the flavor of Godel's incompleteness theorem.

CH to me is similar to the parallel postulate of geometry. Both are structural statements where the truth of the statement not being captured by the axioms is not an example of independence of Godel's 1st theorem (true/unprovable arithmetical statements), but a consequence of the axioms under-constraining the theory, allowing multiple and equally valid mathematical universes to exist side by side.

You mentioned Collatz, but let me point out another arithmetical statement we know to be true in arithmetic but unprovable in PA - Goodstein's theorem, which is a statement about fast-growing sequences of natural numbers that asserts all such sequences eventually terminate. Turns out, Goodstein's theorem is unprovable in PA because it requires transfinite induction on epsilon_0, and PA cannot handle that. This is a "concrete" arithmetic-centered statement that was proven to be true but unprovable in PA - ZFC can prove it true, being 'stronger' than PA, but PA cannot because otherwise it would be equivalent to proving the consistency of PA (Gentzen) which Godel's 2nd theorem says we cannot do. ZFC however can prove Cons(PA), and indeed can handle transfinite induction on epsilon_0 which is why it can prove this arithmetic statement but PA cannot, even though PA can express it.

Turns out, since Goodstein's theorem is independent, by Godel's completeness theorem (not incompleteness) there is a non-standard model of arithmetic where the theorem is false. The very rough intuition is that the tail ends of long sequences of natural numbers don't 'behave' in a way that aligns with arithmetic as we know it, but otherwise it is consistent that there is a non-standard model of arithmetic where you have PA's axioms + negation of Goodstein's theorem. So there can be a counter example to this true but unprovable (in PA) statement, just the example is not a natural number from the standard model. In a stronger theory like ZFC however, Goodstein's theorem is true and provably so.

With Collatz, either it's concretely false, and we can find a concrete counterexample, or it's truly independent - and there might be a non-standard model of natural numbers where CC fails, but that we have shown that PA or ZFC cannot prove nor disprove it.

Another example of a seemingly 'concrete' unporvable truth is the solutions to Diophantine equations - a polynomial equation with integer coefficients for which it is impossible to prove whether or not integer solutions exist within a given formal system like ZFC or PA, even though a definitive true answer exists.

It turns out, that proving integer solutions exist for Diophantine equations is equivalent to proving the Halting problem, so despite it looking like a seeming like a natural statement about numbers, much like Goodstein's theorem, a form of self-reference or consistency comes to play. Indeed, many of these true but unprovable statements have a hidden Godelian mechanism to them because of the connection of the structure of the statement to the relative theory that's expressing it. Goodstein's theorem = proving Cons(PA), solution to Diophantine equations = solving Halting problem, etc. and there are other algebraic/topological formulations of independent statements that have this same hidden Godelian mechanism behind them.

All this said, we use the term 'independent' pretty broadly, but understanding how independence arises in the first place, and what being independent really means relative to a theory helps to unravel the logic behind it all. There's more nuance/formalization to it, but I see independent statements like CH and Parallel Postulate in a different category to independent (true but unprovable) statements like Goodstein's Theorem or Diophantine equation solutions.

I don't know if this answered your question completely, but hopefully it helped in some way. I'm no logician myself either, but like you I had this mismatch in my intuition and understanding of the independence phenomenon until trying to understand the mechanism that causes independence in the first place, and the different kinds of independence you see in those different classes of statements.

[u/RlyehDreams → u/shuai_bear]

Ypu can force the continuum to be any cardinal of uncountable cofinality, for example \aleph_{\omega+1} or aleph_{omega_3}, ie aleph_omega is not an upper bound for the continuum. (But it can't be exactly aleph_\omega as that has countable cofinality.)

[u/shuai_bear → u/RlyehDreams]

Thank you - just went down a rabbit hole of CCC, learned something from your comment.

[u/Lehatan → u/shuai_bear]

Thank you, this was helpful. A lot of things for me to digest, but the idea that there are different ways in which a statement may be undecidable seems crucial, and not something I’ve thought about before.

I still struggle to understand the intuition for the ‘non-standard’ models of PA in which ZFC-provable statements about natural numbers are false.

Edit: based on your and others’ answers on this thread, I am coming to the conclusion that PA is too weak to describe the natural numbers

[u/GoldenMuscleGod → u/Lehatan]

A non-standard model of PA basically has all the natural numbers, but it also has more “infinite” numbers that are larger than all of them but still act like other numbers.

Here is what I think is a good way to build intuition: take PA - or any other theory, you can even take the full set of all true sentences in Th(N) if you want (even though this set is not recursively axiomatizable) - and add to it a new constant symbol c and add the infinite list of axioms axiom c=/=0, c=/=1, c=/=2, etc for each natural number - this is an infinite set of new axioms, we do not add the axiom “for all n, c=/=n” which would be inconsistent since we could substitute c for n.

This theory is consistent: any proof is finitely long and can only cite finitely many axioms, so just pick some number c that isn’t barred from being by the axioms used and say it is that, showing no proof can yield an inconsistency. You can think of this like a game where I choose c and you can ask me questions about it and I say “yes” or “no” and you try to figure out what c is, but I am allowed to “cheat” and change my mind about what c is as long as all my previously given answers remain true. It turns out you can never pin me down to a specific value of c if I am clever enough.

So what would a model of this theory look like? Well it has all the natural numbers, and c must be larger than all of them (since you can list them going up and I have to say it’s larger to keep from being pinned down to a smaller set). It’s also going to have a bunch of things like c-16, or c/2, or c^(2), or floor(log c) or “the number of distinct prime factors in c”. All of these except possibly the last will also be larger than every natural number. On the last, I could have a model where c is prime, or where it is a (nonstandard) power of 2, or where c is divisible by every standard prime.

[u/shuai_bear → u/Lehatan]

intuition for the ‘non-standard’ models of PA in which ZFC-provable statements about natural numbers are false.

GoldenMuscleGod has a great detailed comment about how it works - think of c in their comment as a non-standard integer. Nonstandard integers are able to exist in a model that is consistent with PA (one property is that it is larger than any standard natural number), because PA is too lax and doesn't have enough rules/'strength' preventing their existence unlike ZFC.

And when we plug in these nonstandard integers to Goodstein's algorithm, it produces an infinitely long descending chain of ordinals / sequence - some sequences will never terminate with these nonstandard inputs. This cannot happen when epsilon_0 is well-founded (it can't happen in ZFC), but it can happen in a weaker theory like PA.

And for some model theory intuition, think whether the perspective is external or internal relative to the model - outside of PA, say from ZFC we know Goodstein's theorem being false is false. But inside of it, PA is "naive" in a sense because it can't detect anything wrong with Goodstein's theorem being false, agreeing/being consistent with both either the truth of falsehood of it.

 PA is too weak to describe the natural numbers

Yes in the sense that the proof-theoretic ordinal (think of it as the supremum of ordinals that can be proven to be well-founded in a theory) of ZFC is much higher than PA (how much we don't really know), but enough that it can handle a proof that would only require transfinite induction on said ordinal.

However, note that ZFC also cannot capture the full truth of natural numbers. No theory can (a theory that is consistent, and recursively enumerable - otherwise just take the set of all true statements of arithmetic and call that a theory). While ZFC may be stronger than PA, it too is subject to incompleteness and you get a whole other class of problems that are true but unprovable in ZFC.

[u/yoshiK → u/Lehatan]

Löwenheim–Skolem tells us that if a set of sentences has a infinite model, it has models of every infinite cardinality. So that implies that any theory of the natural numbers has non-standard models. However you are probably thinking about the elemental model of PA. So if you have two models of PA a, b, then both contain a zero and a successor function s_a , s_b (this is just PA) and we can find the isomorphism of two subsets where f: 0_a |-> 0_b and s_a ⁿ (0_a) |-> s_b ⁿ (0_b) so that tells us that models of PA are "the natural numbers" and some additional bits.

[u/AxelBoldt → u/shuai_bear]

Does this mean then, if we managed to prove Collatz to be independent of PA, we'd know that there is no counterexample in the standard natural numbers 1,2,3,..., so therefore Collatz would be true in the standard natural numbers? Is it at all possible to meaningfully talk about "truth in the standard natural numbers"?

[u/shuai_bear → u/AxelBoldt]

Does this mean then, if we managed to prove Collatz to be independent of PA, we'd know that there is no counterexample in the standard natural numbers 1,2,3,...,

Not necessarily - it could be false in ZFC. Some hypothetical scenarios where Collatz is false:

- A standard counterexample enters a finite cycle avoiding 1. PA can prove ¬Collatz, no independence

- A standard counterexample never repeats, and PA can prove it never reaches 1. Same thing

- A standard counterexample never repeats, ZFC proves its nontermination, but PA cannot prove ¬Collatz so independence from PA is possible.

The last one is a possibility, because it's not that we're inputting a nonstandard number into Collatz algorithm - it could be a standard number input, yet PA can't prove it doesn't terminate (maybe the ordinal complexity required is too high for PA). Compared to Goodstein's theorem failing, a nonstandard integer is input into Goodstein's algorithm producing an infinitely descending chain of ordinals (which can't happen in ZFC when epsilon_0 is well-founded).

I realize saying "there might be a nonstandard model of numbers where Collatz fails" is a bit misleading because it almost implies there must be a nonstandard number where it fails. This could be the case, like Goodstein's theorem, but it could also be false in ZFC with a standard number and Collatz can fail in PA or a different reason like proof complexity.

The top comment in this MathSE post has some more info about this - logic - If the Collatz conjecture is undecidable, then it is true - Mathematics Stack Exchange

Is it at all possible to meaningfully talk about "truth in the standard natural numbers"?

Yes!

Note there is a distinction between syntactic vs semantic truth. Godel incompleteness says something about syntactic, mechanical provability. The semantic flavor, Tarski's undefinability of truth theorem says that arithmetical truth cannot be defined in arithmetic - more generally, semantic truth predicate of a sufficiently strong formal system cannot be defined within that same system.

The common theme in these limitative theorems is relativity. PA is syntactically incomplete, and some syntactically unprovable truths can be proven true in a larger system like ZFC. Of course, same thing applies to ZFC with syntactic incompleteness.

PA cannot define semantic truth of arithmetic within itself, but a larger meta-theory like ZFC can define a truth predicate for PA sentences by stepping outside its language. Yet again, this relativity is hierarchical - ZFC cannot define its own truth either, forever pushing the horizon of semantic truth to an even higher meta-language.

Regarding a "one true model of arithmetic":
N=({0,1,2,…},0,S,+,×,<) is an absolute, fixed standard model of arithmetic, where its elements are the ordinary natural numbers, with their usual arithmetic operations. There is only one unique model of arithmetic up to isomorphism.

PA has nonstandard models because its first-order axioms do not uniquely determine this structure up to isomorphism. Of course stepping into ZFC, we have a theory that can capture more truth of arithmetic, but again due to incompleteness and Tarski, we have to go beyond ZFC to capture more truth, and this will always be the case. No sufficiently strong system can capture all arithmetical truth, and no sufficiently strong system can even define arithmetic truth within the same system. Both syntactic and semantic truth will always be out of reach, but there is meaning in discussing the hard limitations of math (proof theory, model theory).

[u/AxelBoldt → u/shuai_bear]

Thank you, that is all very helpful and illuminating. Just to make sure that I understand: suppose we were able to prove that Goldbach's conjecture is independent of PA. That would mean that Goldbach's conjecture holds in the standard natural numbers, correct?

[u/shuai_bear → u/AxelBoldt]

Yes! The nuance here is the type of logical statement the conjectures fall under.

(Sorry the formatting will be weird) - Goldbach is a Pi^0_1 statement, and its independence in PA implies its truth.

Collatz is a Pi^0_2 statement, and proving it false involves proving non-termination, which requires showing a possibly unprovable universal claim (a sequence never terminates).

In Goldbach we just need to check once that it fails. In collatz, it’s not enough for one finite computation - we have to show a sequence loops forever or diverges, a much stronger universal claim to prove.

I would look up Pi logical statements for more info on this if you’re interested.

[u/SOTGO]

I would avoid relying too heavily on intuition here. Take the Busy Beaver function, from Wikipedia "the n-state busy beaver game consists of finding the longest-running or highest-scoring Turing machine which has n states and eventually halts." By definition the longest running Turing machine of a given size that halts must run for a finite amount of time (or else it would never halt), so the busy beaver function must be finite for any n. But it has been shown that for large enough values of n (I believe at least for n > 748) the value of the busy beaver function is undecidable, even though we know for a fact that it is some finite value.

[u/GoldenMuscleGod → u/SOTGO]

You have partial understanding but it is incomplete and I think your answer may mislead OP. The value of the busy beaver function is independent of an axiomatizable theory for sufficiently large inputs, where the size depends on the theory. It isn’t undecidable. Undecidable and Independent are not synonyms. It is impossible (in classical math) for any specific proposition to be undecidable - only decision problems can be undecidable. A single proposition can be independent of a theory but there is no such thing as being “independent” in general - it can only be independent of a theory, not of all theories. Independence is a binary relation.

There is a fact about the busy beaver function related to their intuition: there exists exactly one explictly written n for which BB(1000)=n is consistent with, say, ZFC (assuming ZFC is consistent). This is the “true” value of BB(1000). We can consistently add BB(1000)=/=n as an axiom to ZFC, this theory then proves BB(1000)=/=k for any numeral k. In a model of this theory the value of BB(1000) is a nonstandard element, not an alternative standard natural number.

Edit: actually I think to justify that claim I have to assume more than that ZFC is consistent - enough is to assume that an inaccessible cardinal exists.

[u/SOTGO → u/GoldenMuscleGod]

My apologies, I am not an expert in this area. I called it undecidable based on the title of a paper linked from the Wikipedia page, "The Undecidability of BB(748)" (link). Looking back the actual statement on the page is "it is undecidable by a general algorithm whether an arbitrary Turing machine is a busy beaver," which you are correct is different than the claim I made

[u/GoldenMuscleGod → u/SOTGO]

To be fair the terms are sometimes used synonymously even though they shouldn’t be.

To clarify the difference: a decision problem can be thought of as a case where we have a class of questions and we want a “yes” or “no” answer on each of them. It is decidable if there exists an algorithm taking the question as input and outputting the answer. If not it is undecidable. Note that this definition does not mention any theory.

With this definition (in classical math, using the law of the excluded middle) a single question cannot be undecidable: its answer is either “yes” or “no” and so one of the two algorithms “ignore the input and say yes” and “ignore the input and say no” must give the correct answer. Of course this doesn’t help find the answer, which is why the classical notion of decidability can be counterintuitive (this is one area where constructive theories better capture intuition).

A sentence is “independent” of a theory if that theory neither proves it nor its negation. This depends on the theory. No sentence is independent of every theory: consider the theory where we take that sentence as an axiom. Of course this does not help us to determine whether the sentence is true with the meaning we intend for it. This is similar to the decidability issue for single propositions.

The ideas are distinct but related: suppose we have a binary relation where the problem of whether it holds is undecidable. For example, “does BB(n)=m?” Where n and m are variables that must be set for us to have a specific question. Then that means for any sound axiomatizable theory there must be some specific case of it that is independent of the theory (such as “does BB(1000)=[some explicitly written enormous number]?)

However which of these statements is independent of the theory will depend on the theory, and there is no statement that is independent from all sound and axiomatizable theories.

[u/ZookeepergameWest862 → u/GoldenMuscleGod]

there exists exactly one explictly written n for which BB(1000)=n is consistent with, say, ZFC (assuming ZFC is consistent)

While this is true, it's a bit funny, because that one explicitly written n is BB(1000), of the metatheory. So there is one explicitly written n but we cannot explicitly write (or rather can never confirm) because it was conjured out of excluded middle.

[u/GoldenMuscleGod → u/ZookeepergameWest862]

Yes I’m giving a classical account. I think constructive and intuitionistic theories can give useful alternative ways of looking at it, these theories often deal with the issue at a much earlier step: they are either agnostic about or affirmatively reject the idea that the busy beaver function even exists as a function defined on all natural numbers, and as for specific values like BB(1000) they wouldn’t normally actively deny it exists but they will say, essentially “I’ll believe it exists when I see it.”

Whether they ever will “see it” or not depends how strong the constructive theory is.

[u/GoldenMuscleGod → u/ZookeepergameWest862]

Oh and thank you for this reply because thinking about it a little more made me realize I cannot justify that conclusion simply by assuming ZFC is consistent, if I am restricting myself to ZFC: I cannot eliminate the case where ZFC is consistent but proves BB(1000)=/=k for all standard k. Enough is to assume that an inaccessible cardinal exists.

[u/ZookeepergameWest862 → u/GoldenMuscleGod]

Right. It is generally true that there is at most one (you don't even need consistency of ZFC for this), but Cons(ZFC+BB(1000)=n) (this notation is a bit quacky since n is not necessarily a number writable in the metametatheory, but only exists within the meta ZFC) isn't provable from ZFC+Cons(ZFC) because this would mean that ZFC+BB(1000)=n and ZFC are equiconsistent in ZFC, but this can't be the case because ZFC+BB(1000)=n proves ZFC is consistent.

If ZFC is inconsistent (in the meta ZFC) then ZFC+BB(1000)=n can prove anything, including the (internal) consistency of ZFC. If it is consistent, then the Turing machine M checking the consistency of ZFC doesn't halt, the version of M inside ZFC+BB(1000)=n cannot halt since it would take a nonstandard number of steps which is larger than n, contrary to BB(1000)=n and so M does not halt and ZFC is consistent.

I was confused for a while before writing down the proof above, because this it seems that ZFC+BB(1000)=n can prove the consistency of even large cardinals. Like if T is a theory stronger than ZFC, then ZFC+BB(1000)=n (inside T) seems to prove the consistency of T (assuming that T is checkable with a 1000 states Turing machine, which would include pretty much all theories that we care about), violating Gödel if your argument works. It turns out that the possibility that T is inconsistent inside T is an issue. An interesting thing is that if n is standard with respect to the metametatheory, then ZFC+BB(1000)=n inside T does prove the consistency of T. So it seems that there is a philosophical issue with asserting the definiteness of BB(1000) by appealing to standard natural, as being standard itself is not definite but only with respect to a metatheory, and the precise value of BB(1000) can never be found but only be turtled all the way up the metatheories.

[u/NewtonsThirdEvilEx → u/SOTGO]

I don't think that helps me. You can physically evolve an n-state Turing machine in time with it's transition function and see if it halts or not after an arbitrary amount of steps. But some don't halt. For small ones, we're able to associate certain Turing machines with certain problems and prove that they don't halt in some cases and sometimes we're able to enumerate them. Not in all though.

But for the Collatz case if we find a non 4-2-1 loop, that is a experimentally testable counterexample.

[u/djao → u/NewtonsThirdEvilEx]

There could conceivably exist Collatz counterexamples that never devolve into a loop, but just continue infinitely without ever looping.

[u/NewtonsThirdEvilEx → u/djao]

Yes, but that's beside my point. Nothing forbidding a nontrivial loop assuming the proof is undecidable. Still a counterexample.

[u/djao → u/NewtonsThirdEvilEx]

Um, actually, yes, if you assume the problem is undecidable, there is something that forbids a nontrivial loop; namely, the existence of a nontrivial loop contradicts the supposed undecidability of the problem.

Suppose there exists a nontrivial loop starting from some value x not equal to 1, 2, or 4. Then, start from x and compute enough terms in the sequence to reach x again. Congratulations! You have decided the Collatz conjecture, contradicting the assumed undecidability of the conjecture.

[u/cuervamellori → u/djao]

Only a nontrivial loop in the standard natural numbers would contradict undecideability, correct? A nontrivial loop in nonstandard numbers would not.

It's possible that collatz is undecideable and nontrivial loops can't exist, but that's stronger statement than saying collatz is undecideable.

[u/djao → u/cuervamellori]

I interpret Collatz to state that no counterexample exists in the standard natural numbers.

[u/cuervamellori → u/djao]

"X is true in this particular model of ZFC" will always be either true or false; it can't be a statement in ZFC and can't be said to independent of ZFC, right?

[u/Kaomet → u/cuervamellori]

Hu ?

You can build an inner model of ZFC in any model of ZFC (forcing). Then ZFC can prove X is true in this inner model / false in that inner model. And this is precisely how CH was proven independant of ZFC (Gödel built a model where CH is true, Cohen built a model in which it is false).

ZFC is the axiomatic theory, by definition true in all models. Independant of ZFC means the axiom does not give enough information to decide a statemeent. As in geometry : you need Euclid fith postulate to rule out elliptic and hyperbolic geometry, so it is independant of the previous postulates.

[u/djao → u/cuervamellori]

Ok, maybe this is why non-logician mathematicians get tired of logicians. When someone asserts the existence of a nontrivial Collatz loop, I am imagining something very concrete: here is a natural number x, here is its decimal expansion, here are all the subsequent terms in its Collatz sequence, each of which one can verify, and here is x repeating itself in this sequence after n terms. If you are imagining some different scenario, then we are not thinking about the same thing. If your language is insufficient to express what I am thinking, then your language is inadequate.

[u/cuervamellori → u/djao]

I'd love to take credit for creating ZF(C), but I'm afraid I can't 😀 it's fine to say "what I care about is if CC has a counterexample in the standard numbers". But if you're saying that, then there's no useful way to use words like "undecideable" in relation to ZF(C), those concepts no longer apply.

Undecideable, independent, etc., all relate to a set of axioms. There is no set of first order axioms that define exactly the standard numbers.

The question of whether a fact (like Goodstein's theorem) is independent of a set of first order axioms or not I think usually should not be that interesting to people who care about whether it's true in a particular model.

[u/NewtonsThirdEvilEx → u/djao]

Okay, then that clears about everything.

[u/BiasedEstimators → u/NewtonsThirdEvilEx]

The set <n, k> is countable infinite. Say n is the number of k is the collatz step.

Enumerate <n, k>. Go through the enumeration calculating collatz(n, k) each time. Terminate when you find a nontrivial loop. This algorithm is guaranteed to terminate in finite time given a nontrivial loop.

[u/GoldenMuscleGod → u/NewtonsThirdEvilEx]

The claim that there is no nontrivial loop is a pi_1 claim (as I described that term in another comment I made replying to you), and so is true if it is independent, however it can be independent of PA, or ZFC (in the sense that pi_1 claims in general can be independent - of course we do not know whether this claim is independent). The claim there is no divergent sequence is pi_2 claim so could be true or false if it is independent (as far as we know).

By the way I think the comment above could be potentially misleading so I will link here my response to it clarifying what I think it misses.

[u/NewtonsThirdEvilEx → u/GoldenMuscleGod]

I do like this more formal argument a lot better. I will read a bit more into it, but thank you!

[u/OmnipotentEntity → u/NewtonsThirdEvilEx]

To add to /u/djao on how Collatz could be independent of ZFC. Let's say we have an orbit that may be infinite, or may just be very, very long, so long that we have no way of concretely simulating it in the universe. However, while analyzing it, we somehow find that this particular orbit belongs to an infinite family of related orbits, such that all such orbits terminate if and only if the continuum hypothesis is true.

Any particular orbit may converge, and we may even be able to demonstrate this for particular orbits, but if we prove all such orbits diverge then we have a proof of the continuum hypothesis.

[u/NewtonsThirdEvilEx → u/OmnipotentEntity]

why are you making this “in our universe”. as a trained physicist, that’s making it far more worse for me lol.

[u/OmnipotentEntity → u/NewtonsThirdEvilEx]

well, you had mentioned "physically evolving" Turing machines, which is why I mentioned that in particular.

[u/lurgi → u/SOTGO]

I can't find a reference to 748, but this is relevant.

[u/SourKangaroo95 → u/lurgi]

In his latest blog post he says the number has been brought down to 335

[u/Foreign_Implement897 → u/SOTGO]

Nice!

[u/JustAGuyFromGermany]

The easiest way to think about this topic is to take what is now called the "multiverse view" to set theory: The axioms of set theory are similar to the axioms of groups or topological spaces or something similar - they can have many different instantiations (also called models in set theory), all of which satisfy the axioms (and all provable consequences of those axioms) but they may also differ in statements which are not provable from the axioms.

A statement like the Collatz conjecture being undecidable simply means that there are at least two models: One in which the Collatz conjecture is true, i.e. all natural numbers in that model satisfy the conjecture, and also one in which it is false, i.e. at least one natural number of that other model does not satisfy the conjecture. Just like "xy=yx is not decidable from the group axioms" simply means that there is at least one group which is and one group which isn't commutative.

It is important to note that there is no such thing as "the" natural numbers across all models. There is of course only one such thing in each model, but there should be no expectation that the natural numbers of one model behave the same as the natural numbers of some other model. Just like you wouldn't expect say the centre of one group to be in any way similar to the centre of a different group.

That's basically the whole point of Gödel's incompleteness theorem: Models of set theory can have different natural numbers that can have different arithmetic properties, including what kind of equations have solutions and which don't. And "X is a proof of Y" is just a very, very, very complicated arithmetic equation that may or may not have solutions depending on which model you look at.

To be more precise. You state:

it seems that any counterexample [to the Collatz conjecture] would be constructive (it’s just a natural number!), and hence, if CC is undecidable, such a counterexample cannot exist.

That's not true. If the Collatz conjecture is undecidable, then the natural numbers (inside some model where CC is false) which are counterexamples are exactly not constructive, i.e. they cannot be written as 1+1+1+...+1 with any absolute number of ones. Your own argument shows that: The same string of symbols would define a natural number in any model, including those in which CC is true. And the whole calculation that CC is false for this number would also consist of an absolute number of symbols, which would therefore also be applicable to any other model, including those in which CC is true. Therefore, there cannot be such a finite string.

What we have proven is: The models of set theory in which CC is false (if there are such models) have very weird models of N which do not look at all like the natural numbers of our meta-theory; they are non-standard models of Peano arithmetic and the counterexamples are non-standard natural numbers. The thing is: The model does not know that! From inside the model the counterexample looks like a completely ordinary natural number. It satisfies all properties that ZFC can prove about natural numbers after all. It just doesn't satisfy some of the statements that ZFC cannot prove (like CC in our assumption).

[u/Lehatan → u/JustAGuyFromGermany]

This is a pretty mind blowing answer. What would a weird model of N look like? Can we “write down” an example of a weird model of N? Or is this fundamentally out of grasp?

[u/__mintIceCream → u/Lehatan]

The example I was shown is a result of the compactness theorem, which you can look up as well, it is very cool and awesome.

The idea is that alongside the (first order) peano axioms, we add in an axiom that declares the existence of an infinite element c (we technically need to add infinite axioms saying that c>0, c>1, c>2, etc. for all the usual naturals, and this is where compactness comes in), and then you can examine the consequences because c satisfies all the peano axioms and is thus also a natural number so everything about natural numbers apply. A couple of them:

• c has a successor, and since its not zero c also has a predecessor, so there is a copy of the integers Z around c (the model now looks like N followed by Z)
• c+c cannot be reached via successors of c, since c is infinite, similarly n*c for any n (the model now looks like N followed by N copies of Z)
• c is either even or odd, so we can either divide either c or c+1 by 2, meaning we can fit c/2, c/4, c/8 etc before c and all of those are also unreachable from each other (the model now looks like N followed by Z copies of Z)
• you can add all the inbetween points too by taking averages and whatnot, and we now have N followed by the rational numbers Q; but each point of Q is replaced by a copy of Z.
• theres probably more this is all we got to

I think this is a good example of the multiverse view, its very obviously not the usual model of natural numbers, and just using the peano axioms you cannot tell the difference between this and the usual one. But its (probably, i havent tried) easy ("easy") enough to construct it in zfc

edit to add: this is the same one as the one described by u/JustAGuyFromGermany choose your favorite exposition

[u/Waste-Ship2563 → u/__mintIceCream]

This is strange, I know e.g. in type theory naturals are defined inductively via two constructors, 0: N and succ: N -> N, your example sounds like including a third constructor c: N. But then it seems like this isn't a model of the natural numbers.

Edit: I think I get the idea. In standard models of ZFC, the proposition "∃ c, (0 < c) ⋀ (1 < c) ⋀ ... " is false, but there are nonstandard models in which it's true.

[u/JustAGuyFromGermany → u/Waste-Ship2563]

In type theory, N is defined as the "universal" or "smallest" type with these two properties, i.e. it is explicitly defined as the standard model in a second-order fashion. The construction above is only about the first order Peano axioms.

[u/__mintIceCream → u/Waste-Ship2563]

hmm im not well versed on type theory, but i dont see why not? if we arent stingy about what elements are in the set N (which is the point here), defining succ: N->N for c, as well as all the other elements i've described doesnt seem impossible.

[u/Waste-Ship2563 → u/__mintIceCream]

That makes sense, in other words if you aren't stingy you include elements that can't be reached by finitely many applications of succ.

[u/Lehatan → u/__mintIceCream]

Seeing this example I come to the conclusion that Peano arithmetic is too stupid if it cannot distinguish between these two things. Surely then we should use more axioms when making statements about N

[u/__mintIceCream → u/Lehatan]

It's kind of the opposite, in a sense; the axioms we are looking for to be able to do arithmetic are too powerful. The point of Godel's (first?) incompleteness theorem is that (dependent on some reasonable conditions) even if we add axioms to disallow any specific models we don't like, if it can still do arithmetic as we know it, there will always be some non-standard model in addition to The One True Model.

[u/JustAGuyFromGermany → u/Lehatan]

Well, on the other hand they are powerful enough to do arithmetic ;-)

And indeed, it is a bit of "choose one" here. That's the point of Gödel's incompleteness theorem. As soon as your axioms are powerful enough to do a fair bit of arithmetic (you don't need all of Peano) you already get incompleteness. There are other axioms that are not affected by incompleteness phenomenon and do indeed have unique models, but you can't do much arithmetic with them.

[u/Lehatan → u/JustAGuyFromGermany]

Oh wow! This along side the answer from [u/__mintIceCream](u/__mintIceCream) put a lot of pieces into order in my head.

[u/GoldenMuscleGod → u/Lehatan]

Here is what might also be a helpful piece: there is a theory called “primitive recursive arithmetic.” It is expressive enough to be able to make pretty much any concrete claim like “this algorithm will be in this state after this many steps” where each “this” is something explicitly named. And it is powerful enough to resolve any concrete question you might ask of it in its language.

However it is not expressive enough to say things like “this computation eventually halts” - it can say it does/doesn’t halt in n steps, and it can prove it one way or the other for any concretely given n. But what if n is a variable? Well then obviously if it halts in n steps depends on what n is, so in general we should not be surprised we cannot prove or disprove it.

Now sometimes you might be able to prove “this computation doesn’t halt in n steps” where n is a variable. We understand this must mean it never halts (since we assumed nothing about n’s value) but we cannot treat that statement as saying that: if we assume the computation doesn’t halt in n steps in order to do a direct proof then we have only assumed something about a particular unspecified n, not for all n.

Similarly we cannot say “this computation eventually halts” we can only say things like “this computation halts in 50,000 steps” or whatever for any other number. But of course “this computation halts in 50,000 steps” does not mean the same thing as “this computation eventually halts” - the first claim is stronger and more explicit.

The idea of theories like Peano arithmetic is we want to expand the language to be more expressive so we can say certain things are true of all numbers or of some number, or of all computations or of some computations, without having to name them so concretely. So we add quantifiers. This is very useful, but it is exactly this step in allowing expanded meaning that forces us to have statements we cannot work with as concretely - because they are less concrete.

We want \forall n Pn to be true exactly when Pk is true for every natural number k, this can be taken as a part of a definition of what \forall means. But can we have that \forall n Pn is provable exactly when Pk is provable for every natural number k? Reflecting on this might make you realize this is a lot to ask of a theory, and in fact we can’t make it work for any nice theory. So it is exactly the inclusion of this type of meaning that makes the statements less “concrete” in at least some ways.

[u/Lehatan → u/GoldenMuscleGod]

Thank you, this was very helpful too. This seems to pin down exactly where the loss of ‘concreteness’ happens in the formalism.

[u/GoldenMuscleGod → u/Lehatan]

If you want to explore the logic of this idea of “concreteness” you might want to consider looking into intuitionistic logic and constructive theories. It can take a while to get used to not accidentally using the law of the excluded middle when you reason but it’s actually not so weird as you might think. If you look up Gödel’s Dialectica interpretation of Heyting Arithmetic (the intuitionistic analog of Peano Arithmetic) it might give a lot of insight, although some practice with intuitionistic propositional logic might be necessary to be able to follow it.

[u/Opposite-Friend7275 → u/Lehatan]

Nobody can distinguish between those things. It’s like trying to decide if the universe we live in is infinite, or, a larger version of infinite. With finite means that cannot be decided.

[u/JustAGuyFromGermany → u/Lehatan]

Well "fundamentally" is maybe a bit much, but don't expect too much. We can describe the ordering for example. Non-standard N are well-ordered from their own point of view, of course, but don't look like that from the outside. For one, the Löwenheim-Skolem theorems say that there are non-standard models of any infinite cardinality, in particular there can be models of N that are uncountable from the point of view of the meta-theory.

But let's focus on the countable ones. From the point of view of the meta-theory the ordering of a non-standard N is still a total order, but it has the standard N in front, followed by an infinite number of copies of standard Z which are themselves ordered like standard Q. The Z pieces are simply a consequence of every number having a successor with nothing in between (i.e. \forall n,k: \not (n<k<n+1) is provable and therefore true in all models of Peano arithmetic, even in non-standard models).

Since addition is tightly connected to the order, this also tells you a little bit (but not everything) about how addition looks like in such a non-standard model. However, this result does not tell you much about multiplication or exponentiation. In fact there is Tennenbaum's theorem which shows that non-standard models must always have either addition or multiplication or both as non-computable functions, so depending on how lax you are when you say "writing down", that may be out of reach.

On the other hand, if you're comfortable with the notion of ultrafilters, then the ultraproduct construction can give you a lot of useful (uncountable) models that are reasonably explicit with the single exception of the ultrafilter that you need for the construction.

(See https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic for more details and sources)

[u/shuai_bear → u/Lehatan]

See my other response on Goodstein's theorem which is true but unprovable in Peano Arithmetic and thus has non-standard models both agreeing its truth or falsehood (in PA), but for Goodstein's theorem specifically, the rough intuition is that the tail ends of long sequences of natural numbers don't 'behave' in a way that aligns with arithmetic as we know it (by this I mean with the standard model), but otherwise it is consistent that there is a non-standard model of arithmetic where you have PA's axioms + negation of Goodstein's theorem. So there can be a counter example to this true but unprovable (in PA) statement, just the example is not a natural number from the standard model which might be the case for Collatz.

I have to echo OP's point in that a philosophical resolution to this is the multiverse set-theoretic view of math. We call it "standard model" because the model that aligns with Goodstein's truth also aligns with ZFC (ZFC can prove Goodstein true, even if PA can't but PA can express it). But Collatz might be even stronger or more complex where even ZFC fails to capture its truth, and perhaps there exists is a non-standard model of numbers (relative to ZFC) where Collatz' falsehood is consistent.

However we don't have much insight into larger models than ZFC because ZFC is truly really big, we don't even know the proof-theoretic ordinal that bounds ZFC (PA is epsilon_0), though some large cardinal axioms can enlarge ZFC, this is different from an entirely new foundation that captures ZFC and beyond.

[u/Kaomet → u/Lehatan]

N is the standard model of arithmetic. A model, not a theory of arithmetic. What we can have is a theory of Arithmetic like PA, and non-standard model. But in the case of PA, non-standard models are uncomputable, and their construction is done using the axiom of choice.

Arithmetic without comparison nor reccurence principle has an "obvious" non standard model : function over natural numbers (they can be added, multiplied, and contains constant functions as standard model). But as soon as we add comparison and reccurence, we need the axiom of choice to prove the existence of an ordering < compatible with all the axioms...

[u/Lost_Geometer → u/JustAGuyFromGermany]

Aren't there only nonstandard models for first order theories of the naturals? I wouldn't reject a (dis)proof of CC for using second order induction.

(I'm also not a logician, so maybe this is gravely off-base?)

[u/JustAGuyFromGermany → u/Lost_Geometer]

Yes, I was simplifying a lot here, conflating Peano arithmetic with all of ZFC or whatever else we choose as our axiom system of choice (pun intended).

Yes, there is only a single model of second order arithmetic, the standard N. However: The concept of "second order" depends on the notion of a subset of the model and is therefore dependent on the model of set theory one looks at. Many models of set theory (also called "standard models") just consists of ordinary sets from the meta theory and therefore have the same natural numbers as the meta theory or something very closely related. There are however other models of set theory whose "sets" look nothing like the sets from meta theory and whose natural numbers therefore have very little in common with the standard N in terms of second order arithmetic.

Thus, even going to second order arithmetic won't save you here. The problem just shifts.

[u/GoldenMuscleGod → u/Lost_Geometer]

Usually when we talk about theories we mean first order theories with decidable sets of axioms. Bringing up higher order theories is a little like talking about spherical triangles as counterexamples to the claim “the angles of a triangle add up to 180 degrees” - it’s true this claim doesn’t apply to non-Euclidean triangles but those aren’t the types of triangles we are talking about.

Also saying a second order theory can give us a unique (up to isomorphism) model of the natural numbers is highly misleading if it is not carefully explained what a second order theory is.

Second order theories are not suitable for use as “working” theories because there can be no complete, sound, and decidable deductive system for a second order theory. This is a direct consequence of the incompleteness theorems which are usually framed as talking about first order theories but also apply to higher order theories in this way. That is, there is no general way to produce a “proof” that one sentence in a higher order theory follows from another, and in a very real sense the idea of “proof” in the usual sense is not applicable to higher order theories at all.

That isn’t to say that they are useless - we can learn things by studying higher order theories, and there are abstract (not directly usable) notions of “proof” that can be applied to them, although we cannot write these “proofs” down. But it would be a mistake to think that fundamental barriers arising from incompleteness can be surpassed by just using a “better” type of theory - all we are doing is shifting the issue around so it arises in different ways.

[u/Global-Trust-151 → u/GoldenMuscleGod]

This is wrong. Dependent type theory is a higher-order formal system (or stronger, depending on what you mean by higher-order) that is extremely usable, in the sense that you can literally prove things with it on a computer. Every time you write a .lean file you are writing down a proof in a higher order formal system. I don't know why you would put quotation marks around the word "proof."

I think what you mean to say is that there is no sound, complete, effective proof calculus for full second-order semantic consequence. Higher-order theories can certainly have sound, effective proof systems, and second-order logic even admits a completeness theorem under Henkin semantics.

Full second-order arithmetic can categorically characterize the natural numbers, but that does not mean we can effectively prove every statement true about them. The tradeoff is that categoricity comes at the expense of having an effective proof calculus complete with respect to the intended semantics. This is very different from saying that higher-order theories cannot be used to produce formal proofs.

Intuitively, giving yourself enough expressiveness to completely specify the natural numbers means you necessarily have also given yourself the ability to make true claims which you can't prove.

[u/GoldenMuscleGod → u/Global-Trust-151]

I specified a deductive system that is sound, effective and complete, in the way that Gödel’s completeness theorem means complete. Completeness is about semantics. So I do not see how your “I think you mean” is meant to suggest a disagreement

I think your comment is misleading, like you say it depends what you mean by“second order.” I would normally say someone asking if dependent type theory is first order or second order is trying to apply a distinction used in one realm of logic where we have clearly understood semantics of a restricted type to another where we are much looser and less conventionalized with the semantics we may consider.

Now we could get into a discussion about that terminology in general but the key issue is the context in which I commented. Somebody was specifically talking about having a second order theory being categorical in the classical model-theoretic sense.

This is like how second-order Peano Arithmetic is categorical with standard semantics.

Usually if someone says “second order theory” they mean a theory where we have taken a classical first order theory and added quantification over propositions with the standard classical semantics for those types of theories.

Type theories are not ordinarily interpreted with semantics like these, and the semantics they do have do not ordinarily lead to categoricity in the sense we mean or even any particularly analogous sense, so it is not relevant and they cannot be considered “second order” in the particular sense we care about in context. The usual semantics they might be given are more Henkin-like, and a second order theory with Henkin semantics is essentially a typed first order theory. It’s basically a way of reducing a higher order theory back into a first order one.

Now there is no general definition of what we mean when we say “second order” which relates to my point that it is very problematic to object to claims about theories generally by saying “what about second order theories?” The same could be done when making claims about whatever generalized definition of triangle we try to adopt: we have no general definition for anything that might be called a “triangle” in any possible context either.

So basically talking about theories as though they can all be classified into “first order” and “higher order” generally is already misleading, we have specific carefully defined things we mean by things like “first order T” and “second order T” for particular classical theories T and when we talk about anything else we can only use these terms in a loose “viby” way.

But the bottom line is that no matter how we do it we are not going to be getting an effective method for determining the truth of all arithmetic sentences, which is the thing I think people often mistakenly understand when bringing the issue up in places like this subreddit.

[u/lisper → u/JustAGuyFromGermany]

What you say is true in general, but Collatz is a special case because any counterexample must be transformable to an "ordinary" natural by a finite number of ordinary mathematical operations, and so any counterexample must itself be ordinary.

(There is of course the possibility of an "extended" Collatz conjecture that admits an infinite series of transformations, i.e. a series that corresponds to a transfinite ordinal. AFAIK this has never been seriously contemplated. It makes me a little woozy just thinking about it.)

[u/JustAGuyFromGermany → u/lisper]

There are arithmetical statements that truly cannot be undecidable. I don't know if CC is among them. However, one has to be reeeaaally careful with the word "finite" in these contexts, because we're dealing with non-standard natural numbers. From the point of view of the counterexample-model those non-standard numbers are just ordinary natural numbers after all, in particular a "finite number of steps" can be a non-standard number of steps. Any "finite" encoding of any "finite" structure that one may be tempted to look at can indeed be an encoding using a non-standard number.

For example: Gödel's incompleteness theorems shows that the consistency of ZFC is undecidable and therefore there exists a model of ZFC that thinks that ZFC is inconsistent, i.e. that a proof of 0=1 exists within that model. That proof is a "finite" number of symbols, of course. But it just so happens to be a non-standard number of symbols so that there is no hope of extracting that "proof" from such a model and writing it down explicitly.

It is critically important to always carefully distinguish between what our models think about arithmetical or set-theoretical statements and our meta-theory proves about such statements, between "our" natural numbers and the natural numbers that our models have etc.

[u/lisper → u/JustAGuyFromGermany]

That's a fair point. It comes down to the fact that the Collatz conjecture is usually stated informally as "...you will always eventually reach 1" so the truth of the conjecture turns on the meaning of the English word "eventually". My reading of that word is that it requires the number of steps to be an "ordinary" natural.

[u/wasabi991011 → u/JustAGuyFromGermany]

If the Collatz conjecture is undecidable, then the natural numbers (inside some model where CC is false) which are counterexamples are exactly not constructive, i.e. they cannot be written as 1+1+1+...+1 with any absolute number of ones.

How is this possible? Are the natural numbers not defined by PA, for which induction implies all natural numbers are the successor of another natural number? Am I misunderstanding induction, or the natural numbers, or something else?

[u/JustAGuyFromGermany → u/wasabi991011]

Yes, they are the successor of some other number, which is the successor of some other number, which is the successor of some other number, which ....

Non-standard natural numbers have infinitely many predecessors. But that infinity is only "visible" from the outside. From inside the model the number n has exactly n predecessors just as always. It just so happens to be that n isn't a standard natural number. But the model doesn't know about this.

Think about it in a different way: There is no finite way to construct N or any other infinite set just from finite sets and finite set operations. You can define every finite natural number individually as usual, but that takes finitely many steps and more the bigger the number you construct. You cannot construct all of them with one go. That's why we need the axiom of infinity in ZFC (or any other system) in the first place. That axiom simply states that the construction isn't necessary and we assume that N already exists in one single step. But how much have we actually gotten in that single step? Well, all of it. How much is all of it? Well, it's all. There is by definition no finite way to list it all, you simply get handed a set and a promise that this set really is all natural numbers and nothing else. And from that point on you simply interpret "natural number" and "element of that set" as meaning the same thing.

And as long as set theory is consistent, there is no finite way for you to find any contradiction in that. You might say "aren't the infinitely many predecessors a contradiction"? Well yes, but only if you can prove "there are infinitely many predecessors". You can certainly prove "there are 2 predecessors of n" or "there are 500 predecessors of n" from inside the model, but you cannot prove that there are infinitely many, because you'd run in a version of the same problem of needing a completed infinity to get from finite to infinite. (I'm hand-waving a lot here)

[u/GoldenMuscleGod → u/wasabi991011]

The natural numbers are not defined by PA. To talk about PA at all we must think there are numerals in its language, expressions of the form SS…S0 where only the symbol S appears until a final 0 (here S is a symbol intended to mean the successor function).

The induction axioms only apply to properties that can be expressed by the language of PA, and “is named by a numeral” is not such a property. But we (standardly) would want define the natural numbers to be exactly those things we can name with a numeral. However we have no induction axioms to enforce this rule.

[u/Opposite-Friend7275 → u/wasabi991011]

There is no unambiguous definition of the natural numbers, the set of natural numbers depends on the ZFC model.

[u/loewenheim → u/wasabi991011]

PA does indeed prove that every number is the successor of another number, but that doesn't mean that every number is a finite sequence of successors away from 0. The latter is a property that PA can't even express. But second-order arithmetic can express it and prove it holds for every number via induction, so second-order arithmetic really does nail down the natural numbers unambiguously.

[u/GoldenMuscleGod → u/loewenheim]

Well, sort of. We cannot in general determine whether a particular sentence is entailed by our second order theory, not even on a semidecidable basis, and to even define the semantics of second-order theories we must specify that the “sets” we think exist are “all of them.” But what do we mean by this? If we have formalized our second order theory using ZFC (a first order theory) as a metatheory we cannot think (from the perspective of a meta-metatheory) that the ZFC axioms have really nailed down what “all the sets” means, so we haven’t really resolved the issue so much as hidden it elsewhere in the formalism, and done so with a theory that we cannot even actually produce tangible proofs in.

Now it is true that the second-order theory is categorical in the way you say, but I tend to think it is very misleading to say that without highlighting these issues.

[u/moschles → u/JustAGuyFromGermany]

You were overly wordy in the last part. Suppose Collatz is false. Then there exists a large z that is the counter-example integer. Nothing about Collatz forces z to be constructive. (It gets worse. Mathematics could prove that there exist an infinite number of countering z's, even while nobody can construct merely one of them.)

[u/invertflow]

I believe it has been proven that some generalizations of Collatz (some related but slightly different rules) are undecidable. However, this was done by proving that this generalized conjecture is equivalent to whether ZFC is consistent, i.e. you cleverly encode the rules of ZFC into this generalization so that certain things only happen if ZFC is inconsistent. So, if you work with a slightly bigger set of axioms, namely ZFC plus "ZFC is consistent", then you have actually just proven that particular generalized Collatz. But then, you could come up with something else that encodes that "ZFC plus 'ZFC is consistent'" is consistent, and to prove that conjecture, well, you'd need to assume that "ZFC plus 'ZFC is consistent'" is consistent. And so on.

[u/TheBB]

It's true that there are certain statements that, if they were false, would obviously be provable to be false with an equally obviously computable counterexample. Proof of undecidability can then be interpreted as a proof of the statement (but in the formal system that the proof of undecidability takes place in).

The Riemann hypothesis is such an example. Not in its classical form, but it is equivalent to a statement about integers that has this property.

I'm not sure the same goes for Collatz since a counterexample might grow without bound, and that could be unprovable (I guess).

[u/ventricule → u/TheBB]

This is the reply to the question OP is asking I think. The confusing thing is this: if RH is undecidable, then it is true. The proof is that if it were false, there would be a counterexample, and checking that there is a counterexample is a finite computation (via for example the Lagarias equivalence).

But how could then one take the negation of RH and add it as an axiom while maintaining consistency? The point is that then we're saying that there is a non-standard counterexample (but our theory is too weak to see that it's non-standard).

Note that CC is much less concrete than RH, since there is no way to check in finite time that a given integer is a Collatz counterexample (and indeed the undecidable variants of Collatz build on this by encoding the halting problem into such a computation).

This kind of behavior is encoded in the arithmetic hierarchy.

[u/cuervamellori → u/ventricule]

Is this a fair interpretation: when I say "all the nontrivial zeros lie on the critical line", what I really mean is "all the, you know, standard nontrivial zeros, using the smallest model of zfc, the one we all know and love, all those zeros, lie on the critical line", but there's no way to make that statement in the language of zfc.

Whenever I say RH, I mean that second one in my head, which is why it's so hard to deal with sentences like "RH might be undecideable in zfc", because that's talking about the first one.

I assume it's correct say "RH is definitely either true or false in the standard (smallest) model of zfc"? And presumably there could be some set of axioms that we could add to zfc that would be strong enough to constrain all the allowable models to those in which RH is true (one such axiom of course would be "RH is true") or false, but we don't have any pleasing such set of axioms.

(Obviously all this in a world where RH actually is independent of ZFC which we don't know)

[u/Sproxify → u/cuervamellori]

there aren't any additional "exotic" zeroes of the riemann zeta function given by allowing more extravagant set theory stuff. it's a sufficiently concrete object for that not to be an issue.

[u/cuervamellori → u/Sproxify]

Is that equivalent to asserting that RH is not independent of ZFC?

[u/Sproxify → u/cuervamellori]

no, it still could be independent. you could think of it as being like zfc "knows" all the zeroes of zeta, but might not be able to prove a universal statement about all of them at once.

[u/cuervamellori → u/Sproxify]

My understanding is surface level but if it's independent, shouldn't there be a model where it's false?

Or is it more that RH can't actually be expressed in first order logic, and saying it's independent of ZFC isn't actually well formed?

[u/Sproxify → u/cuervamellori]

my understanding of all the model theory stuff is also entirely surface level but I'm certain you're right that if it's independent then there's a model where it's false and a model where it's true.

assuming for a second that "our" Riemann hypothesis is true but independent ZFC, then I wouldn't think of that as a model where our zeta function has secret addition. I don't know how I would think about it because I'm not knowledgeable enough in this domain to have a strong intuition for what it means in this case. I suppose that is in line with how you phrased it originally then, but I still feel it must be different than the sense in which ZFC has extra sets that you can't construct in ZF for example.

but what I meant more so when I said you can't find additional zeroes, and I realize now I can't make it precise, is that in my intuition you can't add stronger axioms to the theory that would allow you to describe more zeroes of zeta that even plausibly could be there in "our" sense. Because ZFC already proves there's a computable procedure for finding all the zeroes (up to a neighborhood), and there's also computable processes described by ZFC which half iff Riemann is false.

So the model that believes the conjecture is false probably must be understood as something like the countable model of ZFC where the proven statement of uncountability somehow means something different internally in that model.

[u/cuervamellori → u/Sproxify]

Well, luckily for us, it seems there are proofs that RH is decidable in ZFC, so we don't have to worry :)

[u/Sproxify → u/cuervamellori]

well, no, it could still be independent. we can describe a turing machine that would half iff RH is false, and prove that in ZFC, but if the conjecture is corect, so that it never halts, then there may not be a proof of that in ZFC. but if the conjecture it wrong, and it does halt, then that amounts to a finite computation which necessarily corresponds to a proof in ZFC.

so there are 3 options:

(1) Riemann hypothesis is true, and provable in ZFC

(2) Riemann hypothesis is true, but ZFC is not strong enough to prove it

(3) Riemann hypothesis is false, and then ZFC necessarily proves that it's false

scenarios 1 and 2 are both plausible imo, and in scenario 2 I think we as humans are likely incapable of proving Riemann, as I don't think it's likely that ZFC is just too weak for some kind of proof strategy of riemann that humans could muster.

[u/Lehatan → u/TheBB]

> Proof of undecidability can then be interpreted as a proof of the statement (but in the formal system that the proof of undecidability takes place in).

This is exactly what I’d like to understand. Is this a statement one can make formal?

I see your point that the Collatz conjecture may not be the best example due to unbounded sequences. Instead we can say that undecidability of the Collatz conjecture means we won’t find a non-trivial loop.

[u/GoldenMuscleGod → u/Lehatan]

Here’s a formalized statement: if a sentence is sigma_1 in the arithmetical hierarchy and true then it can be proved by any theory that is sufficiently strong for Gödel’s incompleteness theorems to apply to it, this means if a sigma_1 sentence is independent then it must be false.

In fact this fact is used in the proof of the incompleteness theorems and is one of the most overlooked steps among people who otherwise understand the basic proof strategy. Understanding why you need this for the theorems to work is, I think, arguably the key insight to understand in the proofs

A negation of a sigma_1 sentence is a pi_1 sentence. If a pi_1 sentence is consistent with that type of theory it must be true, if it is false the theory proves it is false.

For intuition, some examples of pi_1 sentences are claims like that a particular Turing machine will never halt when run on empty input, a claim that a particular theory is consistent, or a claim that all natural numbers have a particular algorithmically checkable property.

So examples of sigma_1 claims are that a machine will halt, a theory is inconsistent, or there is a number with a checkable property.

The Collatz conjecture is, on its face, a pi_2 claim. This is like a claim that a particular recursive function is total - that a Turing machine will halt on every input. A pi_2 claim that is independent can be either true or false.

[u/trajing → u/Lehatan]

Yes: forget about ZFC for a second; just think about, say, Peano arithmetic. A proof of independence of some statement over PA means that there is some model of PA in which the statement is true, and some model in which the statement is false. However, in the natural numbers, it has to be precisely one or the other, and it is sometimes possible to apply some reasoning which does not go through "within" PA, but does go through "outside" of PA, in order to determine which it must be. You may have heard that the proof of the first incompleteness theorem involves a statement which is "true, but unprovable", and this is exactly what is meant: the statement expressing the consistency of PA is really a statement of the form "for all n, n does not encode a proof of falsity from the axioms of PA", and - since we know the natural numbers exist, and satisfy the axioms of Peano arithmetic, and every natural number satisfying our provability predicate is a valid proof, we know that this must be true in the natural numbers. However, there are models in which this fails, and we can determine by inspection that the witnesses to the existential must be nonstandard natural numbers - they encode proofs that are infinitely long, or have infinitely long formulas, or have some other kind of defect which makes it externally an invalid proof, but which is impossible to detect "internal" to PA.

This is a very technical subject that involves a lot of moves that feel almost circular, but are not due to subtleties about what goes on inside the model and what goes on outside the model and so on, and IMO it helps to step back a little from thinking about ZFC, which is a very strong theory, to considering just an ordinary ring like any other that displays many of the same logical phenomena under discussion.

[u/Disastrous-Cost2185 → u/Lehatan]

Yes: it is true for any formula with no existential quantifiers.

[u/itkillik_lake]

Con(ZFC), the statement that ZFC is consistent, could maybe be considered a more "concrete" example of an undecidable statement.

Check out Schoenfield's absoluteness theorem. It provides evidence that certain statements like the Riemann Hypothesis are "less likely" to be undecidable.

[u/kieransquared1]

An interesting example of a concrete object for which a certain property is undecidable is whether nested sups and infs of a certain explicit polynomial is a measurable function:  https://arxiv.org/abs/2501.02693v3

[u/Traditional_Town6475]

So here’s a fact: Let T be a consistent theory. If φ is a sentence that neither T proves nor disproves, then there’s a model of T where φ is true and there’s a model of T where not φ is true.

Like Godel showed that PA doesn’t prove Con(PA). Assuming PA is consistent, there’s a model out there where not φ is true, there φ is a sentence when interpreted in the natural numbers has the meaning Con(PA). Whatever that model interpret φ as doesn’t have the same meaning as “PA is consistent”.

So if you’ve heard of Goodstein’s theorem, it says that a certain sequence will eventually reach 0. You can show it’s true for the standard natural numbers using tools outside of PA. But there’s a sense in which this sequence is too fast growing for PA. For natural number n, I will let G(n) denote the number of steps it takes for the Goodstein sequence starting at n to go to 0. Well I can write down what that function does in PA, so now I take a nonstandard model of PA and interpret G. The ideal is the following. Pick a nonstandard N, G(N) gets flung really far ahead of N, such that I can cutoff my model before G(N). Then Goodstein’s theorem is false. I can start at N, and “the number of steps it takes to get to 0 is not in my new model”. This is a very handy wavy explanation of this.

So fast growing sequences can lead to independence results such as above.

[u/GoldenMuscleGod → u/Traditional_Town6475]

Elaborating on Goodstein’s theorem: it is true that PA cannot prove “for every n, the Goodstein sequence beginning with n eventually terminates.” However PA can prove “for every n, PA proves the Goodstein sequence beginning with n eventually terminates.”

This shows that if we really believe PA is sound (that everything it proves is true) then we should believe Goodstein’s theorem is actually true. An insight to be gained from this is that PA (or any sufficiently strong theory really) cannot prove its own soundness. Now soundness implies consistency, so we already knew that from the incompleteness theorems, but an insight we can gain is that theories are “modest” - although they trust proofs, they do not trust themselves in a broader sense. In particular, proving a sentence is true as intended is something more than just believing it is a theorem. Löb’s theorem seems counterintuitive to many people on first glance but it is an illustration of this idea and makes sense once you get that we have intended semantics that go beyond just believing the axioms of our theories.

In the case of PA, the “secret sauce” of our intended semantics is that we want “\exists n Pn” to be true if and only if there is a numeral (expression of the form SS…S0) k such that Pk is true. In other words we want the natural numbers to be exactly the things that can describe the lengths of sentences in our theory. It turns out no set of axioms (not even the set of all true sentences in the language of PA) can enforce this intention.

[u/SwimmerOld6155]

This is an excellent and incredibly subtle question, you could write a book chapter about this. I think my answer to your question is sometimes yes and sometimes no. Let me know if I have not captured the spirit of your question, since you might be asking multiple.

A lot of undecidability arguments involve embedding the halting problem. Assuming the consistency of ZFC, there are Turing machines whose source code we can write down, whose halting is independent of ZFC. Take a Turing machine which searches for a ZFC proof of 1 = 0. This machine cannot halt if ZFC is consistent, but if ZFC could prove that the machine does not halt, it would have proven that ZFC is consistent, which would contradict Godel's incompleteness theorem. This is an example of a pretty concrete undecidable statement - you can write down the source code of such a machine. This fact can then be used to find explicit examples of polynomials which have no integer solutions, for example.

On the other hand, statements independent of ZFC will never have explicit constructions in their proofs or disproofs. The reason is that an explicit construction would probably be itself a ZFC proof or disproof. So constructions will be basically "non-constructive" and often start with a model of ZF, which definitely cannot be constructed within ZFC, ZFC can't prove that ZF(C) is consistent.

As an example, there is no constructible non-measurable subset of R. This is because the statement "all subsets of R are measurable" is consistent with ZF. Any essentially explicit construction of a non-measurable subset of R would probably work with the axioms of ZF (since they are incredibly strong), and hence contradict this theorem. So you're always going to be reaching for weird examples that use Choice or similar axioms in inescapable ways and are not really explicit. CH is not a perfect analogy here but for CH too you would not be able to explicitly construct a set with cardinality between aleph_0 or 2^(aleph_0), because such a construction (by virtue of being "explicit") would probably be realisable in ZFC.

I view what I say in the last two paragraphs as an extension of the Church-Turing thesis in some way.

There is no reason to assume that anything is not independent of ZFC. There are many questions in functional analysis that are independent of ZFC, for example. In some fields there is not much precedent for this.

[u/Lehatan → u/SwimmerOld6155]

Thank you for your explanation. In a way, it seems almost an empirical question as to whether a field of mathematics has undecidable statements in practice.

[u/Keikira]

"P is undecidable in ZFC" just means that there is no sequence of basic inference rules that derives the first-order sentence P or its negation from the set of first-order sentences that comprise ZFC -- usually in a classical proof system, but contextually it can also refer to a non-classical proof system such as the one for intuitionistic logic.

If CC is classically undecidable in ZFC, then either it is independent or an example of Gödel incompleteness -- i.e. it's true but no proof exists. It can't be false with no proof existing, because if it is false then there must be a constructive proof by counterexample (though it might be hard to find), but it could be the case that no sequence of inference rules can derive the universal statement of CC over all positive integers. I also think that it can't be independent because the naturals are part of the constructible substructure of every model of ZFC, so we can't exploit differences between non-constructible substructures of different models like Cohen did for CH. If I'm understanding correctly, this is what you mean by "concrete". (EDIT1: I looked a bit deeper into this and now I'm not so sure that CC can't be independent any more, since there may be possible forcing shenanigans around constructible substructures of models of ZFC when e.g. we use an embedding of a nonstandard model of Peano arithmetic to build our set of naturals and eventually integers.)

CC being intuitionistically undecidable means something slightly different though. It's broadly the same idea: there is no explicitly definable algorithm that takes any positive n to a witness t of the property "C^t (n) = 1". The difference is in how this is interpreted -- intuitionism identifies truth and provability, so if no such algorithm exists then CC is constructively proven and therefore intuitionistically not "true", but the rejection of excluded middle means that this doesn't automatically mean that it is "not true" (="false", which would be a proof that any such algorithm must lead to a contradiction -- something that can be built trivially given any known counterexample). CC is intuitionistically undecidable then if there is no constructive proof that it is true, nor is there any constructive proof that it is false. There is no assumption of an underlying truth value independent from these proofs. This is also a stricter notion than classical undecidability because if you prove that a contradiction obtains if such an algorithm does not exist ("not not CC"), you can classically deduce CC without specifying the algorithm, but intuitionistically this only means roughly that "CC cannot be constructively refuted", and a proof of this can obtain even if CC is constructively undecidable.

[u/tralltonetroll]

If you accept the hydra game as "concrete": https://math.andrej.com/2008/02/02/the-hydra-game/ .

It is "kinda related" to Collatz:

Collatz conjecture: Every starting point hits 1 sooner or later.

Hydra theorem: every instance of the game and every strategy, hits zero sooner or later. This is a theorem in ZF (with or without choice), but not in PA. In PA, it is not decidable whether or not a given instance converges.

[u/jphamlore]

I just wish Gregory Chaitin had decided to not end every other sentence with an exclamation mark.

From Philosophy to Program Size

https://arxiv.org/abs/math/0303352

[u/Moonlight-_-_- → u/jphamlore]

Why is the document written in that style? The content looks interesting (at least at a first glance), but the writing style seems at best satirical and at worst, childish.

[u/jphamlore → u/Moonlight-_-_-]

I am completely baffled about the writing style choice as well.

[u/moschles]

I am left with the question: should we expect ‘concrete’ statements, such as CC, to be decidable? Maybe there is a formal answer to this question, by formalising what a ‘concrete’ statement is, and showing that such statements are decidable. Though, to me, this seems unlikely to be possible, by Gödel.

Collatz is a bad example for what you are attempting to communicate. Collatz could have a non-constructive counter example integer.

Let z denote the counter-example positive integer. Proving Collatz false does not force anyone in the room to construct z.

[u/PLANTS2WEEKS]

I want to point out that Collatz and CH aren't really comparable because of the logic system being used. Collatz is stated over second order logic while CH is over first order logic. There is something called the completeness theorem of first order logic which means there exists a model as long as there are no contradictions. This is probably where you got the idea that if a statement is undecidable you can adjoin either the statement or it's negation and keep the theory consistent. Because, this is true in first order logic.

Collatz is a statement about terminating sequence, i.e. for every n there exist m such that n reaches 1 in m steps. Both n and m are quantified over the standard naturals which means it's not a first order statement. There are non-standard models of the naturals and we can't rule these out. I think a bigger issue is terminating in m steps and how to phrase that. We could say the rule to go from a_k to a_(k+1), require a_0 to be the starting number and require a_m = 1, but there is no way to make sure that m is a finite number of additions of 1 away from 0. It just isn't true for non-standard models of the naturals. On the other hand, if Collatz is false for the standard naturals, it is decidable in both second order and first order logic since the standard naturals are contained within any model of non-standard naturals.

[u/Equivalent-Costumes]

There exists an explicit family of Diophantine equation in integers in which there are no algorithms to correctly identify which one has solutions. This is very concrete.

Because there are no algorithms to decide that, it's also undecidable in the logical sense: given any "reasonable" axiomatic system, there are always an equation in the family which you cannot prove nor disprove that it has a solution; and since if there were a solution you would had been able to prove that, what really happen here is that there are no solutions but you cannot prove that there are no solutions with the current system. This remains the case even if you don't have a fixed system of axioms, but an algorithmic scheme to add axioms as needed.

In fact, there is a way to make this even more concrete. Lob's theorem said that (under every Godelian system, such as even a very weak version of Peano arithmetic without induction) the very fact that proof implies truth is itself should be expected to be unprovable except for known vacuous case; more specifically, given a statement T, a combinatorial object describe statement T as part of a proof system, then given any proof that the existence of the combinatorial object describing the proof of T (from the same axioms) implies T is true, you can modify that proof to get a proof of T itself. You can apply this theorem to a contradictory T like 1=0 to immediately get something unprovable, unless the system itself can prove 1=0, ie. it is inconsistent.

But this can be made even more concrete than that. Under extension of PA we actually have a wonderful scheme to produce such kind of statement. Let's start with PA itself. Let P(n) be the statement that "omega tetration n is an ordinal", more specifically, what the statement really say is that certain type of trees up to height n, under certain specific ordering, is "algorithmically" well-ordered (there are no algorithms to produce a strictly decreasing sequence) - in fact this is actually well-ordered but the concept of well-ordering cannot be stated in PA itself. Then we know the following: we can prove P(0) (in fact this is essentially just the induction axiom), and we have an algorithm that given any proof of P(n) the algorithm produce the proof of P(n+1), and we also has a proof that this algorithm always work. That sounds like we should be able to prove that "for all n, P(n) is true", right? No, we actually can't. In fact, you can prove that "for all n, there exists a proof of P(n)", but that cannot be lifted to show that "for all n, P(n) is true".

Lob's theorem showed that this gap cannot be closed, ever. If you add in axioms that works for individual kind of statement, you can produce more complicated statement where this gap exist. On the other hand, if you attempt to make a general axiom applicable to all T to close off this gap, your system will necessarily have a contradiction.

However, an exercise in attempting to close this gap reveal exactly where the problem lies. Note that in Lob's theorem, the axioms used by the combinatorial proof system must be exactly the same as your actual axioms. If you attempt to fix the gap by adding in as axiom "well, if there exists a proof of T using this axioms, then T is true", then your new system of axioms is no longer the same as the axiom in that statement. This means that you must somehow, in your new axioms, being able to talk about the system of axiom after this new axiom had been added. This is - not surprisingly - a form of self-reference, which should immediately raise a lot of red flags.

And if you think about it, this kind of self-reference existed in ZF itself. ZF lets you define a set P(X) containing all subsets of a set X, while simultaneously let you define a subset of X (hence an element of P(X)) using P(X) itself. Believing that ZF is consistent is believing that this kind of self-reference is safe.

If self-reference is so inherently problematic, why not avoid it altogether? Because being able to declare that certain self-reference is safe is a very strong ontological statement about the nature of finite number itself. Let's think about the example above with the trees. In PA, it is consistent that there exists some n such that simultaneously, there is a proof (more specifically a combinatorial object describing a proof) that "there are no algorithms that produce a strictly descending chain of tree from height n" and also there is an algorithm that does produce such a strictly descending chain of tree. How is this possible? The problem is simple: either the algorithm itself, or the proof, is "fake", it does not correspond to an actual proof or an actual algorithm. But...you cannot write down any actual such n, because we have an algorithm to produce the proof for each particular n. In fact, for each particular number that you can write down, you can prove that such n must be strictly bigger than that number. So what is happening here is that PA is not strong enough to eliminate the possibility that there are some "finite number" that you cannot write down at all. The existence of such a finite number implies that certain form of self-reference is not safe aka. an algorithm runs forever. Conversely, by declaring that certain self-reference is safe, what you are really describing is that certain algorithm which looks really fishy with its self-reference, actually always halt. And the reason you believe it will halt is because you cannot imagine it running forever on any actual number you can write down.

This is the crux of the issue. You want to be able to declare certain self-reference to be safe, because you believe it is true for actual finite number you can write down, because you want your axioms about finite number to have any many true property about the actual finite numbers as possible. But as things become more and more complicated, these self-reference started to look more and more fishy, and one has to wonder where things stopped being intuitively should be true.

And this ties back to the Diophantine example. There are always Diophantine equation whose solution does not exist amongst the one you can write down because it breaks some forms of safe self-reference.

So to answer your question, yes, very concrete statement can be undecidable. It's not a property of non-constructive math at all.

In fact, it's actually possible to produce CH maybe-counterexample very concretely. Take the union of all countable von Neumann ordinal. By construction, it is always of cardinality Aleph_1 . If CH is true, there is secretly a bijection between this set and the real, even if you cannot construct it; if CH is false this is a counterexample.

So, what keeps people hoping that what they are working on isn't one of those case? Probably the fact that we are still very far from any sorts of self-reference that we would consider questionable. Of course, there are always skeptics: there are plenty of people who think that even second-order Peano's arithmetic is already too much self-referential. But for most ordinary mathematician, the kind of questionable self-reference seems extremely far away. For example, if you work in higher category theory, it's not uncommon to run into statements that cannot be proved within ZF, yet seems intuitively should be true; for example if you want to prove that certain algebraic operation always work on categories, you want to be able to talk about category of category, but wait, many categories are already proper classes, so this is something that contains proper classes which is illegal! If you care about ZF, you juggle around this U-small machinery, which seems cumbersome; naturally at some points people (such as Godel) are like "nope, let's just have a big enough universe so that we don't have to do this U thing", and bam, you got yourself Mahlo's cardinal. There is some sense the idea that there are still a lot more self-reference we can intuitively accept to be safe.

(...to be continued)

[u/Equivalent-Costumes → u/Equivalent-Costumes]

(...continuing)

Finally, set theorists usually care about essentially 3 kinds of properties: the arithmetical facts, the "height" and the "width" of the universe. Width is about adding or removing sets which is pretty easy to do and there are many modern machinery to do that, statement like CH is about that. The modern philosophy is that it is risky to even conjecture something that is fickle enough to be vulnerable to adding or removing sets, the usual way to deal with this kind of issue is to add in some sorts of "tameness" requirement, so that instead of talking about all sets of some sorts, you talk only about sets that can be described in some small manner. Arithmetic facts cannot be altered by any known "nice" modifications to the universe, they're absolute, and in some sense they are the most concrete statements, and these include facts that state whether some self-reference are safe. And height essentially are witnesses to self-reference. The general philosophy is that if some self-reference is stated to be safe as an arithmetic fact, then it's also reasonable to assume that height is high enough to witness such fact (more concretely, if there is a Godel number that say "Mahlo cardinal is consistent with ZF", then you might as well just imagine that your universe actually have Mahlo cardinal). Height and width are somewhat linked to each other, which is why there are still hope that eventual understanding of what height are more reasonable to have would finally settle CH.

So to conclude, independence are expected to fall under 3 reasons:

• Too much self-reference: the hope is that it's just happened to be a little bit beyond the level that we had formally accepted so far, but it's not actually far enough that it becomes something that we cannot accept.

• Vulnerable to height issue: if you can accept the required level of self-reference, accepting height should not be a big philosophical commitment.

• Vulnerable to width issue: you should had added enough tameness requirement until it's no longer a problem.

[u/Ok-Side-8171]

For me the most enlightening example is that of consistency of ZF.

By Gödel, it is independent of ZF whether ZF is consistent.

But notice that it is possible to build a Turing Machine that enumerates all the statements that are consequences of ZF, and looks for a proof of 0=1.

Whether this machine will halt or not is, again, independent of ZF, even though it is a very concrete question. Even more, we can actually build this machine in our physical world, and then it will either run forever or not, physically speaking. It is as though our physical world had something to say about which axioms are true.

This example is used to show that “truth” and “following the axioms” are different things. Either ZF is consistent, or it is not. But this will not be mathematically provable from ZF.

 

Ps: A possible way to formalize “concrete problems”  is to take them as the Pi_1^0 problems, those that which can be algorithmically disproved.

[u/logbybolb]

Roughly, Large cardinal axioms assert that "a certain very large infinite set exists". It turns out ZFC has a limit to the type of infinite sets it can prove to exist, and that adding larger and larger types of infinite sets makes it able to prove more statements of a certain type. There is also a concern that the very largest of the large cardinals might lead to contradictions and inconsistencies.

One of Harvey Friedman's main research ethos has been "concrete incompleteness". One of the results I know of is A very short set theory statement which implies large cardinals (I.e, a theory stronger than ZFC): ∀a∃b∀c(∀d∀e(d∈c→((e∈d→e∈c)∧(e∈c→(¬d∈a→(¬e∈a→(∀f(f∈e→f∈d)→e=d))))))→c∈b).

The most promising "concrete incompleteness" to me is Laver Tables: For a natural number n, consider the set {1, 2, ... 2^n}. Then is a unique binary operation ★ on this set with the following rules: For all a, if a<2^n, a★1=a+1, but if a=2^n, a★1=0. also, for all a, b and c, a★(b★c)=(a★b)★(a★c).

For example, the Laver table "times table" with n=2 is:

★ 1 2 3 4

1 2 4 2 4

2 3 4 3 4

3 4 4 4 4

4 1 2 3 4

There is something "truly simple" about it: on my first glance I would've assumed filling in a table would have some algorithm like a sudoku puzzle.

Yet, the result that there is always a unique laver table was only proven using one of the STRONGEST large cardinal axioms. (Specifically, the I3 rank-into-rank axiom). So we have no idea if ZFC can prove the same result.

Renrui Qi has recently extracted a new result from this: A certain fast-growing function called q(n) derived from Laver tables grows extremely fast: Formal theories like PA, ZFC have a "speed limit" to the fast-growing functions they can produce, and so if this function breaks that speed limit, it can't be proven a total function within that theory. I believe there are results which tied together with work from the "Googology" community about this, and it might be unprovable within Peano Arithmetic. (Look into "Ordinal analysis" and the "fast-growing hierarchy" for more information about this "speed limit", as it is one of the most prominent ways to show an undecidable statement)

[u/viking_]

we would have a statement for which we can’t show its truth while knowing we cannot find a counterexample

One of the key notions in mathematical logic is that statements like "truth" and "proof" are relative to a given model. The former is not at all unusual: a statement like "all polynomials have a root" is true in C but not in R. The latter is a little more unusual, but the basic idea is familiar to most mathematicians. For example, since the intermediate value theorem is not true in Q, we know that proving it for R requires some fact about R that is not true about Q. If the only facts we had about R were also true about Q, then we know that we can't prove IVT (or that our system is inconsistent).

https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem is another example, a statement that is true in integers, but not provable in Peano arithmetic.

Similarly, proof by "X is independent of ZFC, therefore it is true in ZFC because no counterexamples exist" (Riemann is the standard value of X here) cannot, itself, be written down in ZFC. X is provable in some other system, but not ZFC, just like the strengthened finite Ramsey theorem is not provable in PA.

[u/FlyOk6103]

I am not a logician either, but I've read about the topic. If Collatz conjecture is false, there is a counter example. But it can be true in some model, while being imposible to prove. Chaitin incompleteness theorem address this. There exist finite systems of diophantine equations over the integers such that the following statement is independent from ZFC: there are infinite solutions of this system. No finite sets of solutions is a proof of them having infinite solutions, a solution can be the last time. And at the same time, it's impossible to prove that there are infinite solutions. Chaiting achieves this by casting Gödel incompleteness theorem into and algorithm which codifies it as a giant system of Diophantine equations.

[u/ant-arctica]

I don't quite agree with your perspective on CH. You can explicitly describe many sets (called cardinal characteristics of the continuum) with cardinality >ℵ₀ and ≤ 2^ℵ₀, but where you can't prove in ZFC that they are =2^ℵ₀. I.e. uncountable sets that inject into ℝ, where you can't construct a bijection with ℝ in ZFC.

So imo it's not "there are weird sets without CH", but rather "CH gives you weird bijections".

[u/Traditional_Town6475 → u/ant-arctica]

It’s no more weird that setting 2^ℵ_0 to any other cardinal consistent with Easton’s theorem. All of them involve forcing “weird bijections”.

[u/ant-arctica → u/Traditional_Town6475]

I was specifically replying to:

But that’s ok, because not every subset of the reals can necessarily be obtained ‘constructively’ through schema specification etc. (I am being informal here, but I believe there is a formal way to say this). So us not being able to produce a counterexample of CH does not mean that one cannot exist.

There are sets that you can explicitly write down that are counterexamples to CH in some model of ZFC.

[u/Torebbjorn]

The important thing is that undecidability just means that neither conclusion follows from the axioms. In any given model of a theory, any (non-meta, I guess) statement is either true or false.

If we for example were to just use the axioms
1. There exists a set with 1 element
2. Given any two sets X and Y, there exists a set which is the union of them (i.e. a set Z so that any element is in Z if and only if it is either in X or in Y)

Then the statement "There exists an empty set" is undecidable. I'm not quite sure how "concrete" such an empty set has to be, but I guess you get the idea.

[u/mathemorpheus]

axiom of choice seems pretty concrete, and it's undecidable in ZF

[u/NotJustAQuant]

undecidable Collatz would just mean true but unprovable, since any counterexample is a finite check. Goodstein is a plain number statement PA can't prove, so why would Collatz get a pass?

[u/jphamlore]

Chaitin's constant

https://en.wikipedia.org/wiki/Chaitin's_constant

In the computer science subfield of algorithmic information theory, a Chaitin constant (Chaitin omega number) or halting probability is a real number that, informally speaking, represents the probability that a randomly constructed program will halt. These numbers are formed from a construction due to Gregory Chaitin ...

Each halting probability is a normal and transcendental real number that is not computable, which means that there is no algorithm to compute its digits. Each halting probability is Martin-Löf random, meaning there is not even any algorithm which can reliably guess its digits.

[u/un_blob]

I think you have it backwards. Undecidable means undecidable. You can't prove the statment true or false. And it is neither true or false, it is undecidable

In CC's case if it was undecidable it would not mean it is true, it would simply mean that it can't be proven true... Or false. Basicaly you can choose, and meke it a new axiome : it is true/false and continue building in parallèle math universes