3 ms·

By "all this", I assume you mean the work of first Lucas, and then Penrose, in using Gödel's disjunction to argue against Strong AI [1]. This argument cannot be

By "all this", I assume you mean the work of first Lucas, and then Penrose, in using Gödel's disjunction to argue against Strong AI [1]. This argument cannot be dismissed simply by noting that humans are often inconsistent, and it is not plausible that people of the intellectual stature of Lucas and Penrose would make so simple an error. What these arguments claim is that if a digital computer could emulate a human mind, then the human mind is ultimately algorithmic (so there is an algorithm that can produce all the theorems that the human mind is capable of producing.) The Church-Turing thesis says that every algorithmically computable function is computable with a Turing machine. This is equivalent to the proposition that the collection of humanly knowable theorems can be recursively axiomatized in some formal theory T. This theory would then be consistent [2]. Given that this hypothetical system is consistent, it has at least one Gödel sentence: a true statement which cannot be proven from within the system. Lucas and Penrose assert, however, that humans could see its truth by "stepping outside of the system", as they do, for example, in proving the consistency of Peano arithmetic. Therefore, there would be at least one thing that a human mind could do, but which its supposedly equivalent digital computer could not. So Lucas and Penrose are not assuming that humans are consistent; on the contrary, they are saying that Strong AI proponents themselves are implying that minds are reducible to a consistent formal theory. As Lucas and Penrose do not accept the Strong AI premise, they are not making this implication, and they do not have to reconcile it with the observed inconsistency of humans - that is, as it were, left as an exercise for Strong AI proponents to solve (this, however, is not the crux of their argument, which concerns deducing the truth of the implied system's Gödel sentence, as outlined above.) I believe these arguments can be plausibly challenged, but not by anything so simple as observing that humans are inconsistent. [1] https://iep.utm.edu/lp-argue/ https://iep.utm.edu/lp-argue/ [2] https://www.maa.org/press/maa-reviews/g-dels-disjunction https://www.maa.org/press/maa-reviews/g-dels-disjunction

simonh 5y ago
Ive never heard of Peano arithmetic before and I'm not a logician or mathematician, so I'll rely on wikipedia for what it's worth: "Whether or not Gentzen's proof meets the requirements Hilbert envisioned is unclear: there is no generally accepted definition of exactly what is meant by a finitistic proof, and Hilbert himself never gave a precise definition. The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, relying either on intuition or the acceptance of a consistency proof such as Gentzen's proof. A small number of philosophers and mathematicians, some of whom also advocate ultrafinitism, reject Peano's axioms because accepting the axioms amounts to accepting the infinite collection of natural numbers." - Me again - Frankly that doesn't seem to me to be a case of stepping out of anything to prove it. All they did was expand the set of axioms to include an additional set that allowed the construction of a separate proof, but that still leaves you in the same position you started in because you can't prove the new expanded system in terms of it's aggregate axioms either. In fact it seems we don't even have a clear definition of what a finitistic proof even is. I see no reason why an algorithmic system couldn't engage in such games.
- mannykannot 5y ago
  Lucas himself foresaw the 'expand the axioms' response, and pointed out that once you do this, you get a new formal system with a new Gödel sentence. This means that no such argument against his thesis - i.e. by adding the truth of the formal system's Gödel sentence to that system's axioms - will terminate. Note that I am not saying the Lucas-Penrose argument is indefeasible; I am saying that it cannot be defeated simply by the argument that goes 1) it claims the human mind is consistent; 2) we can see that the human mind is not consistent; ergo, it is false. This argument fails because premise 1 is false. If it were this simple, the video here would not be nearly two hours long! Addendum: The "stepping out" argument is not a matter of adding axioms, it is a sort of meta-argument that a Gödel sentence for a consistent system must be true[1], and the consistency of the hypothetical system under discussion follows via the Church-Turing thesis (which you could challenge if you want to, but I suspect that, to most people who understand the implications of doing so, this would be an undesirable trade of one implausibility for another.) This leaves me wondering if the Lucas-Penrose argument can be challenged on the grounds that the algorithm in question probably does not halt (other than for causes outside the system; namely, the causes of death or the causes of a power outage), or that the question of its halting is undecidable. I am sure this response has been debated somewhere, if it is not obviously wrong. [1] https://math.stackexchange.com/questions/1491061/paradoxhow-can-godel-prove-that-godel-sentence-is-unprovable-but-true-if-such https://math.stackexchange.com/questions/1491061/paradoxhow-...
- mannykannot 5y ago
  Here's a quote that I think you may find interesting, as it seems to be along the lines of what you are saying: "A meta-mathematical proof of the consistency of arithmetic is not excluded by...Goedel's analysis. In point of fact, meta-mathematical proofs of the consistency of arithmetic have been constructed, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936. But such proofs are in a sense pointless if, as can be demonstrated, they employ rules of inference whose own consistency is as much open to doubt as is the formal consistency of arithmetic itself. Thus, Gentzen used the so-called "principle of transfinite mathematical induction" in his proof. But the principle in effect stipulates that a formula is derivable from an infinite class of premises. Its use therefore requires the employment of nonfinitistic meta - mathematical notions, and so raises once more the question which Hilbert's original program was intended to resolve." -Ernest Nagel and James Newman Taken from https://www.mathpages.com/home/kmath347/kmath347.htm https://www.mathpages.com/home/kmath347/kmath347.htm

simonh 5y ago

Ive never heard of Peano arithmetic before and I'm not a logician or mathematician, so I'll rely on wikipedia for what it's worth: "Whether or not Gentzen's proof meets the requirements Hilbert envisioned is unclear: there is no generally accepted definition of exactly what is meant by a finitistic proof, and Hilbert himself never gave a precise definition. The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, relying either on intuition or the acceptance of a consistency proof such as Gentzen's proof. A small number of philosophers and mathematicians, some of whom also advocate ultrafinitism, reject Peano's axioms because accepting the axioms amounts to accepting the infinite collection of natural numbers." - Me again - Frankly that doesn't seem to me to be a case of stepping out of anything to prove it. All they did was expand the set of axioms to include an additional set that allowed the construction of a separate proof, but that still leaves you in the same position you started in because you can't prove the new expanded system in terms of it's aggregate axioms either. In fact it seems we don't even have a clear definition of what a finitistic proof even is. I see no reason why an algorithmic system couldn't engage in such games.

mannykannot 5y ago
Lucas himself foresaw the 'expand the axioms' response, and pointed out that once you do this, you get a new formal system with a new Gödel sentence. This means that no such argument against his thesis - i.e. by adding the truth of the formal system's Gödel sentence to that system's axioms - will terminate. Note that I am not saying the Lucas-Penrose argument is indefeasible; I am saying that it cannot be defeated simply by the argument that goes 1) it claims the human mind is consistent; 2) we can see that the human mind is not consistent; ergo, it is false. This argument fails because premise 1 is false. If it were this simple, the video here would not be nearly two hours long! Addendum: The "stepping out" argument is not a matter of adding axioms, it is a sort of meta-argument that a Gödel sentence for a consistent system must be true[1], and the consistency of the hypothetical system under discussion follows via the Church-Turing thesis (which you could challenge if you want to, but I suspect that, to most people who understand the implications of doing so, this would be an undesirable trade of one implausibility for another.) This leaves me wondering if the Lucas-Penrose argument can be challenged on the grounds that the algorithm in question probably does not halt (other than for causes outside the system; namely, the causes of death or the causes of a power outage), or that the question of its halting is undecidable. I am sure this response has been debated somewhere, if it is not obviously wrong. [1] https://math.stackexchange.com/questions/1491061/paradoxhow-can-godel-prove-that-godel-sentence-is-unprovable-but-true-if-such https://math.stackexchange.com/questions/1491061/paradoxhow-...
mannykannot 5y ago
Here's a quote that I think you may find interesting, as it seems to be along the lines of what you are saying: "A meta-mathematical proof of the consistency of arithmetic is not excluded by...Goedel's analysis. In point of fact, meta-mathematical proofs of the consistency of arithmetic have been constructed, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936. But such proofs are in a sense pointless if, as can be demonstrated, they employ rules of inference whose own consistency is as much open to doubt as is the formal consistency of arithmetic itself. Thus, Gentzen used the so-called "principle of transfinite mathematical induction" in his proof. But the principle in effect stipulates that a formula is derivable from an infinite class of premises. Its use therefore requires the employment of nonfinitistic meta - mathematical notions, and so raises once more the question which Hilbert's original program was intended to resolve." -Ernest Nagel and James Newman Taken from https://www.mathpages.com/home/kmath347/kmath347.htm https://www.mathpages.com/home/kmath347/kmath347.htm