4.1 Outline of metamathematical properties

4.1a Nonstandard extensions of structures
4.1b Nonstandard extensions of theories
4.1c Comments
4.1d Metamathematics of internal theories: the main results

4.2 Ultrapowers and saturated extensions

4.2a Saturated structures and nonstandard set theories
4.2b Quotient power extensions
4.2c Adequate and good ultrafilters and ultrapowers
4.2d Elementary chains of structures

4.3 Metamathematics of BST

4.3a Warmup: several examples
4.3b Infinite Fubini products of adequate ultrafilters
4.3c Standard core interpretation of BST in ZFC
4.3d Saturated standard core interpretation

4.4 The conservativity and equiconsistency of IST

4.4a Good extensions of von Neumann sets in ZFC universe
4.4b Iterated adequate extensions of von Neumann sets
4.4c Iterated adequate extensions in the \theta-version of ZFC
4.4d Long iterated quotient power chains
4.4e Conservativity of IST by inner models

4.5 Non-reducibility of IST

4.5a The minimality axiom
4.5b The source of counterexamples
4.5c The ultrafilter
4.5d ``Definable'' adequate quotient power
4.5e Corollaries and remarks

4.6 Interpretability of IST in a standard theory

4.6a Standard theory with a global choice and a truth predicate
4.6b Formally definable classes
4.6c A nonstandard theory extending IST
4.6d The ultrafilter
4.6e The interpretation
4.6f Extendibility of standard models

Historical and other notes to Chapter 4