timtyler comments on AI cooperation in practice - Less Wrong

26 Post author: cousin_it 30 July 2010 04:21PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Sort By: Best

You are viewing a single comment's thread. Show more comments above.

Comment author: cousin_it 30 July 2010 05:29:01PM * 2 points [-]

The argument is admittedly sketchy, but I don't think it depends much on the implementation of "proves". Of course I'd want the proof system to hold the same properties that are used in the proof of Löb's Theorem, because my argument is almost an exact replica of that; but pretty much all proof systems actually used by people (apart from some extremely weak ones) satisfy these properties. And you're guaranteed not to become worse off if you make your proof system stronger while your opponent stays the same. That's a really big deal, if my argument is indeed correct.

About heat death: even though the two programs say they can iterate up to 3^^^3 or something, the actual time to cooperation will be much less, because the reasoning steps that I outlined are exactly the reasoning steps they'd need to stumble upon. Yes, that would make a proof of length 10000 or so (which would mean 2^10000 proofs tried), but a that's long way from 3^^^3. If the programs use some kind of heuristics to search for working proofs (but still guarantee that they will do the brute force search if heuristics fail), the proofs can be found quicker still.

Comment author: timtyler 30 July 2010 05:52:07PM 1 point [-]

Re: "apart from some extremely weak ones"

It does depend on the implementation - because it is relatively easy to imagine poor provers that result in a failure to understand and prove anything much. So, you would need to specify some constraints on the prover before you can make statements about what it outputs.

Comment author: fiddlemath 31 July 2010 01:23:43AM * 6 points [-]

timtyler: I think you're confused about how proof verifiers work. A proof verifier takes a proof as input, and verifies that the given proof is correct. It doesn't have to generate the proof itself, and it gets to assume that each step is some small, easily-checkable application from a finite set of axioms.

Put another way, if the proof you give a verifier makes a large leap in reasoning, then the verifier will just tell you that the proof is wrong. Moreover, by the formalization that we demand of those proofs, the proof is wrong.

So, the problem that proof verifiers solve is computable. So, we need only to assume that the proof verifier that these programs have is correctly implemented, we don't really need to know their internal details.

(If you already understand this, though, then I'm confused about your confusion. Could happen.)

[edit:] Actually, I think I might see the point you're making; we have to assume the theory the prover understands is rich enough to model stepwise program semantics. This probably should have been specified, but we can just assume it.

Comment author: timtyler comment score below threshold [+] (37 children)

Comment author: Vladimir_Nesov 31 July 2010 10:14:29AM * 5 points [-]

Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski's undefinability theorem is about complete theories of arithmetic.

Comment author: timtyler comment score below threshold [+] (14 children)

Comment author: JoshuaZ 31 July 2010 03:12:25PM * 4 points [-]

There is no such thing as a "complete theory of arithmetic" - see Godel's incompleteness theorems.

The above statement isn't true. What Godel's theorem says is that any effectively generatable theory which is strong enough to model PA is either incomplete or inconsistent. Effectively generatable for our purposes can be taken to mean that valid proofs in the system are enumerable and that there's a primitive recursive procedure to determine whether a given proof is valid.

If one removes the effectively generatable condition then one can easily produce a complete, consistent system. Consider for example the following system: Consider some lexicographic ordering of well-formed statements in the language of PA, and let S(i) be the ith statement in this list. Let P(0) be PA, and generate P(n) by asking whether S(n) or ~S(n) is a theorem in P(n-1). If so, then set P(n) = P(n-1). If not, then let P(n) be P(n-1) with the additional axiom of S(n). Now, consider P(infinity) defined as the union of all P(n). This theory is complete and consistent but it is very much not effectively generatable since we can't even recursively enumerate the system's axioms.

It might help for you to take a model theory or logic course since there are a lot of subtle issues here that you seem to be missing.

Comment author: timtyler comment score below threshold [+] (11 children)

Comment author: Vladimir_Nesov 31 July 2010 12:00:31PM 7 points [-]

Please give up.

Comment author: JoshuaZ 31 July 2010 01:40:11PM 4 points [-]

An automated proof-checker can identify some correct proofs - but not all of them.

That's a consequence of "Tarski's Undefinability of Truth Theorem":

No. That's not what Tarski's theorem says. Tarski's theorem is a statement about first-order arithmetic descriptions of truth (it can be generalized slightly beyond that but this is the easiest way of thinking about it). It asserts that there's no first-order description of what statements are true in a system that lies in the system.

Proof checking is a very different issue. Proof checking is straightforward. Indeed, most of the time we insist that axiomatic systems have proofs checkable as a primitive recursive function. We can do this in Peano Arithmetic for example, and in PA every proof can be verified by a straightforward algorithm.

Comment author: Vladimir_Nesov 31 July 2010 01:54:08PM * 0 points [-]

[Tarski's theorem] asserts that there's no first-order description of what statements are true in a system that lies in the system.

You'd need be careful about what "system" or "description" are you talking about, since you can weakly represent, say, the set of statements true in Robinson arithmetic (which is recursively enumerable), in Robinson arithmetic. There is a formula s(-) with one free variable such that

Q |- s(gn(f)) iff Q |- f

where gn(f) is the Gödel number of (arbitrary) statement f and Q is Robinson arithmetic.

Comment author: JoshuaZ 31 July 2010 02:01:32PM 1 point [-]

Yes, I know that. I was being deliberately imprecise because it is very easy in this case to get lost in the technical details. My intention was not to convey the theorem's precise statement but rather convey to Tim why it doesn't apply in the context he's trying to use it.

Comment author: Vladimir_Nesov 31 July 2010 02:04:24PM * 1 point [-]

I know you know that, but I couldn't quite naturally interpret your informal statement as saying the formally correct thing, so had to make the clarification.

Comment author: timtyler comment score below threshold [+] (4 children)

Comment author: JoshuaZ 31 July 2010 04:48:09PM 2 points [-]

Tim, please reread what I wrote. PA is an example. The relevant point is that Tarski's theorem doesn't say what you seem to think it says.

Comment author: timtyler comment score below threshold [+] (2 children)

Comment author: cousin_it 31 July 2010 08:53:08AM * 2 points [-]

The proof checker checks proofs within some formal theory. The Godel sentence for the checker is certainly true and provable by us, given the consistency of that formal theory. (If the theory were inconsistent, the checker would be able to prove any sentence.) But this doesn't work as a proof within the theory! The theory cannot believe its own consistency (Godel's second incompleteness theorem), so the checker cannot assume it when checking proofs. So your argument doesn't actually give an example of a valid proof rejected by the checker.

Comment author: Jonathan_Graehl 01 August 2010 07:51:53AM 2 points [-]

the checker would be able to prove any sentence

I think you mean that there would be some proof (that checks) for any sentence.

Comment author: cousin_it 01 August 2010 07:54:53AM 2 points [-]

Yes. Thanks.

Comment author: timtyler 31 July 2010 11:24:36AM * 0 points [-]

Let's say we are trying to prove statements within ZFC.

"ZFC can never prove this statement to be true"

...is one thing and...

"This proof checker can never prove this statement to be true"

...is another.

Neither can be proved by the specified proof checker - but the second statement can be proved by another, better proof checker - still working within ZFC - so it can be seen that it is true.

Comment author: Jonathan_Graehl 01 August 2010 07:49:29AM 2 points [-]

"proved by a proof checker" - huh?

Comment author: timtyler 01 August 2010 08:44:40AM -1 points [-]

"Asserted", "approved" - whatever.

Comment author: Vladimir_Nesov 01 August 2010 09:48:54AM * 0 points [-]

Worse, it's only "true" that a consistent theory is consistent in some unclear sense, because you can extend the theory with a statement that asserts inconsistency of the original theory, and the resulting theory will remain consistent.

Comment author: cousin_it 01 August 2010 10:20:13AM * 2 points [-]

What you're saying is certainly true (onlookers, see pages 5-6 of this pdf for as especially clear explanation), but I like to think that you can't actually exhibit a proof string that shows the inconsistency of PA. If you could, we'd all be screwed!

Comment author: Vladimir_Nesov 01 August 2010 10:39:17AM 0 points [-]

I like to think that you can't actually exhibit a proof string that shows the inconsistency of PA.

Proof in what theory, "can't" by what definition of truth? In the extension of PA with inconsistency-of-PA axiom, it's both provable and true that PA is inconsistent.

Comment author: cousin_it 01 August 2010 10:44:36AM 1 point [-]

A proof in PA that 1+1=3 would suffice. Or, if you will, the Goedel number of this proof: an integer that satisfies some equations expressible in ordinary arithmetic. I agree that there's something Platonic about the belief that a system of equations either has or doesn't have an integer solution, but I'm not willing to give up that small degree of Platonism, I guess.

Comment author: Vladimir_Nesov 01 August 2010 10:56:24AM 0 points [-]

You would demand that particular proof, but why? PA+~Con(PA) doesn't need such eccentricities. You already believe Con(PA), so you can't start from ~Con(PA) as an axiom. Something in your mind makes that choice.

timtyler comments on AI cooperation in practice - Less Wrong

Article Navigation

Comments (157)

Nearest Meetups

Virtual Study Room

Recent Comments

Recent Posts

Recent Rationality Quotes

Recent Wiki Edits

Top Contributors, 30 Days

Recent Karma Awards

Comments (157)

Top Contributors, 30 Days

You'll need to login or register to do that

(Don't worry, it only takes a few seconds)

Create

Login