Quote: " ... this provides a foundation which ensures the computer can check any series of logical statements to confirm they are true." (emphasis added)
Not really. I wonder if the author of the linked article realizes that the Turing Halting Problem, and Gödel's incompleteness theorems, are deeply connected and prevent the claimed outcome as stated.
1. Checking a series of logical statements (a proof) is obviously decidable; it's a mere exercise in syntactic manipulation. This is exactly what Isabelle/HOL/Coq/Agda/etc. do.
2. Yes, the validity of theorems is undecidable. But even if that's what the quote was talking about (it's not, read the context), confirming truth (soundness) is very much something computers are capable of. Correctly deciding truth or falsity (soundness + completeness) is what is not possible in every case.
The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement. Compared to most reporting on technical subjects, this reporting was wonderful.
> The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement.
Checking a series of logical statements, and generating a series of logical statements, are not fundamentally different with respect to the issue of undecidability.
> Compared to most reporting on technical subjects, this reporting was wonderful.
Until I got to the passage I quoted, I agreed completely, and I agree in general in spite of it. It's one of those often-heard statements that make more experienced readers say, "Umm, wait, you really don't want to say it that way."
Checking a series of logical statements is just arithmetic.
Generating a series of logical statements is only hard because the formal statements are not generated axiomatically, they are sourced from ill-understood human creativity. Once a formalism is defined it is trivial O(e^n) algorithm to generate all proofs of size n.
Not really. I wonder if the author of the linked article realizes that the Turing Halting Problem, and Gödel's incompleteness theorems, are deeply connected and prevent the claimed outcome as stated.