Metamathematics of internal theories

One of the most important metamathematical issues related to any formal theory is the question of consistency: that is, a theory should not imply a contradiction. As long as minimally reasonable set theories are considered, Gödel’s famous incompleteness theorems make it impossible to prove the consistency in any absolute sense, so that usually the results are given in terms of equiconsistency with some other theory, for instance, ZFC. In this Chapter, we prove that the internal theories IST and BST considered above are equiconsistent with ZFC, that is, consistency of ZFC logically implies consistency of both BST and IST. (For the opposite direction, if IST or BST is consistent then obviously so is ZFC as a subtheory of each of IST, BST see Exercise 3.1.3.)