Cosmological lower bound on the circuit complexity of a small problem in logic

An exponential lower bound on the circuit complexity of deciding the weak monadic second-order theory of one successor (WS IS) is proved. Circuits are built from binary operations, or 2-input gates, which compute arbitrary Boolean functions. In particular, to decide the truth of logical formulas of length at most 610 in this second-order language requires a circuit containing at least 10 125 gates. So even if each gate were the size of a proton, the circuit would not fit in the known universe. This result and its proof, due to both authors, originally appeared in 1974 in the Ph.D. thesis of the first author. In this article, the proof is given, the result is put in historical perspective, and the result is extended to probabilistic circuits.