why is that "unsound"?
what's wrong with an unwritable natural?
Almost all reals are unwritable.
The reality is that mathematicians didn't first come up with the Peano axioms and then study the interesting consequences of them. Both as a matter of history and also as a matter of why most mathematicians do math, mathematicians first came up with numbers, and only later came up with axioms that allow them to do rigorous reasoning about them. The same is actually true of almost all math—real numbers were invented to do rigorous reasoning about calculus, which by that point had been around for a century plus; set theory likewise.
In other words, if the goal is to come up with any old consistent set of axioms, you can assume an unwritable natural number, that's fine, go ahead. But if your goal is to study natural numbers—which, like, I have a lot of experience with natural numbers in my day to day life, I'm pretty sure I could write all of them if I had enough time and space and so on—then you want to study natural numbers, not some other weird things where there are unwritable weird things.
This goes to the parent comment's point about real numbers though. It's silly to assume unwritable real numbers. Why do we do so?
This is unsound in that it runs counter to certain philosophical commitments, namely that there should be some tangible, physical realization of all the natural numbers (although if you really go far in that direction you end up with ultrafinitism, which most set theorists would find unpalatable, so the philosophical implications of all this are rather tricky).
The difference here is that with busy beaver numbers, e.g. BB(101) we can, presumably, write their values with our notation; it's just that we often cannot prove that any particular value written in our notation does indeed denote the value for that function. So if we write 100000...0000 with an unholy number of 0s there, it might be the value of BB(101), in particular we might not be able to prove that it isn't.
On the other hand, for a non-standard number, c, it is definitely the case that 100000...0000 is not c, because, whatever c is, it is strictly greater than 100000...0000, or any other number we can write down.
And thus when it comes to proofs about the termination of Turing machines that do not actually terminate, the unsound system is claiming that some machine terminates, but it doesn't terminate in 1 step, nor 2 steps, nor 3 steps, nor ... nor 100000...0000 steps, nor 100000...0001 steps, nor 100000...0002 steps, nor .... However, regarding the BB(101), the (presumably) sound systems we use such as PA, or ZFC, do not claim that BB(101) isn't 100000...0000. They just may not be able to prove anything one way or the other.
It is true though that various (decidable) proof systems are unable to prove that the Busy Beaver function has any specific value beyond a certain point. However, where that cut-off is varies from proof system to proof system, with stronger proof systems being able to prove more an more values of the Busy Beaver function.
Maybe you find it weird that we can prove (Exists x. P x) without being able to prove P n for any particular numeral n? Welcome to the strange world of classical (i.e. non-constructive) mathematics.
Isn't the result stronger than that though? The value of BB(30) might be X. Or it might be Y. Neither value would cause any problems.
Thus, "the value" doesn't exist. There is no value that is the value of BB(30).
But! that does not mean that all these systems are sound, for if you add the incorrect value as an axiom, specifically if you add anything but the smallest value 'm' such that BB(30)=m is independent of ZFC, then you are in a similar situation to adding ¬Con(ZFC) whereby you only have non-standard models.
They way this works is that, suppose BB(30)=m for some particular m is independent of ZFC, but BB(30) is not actually equal to m. What we will find is that there is some Turing machine M and some non-standard natural number q such that, while M doesn't actually halt in reality, according to some non-standard model it does halt in 'q' number of steps, and, in this model, when it does halt, it leaves 'm' 1's on the output tape.
That said, your comment did push me towards the limits of my comfort zone, so it might be helpful to double check what I'm saying. I don't see how it could be any other way though.
If BB(30) truly equals some particular numeral m, then there actually does exist a Turing machine M that has no more than 30 states and does halt with m 1's on its tape. Not only does this machine really exist, but the fact that it halts in this state is true Delta_0 statement, and thus it is trivially provable, you don't even need induction. It is provable in Robinson Arithmetic, it is provable in Peano Arithmetic, and it is provable in ZFC. Thus we have that RA proves "BB(30) ≥ m" and PA proves "BB(30) ≥ m" and ZFC proves "BB(30) ≥ m", etc.
By transitivity each of these systems also proves "BB(30) ≥ m₀" for every numeral m₀ less than m. But if m₁ is a numeral larger than m, it is no longer the case that RA proves "BB(30) ≥ m₁" and PA doesn't prove "BB(30) ≥ m₁" and (assuming ZFC is sound) ZFC doesn't prove "BB(30) ≥ m₁"
Thus we "can tell" what the true value of BB(30) is because it is the greatest value in which RA (or PA or (presumably) ZFC) proves "BB(30) ≥ m" for the numeral m denoting that value. Equivalently the value of BB(30) is the least value m for which RA, PA, or any other sound system, does not prove "BB(30) ≠ m".
We "can tell" this value even if we might not be able prove it in PA, or ZFC, or "ZFC + there exists a Mahlo cardinal". Indeed each different proof system likely can extend the range of BB values that are provable.
If you add an axiom "BB(30) = m" for some particular numeral m as an axiom to ZFC and it is the wrong value of m, you will either get an inconsistent system if "m" is too small, or you will get an unsound system if "m" is too large. In case "m" is to large, the unsound system will wrongly prove that certain Turing machines halt that do not actually halt. Specifically it will falsely prove that the Turing machine that searches for (a Turing machine with no more than 30 states that halts with "m" 1's on it tape) will halt, when such a machine does not actually halt.
> This independence is sometimes interpreted to mean that these questions have no answer, but most set theorists see that as a profound misconception. They believe the continuum has a precise size; we just need new tools of logic to figure out what that is. These tools will come in the form of new axioms.
I believe the same applies for BBs. They have precise values outside of ZFC but we still cannot ever know them because they are incomputable (??)
That doesn't mean you can't know them. We know BB(2). It means there is no single algorithm which is capable of yielding them all. But there could, theoretically, be an algorithm for BB(10), a different algorithm for BB(11), etc.
In fact, those individualized algorithms don't exist either.
You cannot run a machine for "that many" steps because such a value is unreachable by steps. Non-standard models have a set of values that begin with a copy of the actual natural numbers, followed by some ordered set of copies of the integers in the sense that any values "beyond" the initial natural numbers have an infinite number of successors and an infinite number of predecessors, like integers do. By counting in steps it is not possible to move from a value in the initial natural number fragment to one of these non-standard values, because there are an infinite number of values in between them that you would be required to step through.
That's true for most real numbers in ordinary mathematics too, so if you accept the existence of those numbers, no reason why you can't do the same for the natural numbers in these non-standard models.
> You cannot run a machine for "that many" steps because such a value is unreachable by steps. Non-standard models have a set of values that begin with a copy of the actual natural numbers, followed by some ordered set of copies of the integers in the sense that any values "beyond" the initial natural numbers have an infinite number of successors and an infinite number of predecessors, like integers do. By counting in steps it is not possible to move from a value in the initial natural number fragment to one of these non-standard values, because there are an infinite number of values in between them that you would be required to step through.
Yes...