Metatheorems from Invariants
For the purposes of this chapter, a theorem is a (true) statement about particular equations, for example ‘(387 implies 43)’ is a theorem. A metatheorem is a general statement about implications; one can usually get many theorems from a single metatheorem. This chapter is all about generating many interesting metatheorems using a meta-metatheorem, called the fundamental property of invariants. If all this is making your head spin, don't worry. Look at the sections below for examples of metatheorems you can probably agree are both concrete and interesting. Once you have done that, come back here and we will show you how to prove these and other metatheorems using invariants.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.