...richness.)

A closer look at this proof reveals the second famous Gödel theorem: the consistency itself is an example of unprovable ¬s_x. Consistency C of A is expressible in A as divergence of the search for contradiction. 112#112 intersects 113#113 for some prefix a. C implies that 114#114 extends 115#115, and, thus, 116#116 both diverge. So, C →¬s_a. This proof can be formalized in A which yields 118#118. But 119#119 implies 120#120, so C, 121#121 are incompatible.

Leonid Levin
Wed Aug 21 20:35:42 EDT 1996