**From:** Jeff Medina (*analyticphilosophy@gmail.com*)

**Date:** Thu Oct 21 2004 - 06:57:47 MDT

**Next message:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Previous message:**Christian Szegedy: "Re: [agi] A difficulty with AI reflectivity"**In reply to:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Next in thread:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

"For example, suppose that we start with a Godel Machine that,

meta-level aside, starts with an object-level program that repeatedly

presses a button delivering the equivalent of a nasty electrical

shock. If the meta-level speeds up the object level so that we get

nasty electrical shocks twice as fast, this is not an expected utility

improvement."

In your analogy, "pushing a button that produces nasty electrical

shocks" is meant to correspond to "proving theorems", and is bad

(results in a net utility loss), and is meant to be plausible because

the theorem-proving our theorem-proving machine is doing may be

fundamentally unsound (in that it may be proving some theorems true

that are actually false.) Correct?

If so, then your problem arises without introducing the possibility of

our rewriting its own theorem-prover. Specifically, if one can solve

the current problem (roughly, "How can we prove that a new

theorem-prover is an improvement, when that theorem-prover might be

wrongly proving falsehoods to be truths (pushing the electric shock

button)?") then one can also solve the problem "How can we prove that

our original theorem-prover's proofs correspond to (and only to) true

propositions?"

We can't expect to prove that a theorem-prover's proofs correspond to

(and only to) true propositions, on pain of infinite regress (because

we can always question the fallibility of the meta-theorem-prover we

decided to use to prove the truth-correspondence of the object-level

theorem-prover).

So the answer is, as you mentioned in passing, that we must assume, at

some level, correctness of our proof theory, even though the level at

which we make said assumption might be the proof-theoretic equivalent

of jabbing red zappy buttons in an unfortunate, catastrophe-birthing

manner. Our theorem-proving machine can only ever hope to rewrite its

theorem-prover with a performance-level improvement, not a

truth-correspondence-level improvement (other than accidentally, that

is).

You won't ever find anything in the literature on how to prove that a

system of proof is infallibily truth-producing outside of the context

of said system of proof (or even how to prove that system-of-proof A

is more consistently truth-producing than system-of-proof B; not

outside of the context of system-of-proof A, B, or X) because even if

someone were to come up with something that looked like a proof that

"wraps around" as you put it, they (or the journal editors/referees)

would reject it as unsound, due to a reductio ad absurdum. Namely,

because it would contradict that which the rest of proof theory claims

is true; that wrap around is impossible -- truth is forever uncertain

at its base. We cannot avoid inserting potentially unsound

assumptions.

**Next message:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Previous message:**Christian Szegedy: "Re: [agi] A difficulty with AI reflectivity"**In reply to:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Next in thread:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Michael Roy Ames: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Reply:**Eliezer Yudkowsky: "Re: [agi] A difficulty with AI reflectivity"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

*
This archive was generated by hypermail 2.1.5
: Wed Jul 17 2013 - 04:00:49 MDT
*