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
