I wonder if it is possible for an AI to eventually try to prove currently unprovable theorems by producing it’s own formal system? I don’t know enough about Godels Theorems or ML to know if this is even possible.
You end up with a tower of “universes” that each have some statements they can’t prove which are provable in a higher universe.
You might wonder about the limit… but axioms are only interesting when finite: if you have infinite axioms, just assume the true statements.
You might wonder which those are… but then you’re confronted with the fact it’s all made up and you can have consistent systems from contrary axioms, eg either allowing or disallowing choice.
Mathematics is useful because it gives us a language to tell stories where we can accurately guess questions like “what came before?” or “what happens next?” and where we can describe similarities between stories.
Godel's theorem applies to all systems strong enough to do arithmetic. When we talk about "powerful" systems, it will inevitably have to do arithmetic.
One of the unprovable statements of any such formal system will be that "this system is consistent", which is an important property. [Godel's second incompleteness theorem]
I feel that AI in general is headed towards the direction of saying that provability is not really important, let's just head in a pragmatic direction.
Prior to Euclid people seemed to be concerned with valid arguments. Mathematical proofs are limited to true or false statements. Math is great when modeling physics, but quite lacking when applied to other human endeavours.
I don't think its useful to refer to every symbolic structure that people employ to build machines as "math." There is more to Facebook and Midjourney than the equations used to represent their operation.
Nonsensical is better in modern discussions than "unprovable".
It shows that statements that were previously (and currently by some) thought to be mathematical are actually nonsense just like "x tastes like chicken" but more devious.
Asking if a Turing machine with M memory halts in less than N steps is sane and provable.
> Did Gödel Really Prove That There Exist True yet Unprovable Statements?
> Of course not! All his “statements” were meaningless!
> Every statement that starts : “for every integer n . . .” or “there exists an integer n . . .”, is completely meaningless, since it tacitly assumes that there are infinitely many integers. Of course, there are only finitely many of them, since our worlds, both the physical and the mathematical, are finite.
..
> The statement “n + n = 2n for every integer n” is meaningless. It is only true for every _finite_ integer. It is also true for symbolic n.
I wonder if it is possible for an AI to eventually try to prove currently unprovable theorems by producing it’s own formal system? I don’t know enough about Godels Theorems or ML to know if this is even possible.