- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: David Barrett-Lennard <dbl.domain.name.hidden>

Date: Wed, 21 Jan 2004 09:18:42 +0800

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

Date: Wed, 21 Jan 2004 09:18:42 +0800

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

;-)

that

to

this

systems

anyway.

Received on Tue Jan 20 2004 - 20:20:55 PST

*
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:09 PST
*