Hacker News Reader

> because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets

Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. And no finite enumeration of steps can prove that it doesn’t halt eventually.

Since the statement is infinitary, it’s liable to avoid being probable if our axioms don’t capture it - and so computable set of axioms captures all true statements.

And if we can’t prove that a particular Turing machine of N states doesn’t halt, we can’t prove any value for BB(N), as otherwise we could just staple the first BB(N) states of the Turing machine to show it doesn’t halt, which we can’t prove.

> Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N.

Machines that halt can always be proved to halt, as you say just by exhibiting them running to halting. (In principle at least; in practice this can be quite difficult.)

Machines that don't halt fall into two groups: those that can be proved not to halt and those that cannot be proved not to halt. Provably non-halting machines are not rare or strange. For example, a machine can wind up getting stuck in one state that just moves off to the edge of the tape forever. If this happens, it's obvious that the machine will never halt, and that's provable.

Sometimes non-haltingness has an infinitary character, but not always.

The incompleteness proof depends on the input to the program under consideration, BB is limited to programs that don’t have any input which makes the incompleteness proof irrelevant.

For similar reasons you can have a solution to the halting problem given a program of infinite size that is only considering programs of finite size with finite inputs.

This is not a material distinction: for every pair (M, input) you can create a machine M’ which has no actual input and instead first writes down the input to M onto the empty tape, and then runs M. This technique practically allows you to perform most of the same proofs on inputless machines.

> For similar reasons you can have a solution to the halting problem given a program of infinite size.

Sorry, what is a “program of infinite size” in context of Turing machines?

> This technique practically allows you to perform most of the same proofs on inputless machines.

Emulating a machine allows you to know stuff that the machine being emulated can’t such as the width the the data written to the tape. It seems reasonable that you can still prove incompleteness, but I suspect it’s non trivial.

> Sorry, what is a “program of infinite size” in the context of Turing machines.

“The choice of which replacement symbol to write and which direction to move is based on a finite table that specifies what to do for each combination of the current state and the symbol that is read.” https://en.wikipedia.org/wiki/Wikipedia

Replace “finite table” with “infinite table”.

Well yes, and a proof system with the omega rule also escapes incompleteness, but I never yet saw anyone prove a theorem by checking it held for every natural number.

I might be misunderstanding something, but I don't think an infinite table makes sense? Each machine has a finite set of states and operates on a finite alphabet, so the size of the table will always be at most the product of those two numbers.

You need the table before the machine starts, so “current state” is finite but possible states isn’t.

Think a given natural number X is finite Aka 2, a list of all natural numbers is infinite.

Still confused — aren't we talking about a particular machine? Obviously the number of possible states in any given machine is unbounded, but the number of states in one particular machine is finite.

Ahh, realized I wasn’t clear about this. By definition a touring machine has finite internal states, that’s also changed to infinity.

Think of a machine that:

  1 Knows it’s position on the tape 
  2 looks that position up on a table
  3 writes the resulting cell to the tape
  4 moves one position to the right
  5 repeats from 1

With a finite table it’s going to run out of bounds, with an infinite table and the ability to store arbitrary position it’s always going to be possible to have a unique cell.

Infinitary in the sense that a proof of non-halting must be strong enough to establish something about all natural numbers (does not halt after 1 step, does not halt after 2 steps, does not halt after 3 steps…) which cannot be done on a case-by-case (“finitary”) way. In contrast to a proof of halting, which can be so done.

The usual way to deal with an infinite number of cases is to group them into a finite number of cases and then deal with those. That's how induction works. So if you can prove that (1) the machine is in a certain condition at some step and (2) whenever the machine is in that condition at some step it will get back into that same condition at a later step, then you can prove that the machine will never halt.

Right, the act of iterating a cycle might be infinite but the cycle itself is finite. Proving that nothing can break the cycle is possible in many simple cases.

"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would."

It can not. The TMs can only be affected by things that affect them at a finite level. To put it another way that may be easier to see, for them to have a different idea about a given BB number, there must be two otherwise identical machines facing their decision about what state to transfer into, but the one armed with the CH must choose one state and one without it must choose another. (There must always be some such first state, even if it is the very first transition.) There's nowhere to encode that inside a TM state transition table.

That is the "outside" mechanics of a TM, which are fully defined by the problem itself. The "inner" mechanics of a TM, where we talk about what the machine is "really doing", may have such effects, but that's a bit more mundane. And not even necessarily relevant; while you may have two machines, one with ZFC+CH and one with ZFC without CH, they're both going to be hammered by a machine doing "something" that definitely isn't just running a clearly-defined axiomatic system over propositions, but something "mixed up" beyond all human understanding.

What can affect the BB number is oracles. This is also in some sense "why" oracles are defined as essentially function calls that TMs can make with a sort of equivalent of a system call operation that user space code can use to invoke a kernel's functionality... you can easily encode that into a single finite state transfer. BB relative to an external oracle can be (and is) different than conventional BB. However, while the numbers are larger... much, much, much (etc.) larger... I think in some sense it's also less mathematically interesting and returns to just being "yet another large number generator"; BB is interesting precisely as the boundary between computability and non-computability, and BB+oracle is just straight-up uncomputable. But that's not that interesting, really; there's an infinite number of already-uncomputable functions anyhow.

It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.

> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt.

Just to add, this can only happen for a Turing machine M that does not actually halt. If you take a system which cannot prove that M does not halt, you can consistently add a new axiom that M halts - but the number of steps to halt, and thus BB(n), will be a non-standard number.

> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt.

In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.

I disagree but am open to being corrected. It's possible that for a TM named X there is a proof that it halts in ZFC+CH and there is a proof that it does not halt in ZFC+notCH. This would mean that X does not actually halt but that ZFC+CH contains a non-standard model of the integers [1] where BB(n) = some non-standard integer.

[1] https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

That might affect your proving power but it won't affect the Turing Machine itself. That Turing Machine either will or will not halt after the given number of steps, regardless of whether or not you "hand it" the CH or not. To change the result of BB requires not a change of how you are approaching the proof but the behavior of the TMs themselves, but the TMs are well-defined. Regardless of the computability of the number, BB(10,000,000) is a particular number, regardless of what proof system you try to approach it with.

Amusingly, this opens up the distinct possibility of a wrong proof. You take the CH as an axiom, or, perhaps more likely, some other attractive axiom more relevant to the task at hand, and you "prove" a result with that axiom, but then you never find out that your proof is wrong and in fact the TM's behavior is other than what you proved, because... how are you supposed to run a TM for 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 steps to check your proof anyhow? (Especially since that number would be the tiniest insignificant baby steps for the BB(7) winner.)

Again, if you want to change the BB number, you need to change the Turing Machines themselves, most commonly by adding an oracle to them to result in BB*.

But that's not what OP said and you're stating something that is very different. OP said the following:

"I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would."

And the answer to that is yes, it's in principle possible that ZFC+CH contains a proof that a given TM halts after N steps while ZFC+notCH contains a proof that said TM does not halt after N steps. If that were the case and assuming that both are consistent it will be the case that said TM does not in fact halt (period) and that ZFC+notCH uses a model of non-standard arithmetic in its proof.

You mention the possibility of a wrong proof, but that is mixing up the notion of proof and truth which are not the same things. The proofs in ZFC+notCH and ZFC+CH are both correct since a proof is nothing more than a syntactic structure that adheres to certain rules. It's that ZFC+notCH is using a model of natural numbers that is not what most people normally consider to be a natural number, it's using a model of natural numbers that admits for the possibility of incredibly large numbers that are larger than any ordinary/standard natural number. In effect ZFC+CH would contain a proof that after some unimaginably large number of steps the Turing machine halts whereas ZFC+notCH does not allow for the existence of numbers that large.

So the main concept here is that two formal systems may have different notions of what a natural number is. We humans share some idea of what a natural number is supposed to be and we call those the standard natural numbers but the problem is that there is no formal way to precisely pin down those numbers without also allowing for the possibility of bizarre non-standard natural numbers as well. In this hypothetical case we would conclude that ZFC+notCH comes closer to modelling what we consider the actual natural numbers compared to ZFC+CH, but nevertheless it's impossible for any first order formal system to fully specify the natural numbers and only the natural numbers.

I'm the OP. That was exactly my question, great explanation. I've been confused by similar apparent paradoxes before, where I didn't clearly distinguish something being true inside the theory and outside of it.

Again, in order to affect the TM's execution time, the "proof difference" must have a first step where your TM with CH takes a different step than the one without CH does. There can be no such first step. There is no room in the TM specification for that. It doesn't matter what you prove or don't prove, the TM "with CH" and the TM "without CH" must take the exact same steps.

You are messing up proof vs. truth. Your proof doesn't affect how long a TM runs for. Your axioms do not affect how long the TM runs for. Show me, in the state table of the TM, where the CH or any other axiom you use for analysis affects the truth table or the execution time of the TM. No amount of analysis can change how many steps a TM runs for. The numbers may be large, but they are finite and completely determined. The only thing it can affect is whether you can know the number, but the number exists regardless.

Even more concretely: Show me how your choice of axioms affects BB(4). Show me how it affects the number of steps, without redefining BB. Forget CH; take any axiom you like... for the analysis. Just don't affect the TM itself; that's a given for you. Take anything else you like and show me how it changes the BB(4) number. You can't. You can easily take axioms that will produce a wrong result; most notably we could just take as an axiom that BB(4) = -4. The resulting analysis will show that BB(4) is -4. It will also be wrong.

I am confident my explanation addresses OPs original question, which is whether two different (and consistent) formal systems can disagree about whether a given TM halts or not (and hence differ about what the value of BB(N) for some N), and the answer is yes they can. The source of that disagreement would come down to two different models of natural numbers where the theory that proves that a given TM halts only models non-standard natural numbers whereas the theory that proves that the given TM does not halt contains a standard model of the naturals.

What you're discussing is a completely different matter that while is interesting, does not address OP's issue and is something I already responded to by stating that one must be very careful to differentiate between what is actually true versus what can be proven by a formal system. You are blurring the lines between the two but that distinction is critical to understanding the point being made.

So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it can enumerate all theorems of ZF(C). But because of Gödel, at some point it must necessarily either get stuck in a loop or return "can’t prove or disprove this" for some candidate theorem. As I understand it, the result relayed by Scott proves that N=7198 – as in a state space of merely 13 bits – is sufficient to construct a Gödel-territory TM (but this is just an upper bound)! Having an unbounded tape as a scratch space helps, of course.