Benja comments on An angle of attack on Open Problem #1 - Less Wrong

30 Post author: Benja 18 August 2012 12:08PM

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

Article Navigation

Comments (84)

Comments (84)

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

Comment author: Benja 19 August 2012 08:09:12PM *  0 points [-]

K was just said to be a constant symbol, but fine.

PA_K is supposed to be a new name, not some vector PA indexed by K. But that's just notation, and I agree it was a bad choice.

PAK has just been defined, allegedly, but if PA(K) != PAK then I have no idea what PA(K) is, for it was not defined.

PA(.) is a function that takes a number and returns an axiom system (formalized presumably in the form of a recursive enumeration the axioms). On the metalevel, writing PA(K) makes no sense, since you can only apply PA(.) to a number, and on the metalevel, K doesn't denote a number, only a symbol.

However, you can formalize the function PA(.) in the language of Peano Arithmetic, and if you extend that language by a constant symbol K, you can apply this formalized version of the function to this constant symbol. PA_K is Peano Arithmetic (in the language with K) extended by the axiom schema "If PA(K) proves 'C', then C." Here C ranges over the statements of the base language, and 'C' is its Gödel number (written as a unary literal). PA(K) is the object-level recursive enumeration given by the formalized function PA(.) applied to the constant symbol K; it should be standard that given a recursive enumeration of axioms, you can formalize in the language of PA the assertion that a particular number ('C') is the Gödel number of a theorem that follows from these axioms.

I don't see how you can have a constant language, containing one constant symbol, that becomes equal to PA(SSS0) the moment you add one axiom that says SSS0=K.

[Nit: A language cannot be equivalent to a proof system, but I assume that you can't see how you can have a proof system P in the extended language that becomes equivalent to PA(SSS0) the moment that axiom is added.] That challenge is trivial: let P be the set of axioms {"SSS0=K implies A" | A an axiom of PA(SSS0)}. I'm doing something different, but still.

Would anyone care to write out a concrete example of what this language is supposed to do when generating new AIs? As it stands I can't visualize the language itself.

I think if the above didn't help, it might be more helpful for me to first do a writeup of my now-hopefully-fixed proof, since the new version is simpler and IMO provides much better intuition (I at least now feel like I understand what's going on here in a way that I didn't quite before); I'll have to replace PA_K by yet another proof system, and I'll make my metalanguage more explicit about quoting/unquoting when writing it up, so it might be more useful to have that as the starting base before digging into details.

ETA:

Details are often important in reflective reasoning, I've found. In particular there are questions like whether the expression (K-1) can appear in a proof, and so on.

The more precise metalanguage will hopefully also help with this.

Comment author: Eliezer_Yudkowsky 19 August 2012 09:33:26PM 1 point [-]

Try two:

Does the following language do the same thing as PAK?

PAT = PA + symbol K + schema over Formulas of one variable:
- For all P:
-- if P proves-in-PAT 'Formula(K+1)', then Formula(K)
Comment author: Benja 19 August 2012 10:02:20PM *  0 points [-]

Ha! I'm not sure what the exact relation to PAK is, but PAT is almost exactly what I'm using in my new proof:

PPT = PA + symbol K + schema over Formulas of one variable:
- For all P:
-- if P proves-in-PPT 'Formula(K)', and K>0, then Formula(K-1)

("PPT" for "parametric polymorphism trick, v 0.2".) [ETA: added "K>0" condition.]

Comment author: wuncidunci 19 August 2012 09:48:19PM -1 points [-]

PAK proves all which your PAT does, but probably not the other way around.

I think this bit is all that's strictly necessary in the proof though.

Comment author: Eliezer_Yudkowsky 19 August 2012 09:21:26PM 1 point [-]

Does the following language do the same thing as PAK?

PAS = PA + schema over Formulas of one variable:
- For all N, for all P:
-- if P proves-in-PAS 'Formula(N+1)', then Formula(N)

(Actually, on second thought, I retract that, you do want the special symbol so that proving 4 > 3 doesn't get you 3 > 3. But now I need to see if the same problem applies to the original logic as soon as you add K=3...)

Comment author: Eliezer_Yudkowsky 19 August 2012 08:37:16PM 0 points [-]

(Still trying to read, will comment as I go.)

if x proves "p is safe for K steps", then inst(n,x) is a PA(n+1) proof of "p is safe for n steps"

Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), 'x')->x; and then redefine PAK accordingly. (This seems possible, but it's definitely an extra step that for all I know could trip up somewhere, and ought to be stated explicitly.) If we don't take it, then inst(n, x) gives us something that seems like it ought to be provable by analogy, but isn't a direct translation, because the original PA(n) didn't contain a provability formula quantified over PA(.) into which we could plug K=n; and since I think we were proving things about inst later, that's not good.

Comment author: Benja 19 August 2012 08:43:34PM *  0 points [-]

Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), 'x')->x; and then redefine PAK accordingly.

But that's not a redefinition -- that was the definition! [ETA: except you need PA(2) instead of PA(3) in the provable(_,_) predicate, of course.]

Powered by Reddit Powered by Reddit