Re: Are conscious beings always fallible?
How would they ever know that I wonder? Well let's see. I'm conscious and I'm not fallible. Therefore ;-) David Barrett-Lennard wrote: I'm wondering whether the following demonstrates that a computer that can only generate thoughts which are sentences derivable from some underlying axioms (and therefore can only generate true thoughts) is unable to think. This is based on the fact that a formal system can't understand sentences written down within that formal system (forgive me if I've worded this badly). Somehow we would need to support free parameters within quoted expressions. Eg to specify the rule It is a good idea to simplify x+0 to x It is not clear that language reflection can be supported in a completely general way. If it can, does this eliminate the need for a meta-language? How does this relate to the claim above? - David I don't see the problem with representing logical meta-language, and meta-metalanguage... etc if necessary in a computer. It's a bit tricky to get the semantics to work out correctly, I think, but there's nothing extra-computational about doing higher-order theorem proving. http://www.cl.cam.ac.uk/Research/HVG/HOL/ This is an example of an interactive (i.e. partly human-steered) higher-order thereom prover. I think with enough work someone could get one of these kind of systems doing some useful higher-order logic reasoning on its own, for certain kinds of problem domains anyway. Eric
Re: Are conscious beings always fallible?
I agree with you. Actually you can use the second recursion theorem of Kleene to collapse all the orders. This is easier in an untyped programming language like (pure) LISP than in a typed language, although some typed language have a primitive for handling untyped self-reference, like the primitive SELF in Smalltalk ... Bruno At 23:29 19/01/04 -0800, Eric Hawthorne wrote: How would they ever know that I wonder? Well let's see. I'm conscious and I'm not fallible. Therefore ;-) David Barrett-Lennard wrote: I'm wondering whether the following demonstrates that a computer that can only generate thoughts which are sentences derivable from some underlying axioms (and therefore can only generate true thoughts) is unable to think. This is based on the fact that a formal system can't understand sentences written down within that formal system (forgive me if I've worded this badly). Somehow we would need to support free parameters within quoted expressions. Eg to specify the rule It is a good idea to simplify x+0 to x It is not clear that language reflection can be supported in a completely general way. If it can, does this eliminate the need for a meta-language? How does this relate to the claim above? - David I don't see the problem with representing logical meta-language, and meta-metalanguage... etc if necessary in a computer. It's a bit tricky to get the semantics to work out correctly, I think, but there's nothing extra-computational about doing higher-order theorem proving. http://www.cl.cam.ac.uk/Research/HVG/HOL/ This is an example of an interactive (i.e. partly human-steered) higher-order thereom prover. I think with enough work someone could get one of these kind of systems doing some useful higher-order logic reasoning on its own, for certain kinds of problem domains anyway. Eric
RE: Are conscious beings always fallible?
Even if we utilize a language with reflection capability, do we still have an underlying problem with different levels of mathematical truth as indicated by the question of whether 3+4 equals 7? When an expression contains a sub-expression, don't we expect to be able to replace that sub-expression by an equivalent one? But deciding whether two expressions are equivalent depends on a particular perspective of mathematical truth. Btw I thought Smalltalk was weakly typed (can throw a message at any object regardless of type) - David -Original Message- From: Bruno Marchal [mailto:[EMAIL PROTECTED] Sent: Tuesday, 20 January 2004 6:44 PM To: [EMAIL PROTECTED] Subject: Re: Are conscious beings always fallible? I agree with you. Actually you can use the second recursion theorem of Kleene to collapse all the orders. This is easier in an untyped programming language like (pure) LISP than in a typed language, although some typed language have a primitive for handling untyped self-reference, like the primitive SELF in Smalltalk ... Bruno At 23:29 19/01/04 -0800, Eric Hawthorne wrote: How would they ever know that I wonder? Well let's see. I'm conscious and I'm not fallible. Therefore ;-) David Barrett-Lennard wrote: I'm wondering whether the following demonstrates that a computer that can only generate thoughts which are sentences derivable from some underlying axioms (and therefore can only generate true thoughts) is unable to think. This is based on the fact that a formal system can't understand sentences written down within that formal system (forgive me if I've worded this badly). Somehow we would need to support free parameters within quoted expressions. Eg to specify the rule It is a good idea to simplify x+0 to x It is not clear that language reflection can be supported in a completely general way. If it can, does this eliminate the need for a meta- language? How does this relate to the claim above? - David I don't see the problem with representing logical meta-language, and meta-metalanguage... etc if necessary in a computer. It's a bit tricky to get the semantics to work out correctly, I think, but there's nothing extra-computational about doing higher-order theorem proving. http://www.cl.cam.ac.uk/Research/HVG/HOL/ This is an example of an interactive (i.e. partly human-steered) higher-order thereom prover. I think with enough work someone could get one of these kind of systems doing some useful higher-order logic reasoning on its own, for certain kinds of problem domains anyway. Eric
