I'd like some elaboration on that. I failed to find a source.
Surely the principia and similar efforts will still yield useful results even if they cannot necessarily prove every true statement from the axioms?
So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class.
On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to some entity external to your analyzer, and your IDE shouldn't be able to catch that.
Also Russel himself ruined the cathedral of Frege with its eponymous paradox, he was clearly among the best to understand how a thing like Godel's incompleteness theorem could come along the way.
And for his relation to madness, his personal life have been felt with many turmoil from an early age. If anything it seems that mathematics saved him, preventing his early desire for suicide.
https://plato.stanford.edu/entries/neutral-monism/
https://en.wikipedia.org/wiki/Copleston%E2%80%93Russell_deba...
The way formalists (mainstream mathematical community) dealt with the foundational issues was to study them very closely and precisely so that they can ignore it as much as possible. The philosophical justification is that even though a statement P is undecidable, ultimately speaking, within the universe of mathematical truth, it's either true or false and nothing else, even though we may not be able to construct a proof of either.
Constructivists on the other hand took the opposite approach, they equated mathematical truth with provability, therefore undecidable statements P are such that they're neither true nor false, constructively. This means Aristotle's law of excluded middle (for any statement P, P or (not P)) no longer holds and therefore constructivists had to rebuild mathematics from a different logical basis.
The issue with Principia is it doesn't know how to deal with issues like this, so the way it lays out mathematics no longer makes total sense, and its goals (mathematical program) are found to be impossible.
Note: this is an extreme oversimplification. I recommend Stanford Encyclopedia of Philosophy for a more detailed overview. E.g. https://plato.stanford.edu/entries/hilbert-program/
If incompleteness isn't the killer of the Hilbert program, what is? The axiom of choice and the continuum hypothesis. Both lack any form of naturalness that would prevent any philosophical arguing. Worse, not accepting them also do. There is such a wealth of intuitionistically absurd results implied by these systems -- most famously, there is the joke that “The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma?”, when these 3 statements are _logically_ equivalent. So, we're back to a mathematical form of epistemological anarchism; there is no universal axiomatic basis for doing mathematics; any justification for the use of one has to be found externally to mathematics.
"In mathematical logic, a theory is categorical if it has exactly one model (up to isomorphism)."
(categorical is stronger than complete)
Am I missing something, or has the project only just begun?
https://github.com/ndrwnaguib/principia/blob/main/Principia/...
Which theorem are you trying to prove?
Sorry if this is obvious in one of the links, but does there exist a high quality “OCR-ed” version of the original text?
I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!
Lean is also a lot faster.
What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.
What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?
Because from what I understand Rocq too has Gallina or something right?
I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.
Few style Remarks: I personally would not call them Prof. Or Dr. In formal English that would be the latter. But the name of them stands for itself.
wanderlust123•9mo ago
ndrwnaguib•9mo ago