In this section we try to identify the creative aspects of the proofs with specific formulas of logic. We use Zermelo-Fraenkel set theory, formalized in first order logic, because its power allows formulas that are closer to expressing the human ideas behind the proofs.
The traditional proof and the proofs by Winograd, Minsky and Stefanuk can all be based on the following sentences of set theory axiomatized in first order logic.