Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

When using a theorem prover that reasons about a certain class of mathematical operators to reason about expressions containing a larger class of operators, we have to hide from the prover the operators it can’t handle. For example, a prover for ordinary mathematics would (incorrectly) deduce that the TLA+ action formula (x = y) => (x’ = y’) is a tautology if it were to treat priming ( ‘ ) as an ordinary mathematical operator. We call this kind of hiding coalescing. This paper shows that coalescing is somewhat more subtle than one might think, and explains how to do it correctly in some important cases.