I will show that my AI will be able to accept itself as a safe rewrite
Now again unsure whether I can show this. Argh.
ETA: The argument I want to be making is the one from the third paragraph in the proof sketch. The problem is the quantification over p—I need to show in PPT that “for all p, if PPT proves ‘p is safe for K steps’, then p is safe for K-1 steps”. But the axioms of PPT (v0.2) don’t allow for parameters (free variables) in the statement C.
Now again unsure whether I can show this. Argh.
ETA: The argument I want to be making is the one from the third paragraph in the proof sketch. The problem is the quantification over p—I need to show in PPT that “for all p, if PPT proves ‘p is safe for K steps’, then p is safe for K-1 steps”. But the axioms of PPT (v0.2) don’t allow for parameters (free variables) in the statement C.
I seem to have fixed the remaining problems; new proof attempt here.