The fundamental theorem of Ehrenfeucht-Fraisse games. It seems innocuous (because of the game formulation?) but the applications never stop. It provides a natural way to prove a property is not expressible in a logic. It is one of the tools of classical model theory that is also used in finite model theory. In the related notions of bisimulation and simulation, we have a cornerstone concept of concurrency theory and program verification.
|
1 | [made Community Wiki] | ||
|
|
||||
