Editing Busy beaver (section)

==== Consistency of theories ====
Another property of S(n) is that no arithmetically sound, computably axiomatized [[Axiomatic system|theory]] can prove all of the function's values. Specifically, given a computable and arithmetically sound theory <math>T</math>, there is a number <math>n_T</math> such that for all <math>n \geq n_T</math>, no statement of the form <math>S(n) = k</math> can be proved in <math>T</math>.<ref name=":62" /> This implies that for each theory there is a specific largest value of S(n) that it can prove. This is true because for every such <math>T</math>, a Turing machine with <math>n_T</math> states can be designed to enumerate every possible proof in <math>T</math>.<ref name=":62" /> If the theory is inconsistent, then all false statements are provable, and the Turing machine can be given the condition to halt if and only if it finds a proof of, for example, <math>0 = 1</math>.<ref name=":62" /> Any theory that proves the value of <math>S(n_T)</math> proves its own consistency, violating [[Gödel's incompleteness theorems|Gödel's second incompleteness theorem]].<ref name=":62" /> This can be used to place various theories on a scale, for example the various [[Large cardinal axiom|large cardinal axioms]] in [[ZFC]]: if each theory <math>T</math> is assigned as its number <math>n_T</math>, theories with larger values of <math>n_T</math> prove the consistency of those below them, placing all such theories on a countably infinite scale.<ref name=":62" />