"The intuitively attractive ideal of having a system in which every true statement you care about can be proved is not achievable".
Sure it is. But the system cannot contain infinities or real numbers of infinite precision. The halting problem for deterministic computers with finite memory is solveable - the system must either halt or repeat a state, and if it repeats a state, it's in an endless loop. Yes, the number of states may be very large, but not infinite.
An interesting question to ask is "do we need infinities". In a sense, infinities are a convenience feature to make formulas simpler. Without infinities, everything has edge cases, bounds problems, tolerances, and all the annoyances known to people who do serious computer number-crunching. Theory in that area has lots of case analysis.
It's perhaps unfortunate that Russell lived in the pre-computer era. Simple theorems were essential in the paper and pencil era. In the 1970s and 1980s, Boyer and Moore took on much the same problem as Principia Mathematica. They published "A Computational Logic"[1], and built the first good inductive theorem prover for constructive mathematics. (I used it back then, and a few years ago I got it running again on Common LISP and put it on Github, so you can still run it.[2]) Proofs that come out of that thing have lots of case analysis. Mathematicians used to hate proofs like that. Many still do.
At one point Boyer and Moore formalized what a floating point unit does, and this was used to verify an AMD floating point unit. This followed an embarrassing recall of Intel CPUs that were slightly off on division, and was paid for by AMD. It's a huge, ugly problem to formalize, compared to the ordinary rules for real arithmetic. It is, however, a system in which every true statement you care about can be proved.
The proof of the four-color theorem shook up the field. Thousands of cases. A simple problem with a huge proof that required machine assistance was a new thing back then. Now it's more common. Still makes many mathematicians unhappy.
Sure it is. But the system cannot contain infinities or real numbers of infinite precision. The halting problem for deterministic computers with finite memory is solveable - the system must either halt or repeat a state, and if it repeats a state, it's in an endless loop. Yes, the number of states may be very large, but not infinite.
An interesting question to ask is "do we need infinities". In a sense, infinities are a convenience feature to make formulas simpler. Without infinities, everything has edge cases, bounds problems, tolerances, and all the annoyances known to people who do serious computer number-crunching. Theory in that area has lots of case analysis.
It's perhaps unfortunate that Russell lived in the pre-computer era. Simple theorems were essential in the paper and pencil era. In the 1970s and 1980s, Boyer and Moore took on much the same problem as Principia Mathematica. They published "A Computational Logic"[1], and built the first good inductive theorem prover for constructive mathematics. (I used it back then, and a few years ago I got it running again on Common LISP and put it on Github, so you can still run it.[2]) Proofs that come out of that thing have lots of case analysis. Mathematicians used to hate proofs like that. Many still do.
At one point Boyer and Moore formalized what a floating point unit does, and this was used to verify an AMD floating point unit. This followed an embarrassing recall of Intel CPUs that were slightly off on division, and was paid for by AMD. It's a huge, ugly problem to formalize, compared to the ordinary rules for real arithmetic. It is, however, a system in which every true statement you care about can be proved.
The proof of the four-color theorem shook up the field. Thousands of cases. A simple problem with a huge proof that required machine assistance was a new thing back then. Now it's more common. Still makes many mathematicians unhappy.
[1] https://www.cs.utexas.edu/users/boyer/acl.pdf [2] https://github.com/John-Nagle/nqthm