Bluntly,
looks to be almost exactly wrong. We can, and do, have consistency, but not completeness. But incompleteness is a glory; what can be said mathematically will always be more than what can be proved; so mathematicians will never be out of work.
Bits of my post disappeared - multiple windows, perhaps.
Here’s a paper by Vaananen on Second order logic and Foundations of Mathematics. It has more detail on his ideas of the power of expression. One direction of recent work has been towards using second order logic as a foundation for maths, as an alternative to set theory. The paper appears to be saying that Second Order Logic is itself dependent on set theory, somewhat surreptitiously, and so doesn’t help as much as might have been supposed.
Well beyond my ken. But our logicians are absent without leave. There’s a play on the difference between formal and informal arguments in the article that might be reflected in the exposition in the OP’s article.
Basically agree, a glory, and Chaitin sees it this way. My understanding is that “we” can’t prove consistency in systems like ZFC. Not saying we need to.
Personally I don’t care much about set theory. I was trained to use it in writing proofs, and it has some advantages as a language, but I find the numerical/computational core of mathematics more solid than what would prop it up.
Very meta.
I think maybe he is thinking in terms of later related findings, Lindstrom’s Theorem, etc., and so it’s not a total non-sequitur, it just isn’t explained very well (probably for brevity)?