Hacker News new | past | comments | ask | show | jobs | submit login

Yes, what you are saying is indeed the case in the sense that if BB(30)=n for some particular numeral n is independent of whatever proof system we are focusing on, for the sake of argument let's say ZFC, (though 30 feels a a bit on the low side for ZFC), then we can consistently add BB(30)=n or BB(30)≠n as axioms to the system, the same way to can for any other independent statement. And there will be arbitrary large values of n that are independent, so we could add BB(30)=n or we could add BB(30)=m or so forth for any numerals i so long as BB(30)=i is independent of ZFC (or whatever axiom system we are considering).

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: