Journey to the Edge of Reason: The Life of Kurt Gödel

this says nothing about whether the statement is true, just whether the expression is constructed according to the formal rules of the system.

all subsets that can be formed from the infinite set of counting numbers is also one of those larger alephs—in fact, it is exactly equal to the cardinality of the continuum.

brilliantly sidestepped that pitfall by substituting the concept of provability for the concept of truth.

proof is a sequence of formulas, so a complete proof can be represented by a sequence of numbers.

One way to reduce the abstract notion of numbers to logical concreteness was through set theory. A set, or “class” as Russell called it, is simply a group of things. The elements that make up a set can be either explicitly listed or defined by a shared property: the set of black cats; the set of primary colors; the set of the numbers 1, 7, and 23;

As Brouwer noted, there is a fundamental distinction between demonstrating that a system is correct

Cantor made the remarkable discovery that infinity comes in different sizes.

proving the completeness of first-order logic,

there is no possible series of proof steps, starting from the axioms of the system and proceeding by its valid laws of inference, by which formula number g can be derived. But formula number g is that proposition G itself. G in other words states: “G is unprovable.”