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)
> -----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 ...
> 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
> >>only generate "thoughts" which are sentences derivable from some
> >>axioms (and therefore can only generate "true" thoughts) is unable
> >>This is based on the fact that a formal system can't understand
> >>written down within that formal system (forgive me if I've worded
> >>Somehow we would need to support free parameters within quoted
> >>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
> >>general way. If it can, does this eliminate the need for a meta-
> >>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.
> >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
> >doing some useful higher-order
> >logic reasoning on its own, for certain kinds of problem domains