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:marchal.domain.name.hidden]
> Sent: Tuesday, 20 January 2004 6:44 PM
> To: everything-list.domain.name.hidden
> 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
Received on Tue Jan 20 2004 - 20:20:55 PST