8 ms·

> 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

by dvt 5y ago

> 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/frege.html https://www.math.uwaterloo.ca/~snburris/htdocs/scav/frege/fr...

drdeca 5y ago
typesetting? huh? edit : oh, they also procedurally produce typeset text in the original syntax from the code in coq
Rerarom 5y ago
He mentioned it in the title of the incompleteness paper.
woolion 5y ago
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.
bees_buzz 5y ago
> 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/content/view/0C347F171985A54395CDA89D31C4A59A/S1079898616000354a.pdf/russell_and_godel.pdf 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.
Arainach 5y ago
>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_Propositions_of_Principia_Mathematica_and_Related_Systems https://en.wikipedia.org/wiki/On_Formally_Undecidable_Propos...

by dvt 5y ago

drdeca 5y ago

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

Rerarom 5y ago

He mentioned it in the title of the incompleteness paper.

woolion 5y ago

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.

bees_buzz 5y ago

> 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/content/view/0C347F171985A54395CDA89D31C4A59A/S1079898616000354a.pdf/russell_and_godel.pdf 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.

Arainach 5y ago

>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_Propositions_of_Principia_Mathematica_and_Related_Systems https://en.wikipedia.org/wiki/On_Formally_Undecidable_Propos...