DavidCooper wrote:
Schol-R-LEA wrote:
The whole issue of 'undecidability' in Gödel's paper is regarding the ability to 'decide' a proposition within a given propositional calculus, not in any absolute terms.
If a propositional calculus allows irrational moves to be made, then it's fantasy mathematics rather than anything of relevance to the real world
Well, yes, and that was the point - that propositional calculi were a dead end for automatic theorem derivation, because they would all have that problem. The idea of a propositional calculus as a way to find all mathematical theorems by a purely mechanistic process, without also finding false positives, doesn't work. That's all Gödel's theorems really say on their own; they are about the limits to which formalization can be taken.
To put it in a way more familiar to most grammarians (and compiler developers), what they really say is that
syntax isn't semantics.
(Assuming you are talking about a 'sufficiently strong' language i.e., one which cannot be described in terms of a regular grammar, so ones requiring either a context-free or a context-sensitive grammar to describe. Regular languages are vacuous enough that they don't really carry any additional semantics unless you deliberately impose an interpretation in them, as you would when using one for, say, a regex parser.)
Do Gödel's theorems apply to any possible mathematics? Not directly, because there is nothing inherent to mathematical reasoning that requires a strictly formal approach. Does it necessarily apply to any mechanical system trying to work out mathematical problems? No, obviously not, since that would mean human brains - which are mechanical processes, so far as we know - couldn't figure out things such as, say, Gödel's theorems. It just means that that particular approach to it, doing it by a fixed set of rules
without applying any sort of external interpretation while applying the rules, leads to absurdities. Nothing more, nothing less.
(Assuming you could do that in the first place; as I said, part of what the paper the theorems were published in showed was that most logicians trying that weren't managing to avoid interpretation - indeed, the theorems themselves are based on showing the need for interpretation outside of the calculi.)
It doesn't even mean that propositional calculi don't have value in more constrained uses, just that they aren't a silver bullet for finding mathematical proofs flawlessly.
What bearing does it have on hard AI? No one knows, though honestly, I don't see any reason it would have any at all. But then, I am not convinced (as I joked earlier) that 'intelligence' actually is all that meaningful to begin with (yeah, yeah,
cogito ergo sum, but Descartes was pulling a bit of a fast one with that - one which fit his ulterior goal of divorcing philosophy, logic, and mathematics from religious doctrine - by not actually defining what 'esse' or 'cogitere' mean in his system). 'Intelligence' is, metaphorically, a necessary axiom for rational discussion rather than something which can be defined.
I am not convinced that we'd be able to overcome the limitations of our neurological structures when observing a self-aware system that is based on different underlying structures; that is, even if we could create an AI, what guarantee is there that we'd be able to tell that it
is an AI, if it thinks in ways which are radically different from the ways we do? The flaws in the Turing Test are pretty well known, and expecting
a priori that an AI could even meaningfully communicate with us (or conversely, that a system which appears to converse as we do actually is self-aware) is a pretty shaky assumption. I doubt that it would be possible to prove beyond a reasonable doubt that your AGI
is an AGI, even if it is one.
I won't even get into the question of whether creating a new sophont (by any means at all) is ethical or meaningful; suffice it to say that I refuse to have any children of my own.
Mind you, the other part which most people fixate on - undecidability - is not quite what it is usually described to be, either. Basically, it was merely a new tool in the mathematicians' arsenal, a method by which they could reason about reasoning; it showed that you could make proofs about whether a conjecture was
decidable (provable or disprovable), by presenting an argument about mathematical logic as a whole as it applied to the topic, even if you couldn't prove or disprove said conjecture directly (i.e., you night not have a way to prove or disprove something,
but you could at least figure out if a proof was
possible or not). Since mathematicians don't like being frustrated any more than anyone else does, this at least lets them drop fruitless lines of inquiry (e.g., the Halting Problem) ahead of time.
(The other practical effect of proving undecidability of a problem is to say that if you take a conjecture about the truth or falsity of something as an axiom - that is, if you say, "I haven't proven this yet, but here's what it would mean if I had" - and that conjecture is then shown to be undecidable, then the reasoning based on that conjecture is itself undecidable, and thus isn't really usable in mathematics except as a counterfactual; you can do it, but it won't lead anywhere. IOW, undecidability is contagious - any reasoning based on an undecidable proposition can't be used in a decidable proof.)
The point is that it is method of reasoning about mathematics
itself, rather than about any particular application of mathematics.
What I am trying to say is the real problem is that Gödel's theorems - what they mean, what they apply to, the supposed profundity of them - has been vastly misrepresented in the popular press, and even the ones who mostly get it right such as Hofstadter are generally misunderstood by those reading their works. So, Inigo Montoya gets the last word after all fnord.