Summary: More examples using formal proofs (inference rules) for determining whether a formula is true.
The theory of a programming language type system would be all the provable statements about which programs typecheck.
The theory of WaterWorld is all the provable statements about safety in all possible boards.
Note: alternate syntax for proofs (overbar)