How to Write a Long Formula

Specifications often contain formulas that are a page or two long. Mathematicians almost never write formulas that long, so they haven’t developed the notations needed to cope with them. This article describes my notation for using indentation to eliminate parentheses in a formula consisting of nested conjunctions and disjunctions. I find this notation very useful when writing specifications. The notation is part of the formal syntax of TLA+ (see [127]).