   Godel's Incompleteness Theorems and Mind
  A thread birthed from the Dinosaur and Evangelism.Quote:Original post by DmytryQuote:Original post by DaeraxQuote:Original post by DmytryBTW, consider this. If you "formally prove" some statement, there's always chance of screwup, and there is chance of screwup on check, and no matter how many checks you do, no matter how macroscopic your machine is, the chance won't be zero. Essentially, formal proofs don't really exist in this universe. Some statements are very likely to be true (practically true) and some are very unlikely (practically false).I suppose. But that is the least of concerns and likely wont surface the same way in all machines and or brains if at all. Consistency across all should be sufficient and is all that we can have. Anyways formal proofs more means mechanically traceable and consitent with axioms and wffs than infalliability.This bring question: If humans construct some quantum mechanical thing that answers whever proof exist or not (with good enough probability), and capable of answering things that normal proving can not, would that be acceptable?This thing would not be a formal system or one whose operation was algorithmic - it likely would not be constructed but instead with functionality that was evolved and whose root behaviour would be just as, if not more alien to us than we are to ourselves (too complex). But I did not answer your question and I cannot since we do not know enough to even posit on the possibility of such a thing. But if we can make thousands whose results did not differ across centuries then why not? Why specific mention of quantum mechincal? Everthing is quantum mechanical at enough depth.Quote:Quote:Quote:Brain: if brain works by physics laws, would you consider it "formal system"?Not necessarily. In fact, IMHO, likely no. That is Physical Laws or Not is not sufficient for formal system true.What i meant is that if brain is governed by classic physics laws as we know them, any conclusion that brain makes can be achieved with many mechanical steps in simulation. That's how you defined "formal".Though there's some randomness in the brain. But mechanical systems can be very good at simulating randomness.What is mechanical? Dont bother, that was a rhetorical question. Nonetheless when I think on the nature of proofs in a formal system I think: thoughtlessly, mechanically traceable - algorithmic in action. We operate heuristically so I feel that in support of the fact that we are more than simply machines. The ability to operate on non computable functions is another. Indeed we can easily break Godel's 1st ICT. Since there will be things I could prove that a mechanical system supposed to model or emulate my brain could not. Nonetheless we can do mechanical tasks as well and may well be truly mechanical in action which in fact would, assuming that we can do more than any machine meant to do what we do :D,  invalidate the Church turing thesis. Since it would be false that any given computable function can be computed by a turing machine. Quote:Quote:Quote:If brain would be good at solving halting problem, we could argue it is something greater than 'turing machine with rng' and that classic computer can't ever have mind. (like, human are given initial state and rules and must tell if it will ever halt. What is more insteresting is the veracity of the Church turing thesis in the first place when considering it, the human brain and G's 1st Theorem together. We know that human can make Godel's theorem(s), it is not really certain whever computer (with random numbers) can make it with good probability, but there's really no reason to conclude it can not.Consider computer whose task is to make maximally convincing argument(proof). It doesn't have to be 'consistent' in it's argumentation or something like that.I believe that such computer can find these theorems about natural numbers, even though this computer will have trouble applying similar argumentation to itself and it's own internal mechanics. Kind of like human, you can reason without trouble about self reference in some other system, but if it is self reference to yourself, it becomes "paradox".Im not quite sure what you mean there but there is no gurantee that in some randomly given formal system that it will not eventually generate theorems that were the same as Godel's.  I think, I dont know much proof theory yet. :)Quote:Quote:Quote:edit: There does exist valid answer to the question i asked, "I ask you whever you will answer this question negatively (negatively as in no, nope, not)." (where, "this question" refers to that question itself).  The answer is: No, you didn't answer this question negatively. [grin]Hmm, it seems you are discussing paradoxes generated in self referential statements.Godel's first theorem is actually based on sort of such "paradox". There's more info on how it is constructed mathematicallyThis is indeed complicated at details (at how "can be proved" is formally expressed with numbers), but deeply inside it has self reference. Possibly inspired by other self reference "paradoxes". It is not really paradoxes, it is self contradictions / inconsistency of statements like "this statement is false".Indeed, that is very true. But just because you can generate a paradox in a self referential system - one outside the scope of applicability of Godels ICTs mind you - does not mean that the theorems apply to them. They are just similar in a basic manner, conceptually. Godels ICTs are not of universal applicability, they only apply to a specific axiomatic type of system and you cannot rigorously claim that its results apply even more generally.   
  It is easy to make theorem prover with some weird logic or few self-contradicting axioms or maybe some bug like buffer overflow. Or prover that misunderstand the axioms or theorems. So that starting from axioms the prover proves theorems ABC and starting from theorem A and B prover proves ~C . If it is deterministic, in some very deep abstract sense it is consistent inside, but the result that it gives is not consistent, and Godel's first theorem obviously shouldn't apply to whatever proofs it will make. Only something conceptually similar may apply. You're discussing minds and machines, that's why i thought you were talking about self references for machines, similar to to Godel's first theorem. And this prover's behavior is not that different from what humans often do. There's nothing impossible about having some AI who don't believe he is equivalent to turing machine, and who, to support his belief, "proves" that X="machine can't prove X" is true.Quote:Nonetheless when I think on the nature of proofs in a formal system I think: thoughtlessly, mechanically traceable - algorithmic in action. We operate heuristically so I feel that in support of the fact that we are more than simply machines. The ability to operate on non computable functions is another. Indeed we can easily break Godel's 1st ICT.Well. Godel's first theorem definately isn't a proof that machines can't find Godel's first theorem(as is) and see it true.I think you simply misinterpret something. Probably you misinterpret the mechanical proving process (using first order logic, giving always consistent results, etc) for machines in general. Also:a: Godel himself would want and tried to prove that humans are greater than machines,b: Godel know his theorems better than you or me or philosophers do.c: Godel has only arrived at conclusion that "(a) the human mind is not a consistent finite machine, or (b) there exist Diophantine equations for which it cannot decide whether solutions exist". (as about b, there do exist infinitely many Diophantine equations that hasn't been solved yet[lol].)I think the main philosophical implication of Godel's first theorem, halting problem and such is that those of philosophers who believe that human can solve everything will now believe human mind can do things that is impossible to do mechanically (something that hasn't been at all demonstrated so far). And will often construct inconsistent arguments to support this idea. (see Godel's second theorem hehe. it's relevant to consistency of belief that humans can prove everything)It would be better to discuss halting problem IMO, because it is actually applicable to any machines (unlike original Godel's theorems. The self reference contradiction similar to Godel's theorem can be considered equally applicable to machines or minds, and the original one is equally unapplicable.).Also, there's discussion of some argument[Edited by - Dmytry on June 13, 2006 6:59:52 AM];Quote:Original post by DaeraxIndeed, that is very true. But just because you can generate a paradox in a self referential system - one outside the scope of applicability of Godels ICTs mind you - does not mean that the theorems apply to them. They are just similar in a basic manner, conceptually. Godels ICTs are not of universal applicability, they only apply to a specific axiomatic type of system and you cannot rigorously claim that its results apply even more generally.What i mean is merely that Godel's theorem is related to the minds(in general) in exactly same way as to machines(in general). As self reference contradiction, that is.  The point is not really that "Godel's theorem" applies to something. If you take it in it's exact formulation, it doesn't apply to machines either and should be considered irrelevant to discussion whever mind is more than machine or not.The point, there is self-referential statement that has answer, but can't be answered by system that is self-referenced without making self contradiction. It is fundamental, it's not something that human mind or machine can violate somehow.   ;  I never opened the bible and dinosaurs thread, because I knew it would become a lengthy religion discussion from the start. I was right, because the thread is still alive and kicking on the front page with more pages every day.And now I got tricked into the discussion anyway by opening another thread with a different topic as disguise :(   ;Quote:Original post by DmytryIt is easy to make theorem prover with some weird logic or few self-contradicting axioms or maybe some bug like buffer overflow. Or prover that misunderstand the axioms or theorems. So that starting from axioms the prover proves theorems ABC and starting from theorem A and B prover proves ~C . If it is deterministic, in some very deep abstract sense it is consistent inside, but the result that it gives is not consistent, and Godel's first theorem obviously shouldn't apply to whatever proofs it will make. Only something conceptually similar may apply. You're discussing minds and machines, that's why i thought you were talking about self references for machines, similar to to Godel's first theorem. And this prover's behavior is not that different from what humans often do. There's nothing impossible about having some AI who don't believe he is equivalent to turing machine, and who, to support his belief, "proves" that X="machine can't prove X" is true.Indeed, that is why for now, I am skeptical of provers and am more interested in verifiers. As to what I was talking about...I dont remember but it was not about self referencing for machines or humans. I think i was just discussing Godel in general and some implications. Quote:Quote:Nonetheless when I think on the nature of proofs in a formal system I think: thoughtlessly, mechanically traceable - algorithmic in action. We operate heuristically so I feel that in support of the fact that we are more than simply machines. The ability to operate on non computable functions is another. Indeed we can easily break Godel's 1st ICT.Well. Godel's first theorem definately isn't a proof that machines can't find Godel's first theorem(as is) and see it true.I think you simply misinterpret something. Probably you misinterpret the mechanical proving process (using first order logic, giving always consistent results, etc) for machines in general. You misunderstand me, because I do believe that a machine could find Godel theorems. That is why I said in the first post: "there is no gurantee that in some randomly given formal system that it will not eventually generate theorems that were the same as Godel's.". Basically, I agree that some machine, given suitable wffs and inference may eventually output Godel's Theorems.Quote:Also:a: Godel himself would want and tried to prove that humans are greater than machines,b: Godel know his theorems better than you or me or philosophers do.c: Godel has only arrived at conclusion that "(a) the human mind is not a consistent finite machine, or (b) there exist Diophantine equations for which it cannot decide whether solutions exist". (as about b, there do exist infinitely many Diophantine equations that hasn't been solved yet[lol].)I think humans are greater than machines too. :D Again I quote myself: "We operate heuristically so I feel that in support of the fact that we are *more* than simply machines. The ability to operate on non computable functions is another."Quote:I think the main philosophical implication of Godel's first theorem, halting problem and such is that those of philosophers who believe that human can solve everything will now believe human mind can do things that is impossible to do mechanically (something that hasn't been at all demonstrated so far). And will often construct inconsistent arguments to support this idea. (see Godel's second theorem hehe. it's relevant to consistency of belief that humans can prove everything)I also think with regards to the first theorem (and assuming applicability) that there lie implications as to us being ever able to understand fully how our brains, how we work; and assuming we are consistent we can never know if our inherent logic, the root of our logic, our math, our science is solid, if we are truly sane. But really, I dont think Godel's theorem apply to us. At least not entirely. Quote:It would be better to discuss halting problem IMO, because it is actually applicable to any machines (unlike original Godel's theorems. The self reference contradiction similar to Godel's theorem can be considered equally applicable to machines or minds, and the original one is equally unapplicable.).Also, there's discussion of some argumentOkay, but I am not so confident about Turing as I am with Godel so I will have to do some extra reading. With regards to the halting problem though, I think you would have to first consider if the concept of universality across turing machines is not a broken one. Indeed, your link was what I was hinting at when I stated: "Nonetheless we can do mechanical tasks as well and may well be truly mechanical in action which in fact would, assuming that we can do more than any machine meant to do what we do :D, invalidate the Church turing thesis. Since it would be false that any given computable function can be computed by a turing machine."There is absolutely no reason to believe that we are less than or equivalent to machines. But then, there is no reason to believe Godel applies straight to us either. You need both to speculate on the mind machine relation. To be able to apply halting on human is to imply Godel as well applies (with all the baggage it brings) which would in turn allow one to show that the mind is not a machine, so turing does not apply...assuming consistency and you are not one of those 'brain is a computing machine' obsessed zealots, of course. :D   ;  Something intersting and related that Ive encountered and been meaning to read about is the theory of Hypercomputation.;  Well, the question boils down to whever there is hypercomputation in "human mind", or there isn't. If there is hypercomputation, human can do things that machine can't possibly ever do. If there is no hypercomputation, anything that can be done by human can be done by computer (with access to random numbers). Computer would need enormous power, though (on order of 1016 operations per second to simulate brain, possibly some orders of magnitude less if optimized), so it won't happen until at least 2030.So far there has been no evidence for hypercomputation in the human mind (and it seems we agree that humans proving Godel's theorem is no evidence for hypercomputation). So far, with all evidence, human mind should be considered as result of physical interactions in the brain.You can believe in hypercomputation-in-the-brain, or believe in soul, or believe in solipsism, or whatever else, but that is not science. These things is all non-falsifiabe.As for Turing machines and halting problem, the idea is that if you have for example black box that somehow, for any turing machine with any initial state, correctly tells if this machine ever halt [btw in general we won't even be able to verify it is correct! lol.], then the black box can't possibly be emulated by computer. Clearly, human mind is not really an example of such black box.   ;Quote:Original post by Daerax[...]Indeed, that is why for now, I am skeptical of provers and am more interested in verifiers.[...]MetaMath.orgQuote:[...]I do believe that a machine could find Godel theorems.[...]Interestingly, a machine that explores an axiomatic system cannot find Godel's theorems (or anything equivalent) unless the system it is exploring is inconsistent, because finding a theorem (starting from axioms/axiom schemas and advancing using theorems/theorem schemas) is equivalent to 'proving' it true in that system.Of course, such a machine is likely to be given a 'meta' layer or N with which to examine the axiomatic system, in which case it could possibly find such theorems.   ;Quote:Original post by ExtrariusQuote:Original post by Daerax[...]Indeed, that is why for now, I am skeptical of provers and am more interested in verifiers.[...]MetaMath.orgFundamentally, verifier is equvalent to prover (take all possible strings, use verifier to select ones that is correct theorems)Quote:Quote:[...]I do believe that a machine could find Godel theorems.[...]Interestingly, a machine that explores an axiometric system cannot find Godel's theorems unless the system it is exploring is inconsistent, because finding a theorem (starting from axioms/axiom schemas and advancing using theorems/theorem schemas) is equivalent to 'proving' it true in that system.Well, actually that isn't strictly true, if you use logic that is more powerful than logic of system for which you want to prove Godel's theorem, you can prove Godel's theorem for that less powerful system. Or consider machine that doesn't actually explore axiomatic system, but tries to make maximally "convincing" and "logical" argument.   ;Quote:Original post by ExtrariusQuote:Original post by Daerax[...]Indeed, that is why for now, I am skeptical of provers and am more interested in verifiers.[...]MetaMath.orgAhh yes, Metamath. That little program has had a large impact on my view of math. Im implementing a stripped down implementation (with some minor syntatical changes) of that in F#. You may also want to check out the much more complex Mizar as well.Quote:Original post by DmytryQuote:Original post by ExtrariusQuote:Original post by Daerax[...]Indeed, that is why for now, I am skeptical of provers and am more interested in verifiers.[...]MetaMath.orgFundamentally, verifier is equvalent to prover (take all possible strings, use verifier to select ones that is correct theorems)No, actually. They could not be more different. Well fundementally that is. First keep in mind that for many systems Godels first theorem makes it impossible to mechanically decide if a theorem is correct or not. An automated prover is a fairly complex piece of work. In such one has wffs, inferences etc. which are then followed and applied to generate proofs of theorems. These proofs are often very large and difficult to decipher, coupled with the semantics in use and other required built in axioms and such, it becomes difficult to be sure that the code of the prover or even that the generated proof is correct and can be trusted. A verifier on the other hand may be devoid of anything, sometimes not even wffs. It is pure and uses simple pattern matching and substitution to check that a proof is correct. Provers generate and are complex to implement and understand generated proves. Verifiers simply check and store, archive.   