4 ms·
By no means, you know normaly maths are written leaving tons of detail to context, folklore, references and well-knowns with human checkable sketchy proofs but
by jesuslop 9y ago
By no means, you know normaly maths are written leaving tons of detail to context, folklore, references and well-knowns with human checkable sketchy proofs but in contrast here Russell makes one of the first serious attempts to give a self contained and no assumptions, formal presentation of a part of core maths. Something like now the Mizar library or Coq HOTT. Gödel studied deeply this text and proved the epistemological limitations inherent in this program in his famed theorems, in fact Gödel paper title alluded to Russell's ('on the existence of formally undecidable propositions in Principia Mathematica and related systems').