> If we allow experimental evidence
That's a remarkably big if. (Consider the history of the parallel postulate: https://en.wikipedia.org/wiki/Parallel_postulate#History )
That's a remarkably big if. (Consider the history of the parallel postulate: https://en.wikipedia.org/wiki/Parallel_postulate#History )
This is a case of presentism, which due to the work of Gödel we accept the costs of the implications of his findings.
RE is semi-decidable, meaning we can find yes-instances, although some yes-instances may be false.
RE+co-RE=R, when the author is only referencing RE.
Failure as negation does have its place but it also is what will probably block strong-AI.
Also note that presburger arithmetic, FoL with (+,=) or (*,=) is fully decidable. But proofs require double exponential time. Superfactorial time isn't practical.
Same with attention in feed forward networks requiring exponential time with a reduction in expressability.
This is a lower bound for negation through exhaustion in zero order logic through the strong exponential time theorem.
The loss of reliable negation: (¬) in all but the weakest logic forms in the general case has huge practical implications for all but the most trivial problems.
Unless you are lucky enough to have a fully decidable model aka recursive, the costs are high.
PA was shown to be consistent with transfinite induction BTW. But that is because the natural numbers are well ordered.
But transformers with soft attention being limited to solving problems in TC^0 with failure as negation is a very real cost of Gödels (in) completeness theorems.
Specifically, for all practical purpose, it is sufficient to have probabilistic guarantees. Suppose an AI is able to generate mathematical proofs as well as humans, it wouldn't really matter if in theory "they are limited to solving problems in TC^0 with failure as negation"
LTSM is much more powerful.
Interesting, could you please explain more on this?
Consider strong negation:
Did Homer write the Iliad? No, he did not.
VS a too computationally expensive system with true,false,other with no knowledge of Homer:
Did Homer write the Iliad? No, Homer did not exist.
Vs negation as failure of binary threshold ANNs:
Did Homer write the Iliad? No.
Transformers explicitly can find known unknowns, unknowable unknowns (eg future unknowns), etc..
But exhaustive unknowns may or may not be valid.
There is a lot more to it, but strong AI requires universal quantification, ML is existential quantification.
The above is just one way to think about why Word sense disambiguation and ATP are though to be AI-complete.
Huh? Can you say more about that? What takes exponential time with transformers?
https://proceedings.mlr.press/v201/duman-keles23a/duman-kele...
I acknowledge that they related this to the assumption of the SETH (which surprises me a little). But, this doesn't mean that transformers take exponential time. I don't think I understood what you meant by the "with a reduction in expressability" part of the statement, so maybe that is the reason behind me not following.
Still, the outcome is probably roughly the same. We'd replace the inconsistent axiom with something similar and 99.99% of existing practical math would still follow, and only a few intentionally specious constructions would fail. (It kind of begs the question of whether math follows from the axioms we want or axioms follow from the math we want). Plus perhaps some new math would start to unfold as we begin to explore the inconsistent axiom's subtleties.
Only tangentially related, but the same idea comes to mind reading Terence Tao's masterpiece on "Smoothed asymptotics" for divergent infinite sums (e.g. the infamous 1+2+3+4+… = -1/12):
https://terrytao.wordpress.com/2010/04/10/the-euler-maclauri...
Our intuitive interpretation (Σn must be infinite! and surely positive! never -1/12) fails miserably for such infinite series, in the sense that "practical experiments" (QM) hint at reality preferring that bizarro -1/12 interpretation instead. Who is at fault here – our seemingly iron-clad intuition or the experiments? And why the disconnect?
Like you say, what new math unfolds once we accept and internalize this new interpretation and adjust our intuition? Tao's piece offers an excellent basis for that. While we may come up with any interpretations and axioms we like, experiment is the final arbiter on which of these "math worlds" are real.