Sure, but that didn’t stop you from describing them as TMs that halt. Isn’t that the sort of statement you’re arguing is meaningless?

It’s not easy to only ever talk about proofs, but never about the meaning of the statements that they’re proofs of. And why should we? If we didn’t think that a statement has a meaning, that it’s either true or false, and that its provability implies its truth, why would we care about proving it?

]]>For all n > 2, **BB(n) < BBB(n) < BB(n + 1)**.

I don’t know how to prove that, but my intuition is the following.

On each execution step, a machine does three things: print some color, move left or right, then go to some state. Call these things together an *action*.

A 2-color n-state program has 2n actions (one per color per state). For a halting program, at least one of these actions tells the machine to halt. A halting action cannot contribute to the computation, so a halting program is effectively operating with 2n – 1 actions. The BBB game does not require programs to halt, so that wasted halt action can be used for something more productive. A program can operate with all 2n actions, and can thus do more computation.

On the other hand, a halting (n + 1)-state program has 2n + 2 actions. One of these is a wasted halt action, so it’s really operating with 2n + 1 actions. This is more than the nonhalting n-state machine’s 2n actions, so the halting (n + 1)-state program can do more computation, and BBB(n) < BB(n + 1).

Can anyone come up with an explicit construction to show this?

]]>Firstly, what do you mean by M’s haltingness being “decidable”…?

Fix a theory T and an input I and let M be a machine. M’s haltingness on I is decidable in T if there is a proof in T that M halts on I or there is a proof in T that M does not halt on I.

The haltingness of all halting machines is decidable, and the haltingness of some and only some nonhalting machines is decidable. I conjecture that the haltingness of any n-state machine for n under 5 is decidable.

I hold these truths to be self-evident, that every Turing machine either halts or runs forever, and that which it does is a fact independent of all theories, interpretations, and models. And that to decide these facts, theories are instituted among men, but when a theory fails to decide the facts to our satisfaction, we have the right, we have the duty, to replace it by a better theory.

I don’t deny any of that, so maybe we are arguing at cross purposes. It sounds like you are arguing against an extreme constructivist position that identifies truth with provability. That may be STEM Caveman’s position, but it isn’t mine. All I’m saying is that it’s a good idea to separate those arguments that make unavoidable appeals to LEM from those that do not. (I guess I am a moderate, open-minded constructivist.)

In fact, from a platonic standpoint, it doesn’t matter whether or not you care about the distinction, because it always already exists anyway. For let P be a provable claim. Then either P can be proved without LEM or it cannot be proved without LEM (is that claim itself constructively valid???). So my claim is just that it’s a good idea to keep this distinction in mind. If you make a LEM argument, does it really need LEM, or can it be done without? This is like asking whether a theorem of geometry can be proved without set theory. Ignoring the distinction or not is just a matter of hygiene.

Do you have any examples of arguments that make unavoidable appeal to LEM that don’t have to do with halting, incompleteness, uncountable sets, etc?

]]>Just stating theorems more carefully sounds easier in theory than it actually is in practice. This becomes important for proof assistants and automatic theorem proving. Even those intuitionistic dependent type theories used in Coq and some other proof assistants are no pancake in this respect.

But I basically agree with you that no change to the foundations of mathematics with respect to arithmetic is required (regarding excluded middle). Even for second order arithmetic, I see no indications that being careful about excluded middle would change the conclusions in any meaningful way. The story is different for third order arithmetic.

]]>It sounds like most of the problems you describe could be solved by just stating theorems more carefully, without any change to the foundations of mathematics.

And yes, the No-Free Lunch Theorem seems like a perfect example of its name: a failed attempt to get a nontrivial conclusion out of a trivial argument. 😀

]]>This, incidentally, was also Gödel’s position (Gödel went even further, hoping for “self-evident” axioms that would settle the Axiom of Choice and the Continuum Hypothesis, something on which I’m completely agnostic).

The Axiom of Choice is well researched and understood extremely well. The Continuum Hypothesis is also well researched, but not understood so well. The currently accepted foundations of mathematics are ZFC, and it would be a mistake to assume that ZF is an improvement over ZFC. It is well know when and why Choice can make trouble, and some good ways to cope with it are known too.

When restricted to arithmetic, I have yet to see a single problem that this position leads to.

The problems are not in the proofs, but in the statements of the theorems being too vague (or idealized) about what has actually been proved. The classical symptom of this are corollaries stated after the main theorem, which turn out not to be corollaries of the main theorem itself, but only of its proof.

Take the model existence theorem for first order logic, as an example. For me, being computable in the limit means that the existence implied by that theorem has a nice specific interpretation of what it means, and of what it doesn’t mean. But since the theorem is normally just stated in a way that the existence it proves might also just be of the type ensured by the Axiom of Choice (the best way to interpret is I know so far is that I will be unable to construct a contradiction), I wondered for years what sort of ontological commitments might be sufficient for proving it (even so in the end the answer turned out to be sort of trivial).

Or maybe a better example is the other way round, where the theorem suggests that the proof showed something much more nontrivial than it actually did. The No Free Lunch Theorems for Optimization are paradigmatic examples of this problem.

- I would modify that to say “Turing machines for which haltingness is decidable”.

Then this is really the crux of the disagreement. Firstly, what do you mean by M’s haltingness being “decidable”: do you mean there has to be a TM to decide whether M(x) halts for arbitrary x? If so, why is that relevant at all to the definiteness of whether M halts on a *specific* x? Or do you mean that M’s haltingness has to be *provable*? If so, provable in which theory: PA? ZF? Large-cardinal theories?

Rather than trying to adjudicate any of that, I take a far simpler approach. I hold these truths to be self-evident, that every Turing machine either halts or runs forever, and that which it does is a fact independent of all theories, interpretations, and models. And that to decide these facts, theories are instituted among men, but when a theory fails to decide the facts to our satisfaction, we have the right, we have the duty, to replace it by a better theory.

This, incidentally, was also Gödel’s position (Gödel went even further, hoping for “self-evident” axioms that would settle the Axiom of Choice and the Continuum Hypothesis, something on which I’m completely agnostic). When restricted to arithmetic, I have yet to see a single problem that this position leads to.

]]>Thanks for clarifying on sigma vs. “ones”!

According to “http://turbotm.de/~heiner/BB/mabu90.html”, cited as [10] in Scott’s survey article, there are two sigma(5) candidates with 4098 ones, among them the Marxen-Buntrock BB(5) candidate. Both machines are described to execute 1L in Halting state and to overwrite 0, so that the best known result for sigma(5) is 4097 if the machine does not write 1 in Halting state.

Funny that there exist not one but two candidates for sigma(5).

So the Marxen-Buntrock BB(5)/sigma(5) candidate uses 12,289 squares of space but produces 4097 ones only. If that candidate is the true champion, then it behaves differently than the champions for BB(1), BB(2), BB(3), and BB(4) which produce almost as many ones as they use space.

I also simulated the other sigma(5) candidate which I can confirm makes 11,798,826 steps. It is more memory-effective than the BB(5)/sigma(5) candidate: For producing 4097 ones it only needs 6145 squares of space.

]]>**1LB 1LC 1RC 1LD 1LA 1RD 0LD 0RB**

This one hits state B at step 2819 before spinning out into state D. If this is right, then **BBB(4) >= 2819**.

The 2568-step candidate left its tape totally blank before spinning out, giving it a disappointing sigma count of 0. This one has a sigma count of **69** (that is, it leaves 69 ones on the tape, in one consecutive block in fact). For comparison, the sigma count of the 4-state busy beaver is 13.