Sequential theories form a fundamental class of theories in logic. They have full coding possibilities and allow us to build partial satisfaction predicates for formulas of bounded depth-of-quantifier-alernations. In many respects, they are the proper domain of Gödelian metamathematics. We explain the notion of sequential theory.

A theory is restricted if it can be axiomatised by axioms of bounded depth-of-quantifier-alernations. All finitely axiomatised theories are restriced, but, for example, also Primitive Recursive Arithmetic. We explain the small-is-very-small principle for restricted sequential theories which says that, whenever the given theory shows that a definable property has a small witness, i.e., a witness in a sufficiently small definable cut, then it shows that the property has a very small witness, i.e., a witness below a given standard number.

We sketch two proofs that restricted theories are incomplete (however complex the axiom set). One uses the small-is-very-small principle and the other a direct Rosser argument. (The second argument was developed in collaboration with Ali Enayat.)