[HN Gopher] The complete story of Godel incompleteness
___________________________________________________________________
The complete story of Godel incompleteness
Author : herodotus
Score : 19 points
Date : 2024-03-11 14:33 UTC (1 days ago)
(HTM) web link (billwadge.com)
(TXT) w3m dump (billwadge.com)
| 082349872349872 wrote:
| > _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 )
| nyrikki wrote:
| > With a little more effort we can establish the same for any
| enumerable set of axioms.
|
| This is a case of presentism, which due to the work of Godel 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 Godels (in) completeness theorems.
| hackandthink wrote:
| "Before this, logic had been strictly syntactical and proof
| theoretic"
|
| Frege disagrees:
|
| "Just as the concept point belongs to geometry, so logic, too,
| has its own concepts and relations; and it is only in virtue of
| this that it can have a content. Toward what is thus proper to
| it, its relation is not at all formal."
|
| https://plato.stanford.edu/entries/frege/#FreConLog
___________________________________________________________________
(page generated 2024-03-12 23:00 UTC)