How to Write a Long Formula

FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. |

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]).