Hacker News Reader

Comment by dvt | Hacker News Reader

> Principia has been criticized by famous logicians like Kurt Gödel as being a “step backwards” from Frege

Kind of a weird dig here towards Gödel, but I don't think typesetting the whole thing's going to do anything to alleviate his points, as he was mainly criticizing the syntax. Logicians were in love with Frege's Begriffschrift for a long while (first seen in the late 1870s[1]). Either way, this was literally Gödel's first paper (published in 1944: "Russell’s Mathematical Logic") and he never mentioned Principia Mathematica again.

[1] https://www.math.uwaterloo.ca/~snburris/htdocs/scav/frege/fr...

View on HN

> he never mentioned Principia Mathematica again.

???

This paper contains a nice summary of Gödel's interactions with Russell. https://www.cambridge.org/core/services/aop-cambridge-core/c...

Gödel's future work on constructible hierarchies and the dialectica interpretation were directly inspired by Principia Mathematica. I agree that characterizing Gödel's view on Principia as a "step backwards" is overly simplistic, but he certainly mentions and takes inspiration form the work throughout his career.

> as he was mainly criticizing the syntax

If you mean to say that Gödel's criticisms of Principia were just about syntax - that is also incorrect. Gödel had substantial complaints about the truthfulness of the axiom of reducibility that (IIRC) Russell himself thought posed a valid attack on the system in Principia.

>Either way, this was literally Gödel's first paper (published in 1944: "Russell’s Mathematical Logic") and he never mentioned Principia Mathematica again.

I'm not sure what you're trying to say here. That paper was nowhere near Godel's first, nor was it the only time he mentioned Principia.

The title of the first of his works on the incompleteness theorem was "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" in 1931.

https://en.wikipedia.org/wiki/On_Formally_Undecidable_Propos...

There's a tendency in proof theory circle to dismiss set theory and related foundational work, yet it is ultimately the basis that is used (other foundational programs with 'better properties' tend to have worse issues). So it's not necessarily a dig towards Gödel, but to show that the book would be dismissed, without any dig to living logicians.

But the reason would be that you find better and easier introductions to the material, where you don't have to internally translate to their more idiosyncratic syntax. Such a project is not going to give it mass appeal, but make it a tad more approachable for highly motivated people.

He mentioned it in the title of the incompleteness paper.

typesetting? huh? edit : oh, they also procedurally produce typeset text in the original syntax from the code in coq

Reply on news.ycombinator.com