== Problem 1 ==

Consider a program that knows its own source code (by quining) and
contains a strong enough proof checker. The program's algorithm is 
as follows: try all proofs of length up to nmax, looking for a 
proof that the program itself returns 1. If such a proof is found, 
return 1. Otherwise do the same for 2, then 3, then return 0. 

The question is: what will the program return?


== Solution to problem 1 ==

I believe that the program will in fact return 1. Because the proof 
is quite involved, I will first write out the program itself, using 
a JavaScript-like syntax, with large parts snipped.

    function eval(code)
    {
        // Runs code and returns whatever it evaluates to.
        // Uses the definitions of other functions directly.
        ...
    }

    function proves(code, maxsteps)
    {
        // Enumerates all proofs up to maxsteps, searching for a 
        // proof that code evaluates to true. Returns true if found.
        // Uses the definitions of other functions known by quining.
        ...
    }

    function outputs(x)
    {
        // Returns a string of code claiming that main returns x.
        return "main()==" + x;
    }

    function implies(bool1, bool2)
    {
        // Returns true if one boolean value implies another. 
        if (bool1)
            return bool2;
        else
            return true;
    }

    function main()
    {
        var nmax = ...; // A big number
        if (proves(outputs(1), nmax))
            return 1;
        if (proves(outputs(2), nmax))
            return 2;
        if (proves(outputs(3), nmax))
            return 3;
        return 0;
    }

Now for the actual proof. It will closely follow the proof of Lob's 
theorem, but add length limits where needed. Let n1, ... ,n6 be a 
suitably fast-growing sequence of numbers smaller than nmax. The 
number n1 should also be large enough to start with; the proof will 
show exactly how large. I will list twelve code snippets that are 
proved to return true by the program:

1. By the Diagonal Lemma, there exists a code string "box" such 
   that the following will be proved:

   eval(box) == implies(
                    proves(box, n1),
                    eval(outputs(1)))

2. The program can inspect the source code of main() and notice 
   that, if the first conditional happens to be true, the program 
   will output 1:

   implies(
       proves(outputs(1), n6),
       eval(outputs(1)))

3. An obvious consequence of 1:

   implies(
       eval(box),
       implies(
           proves(box, n1),
           eval(outputs(1))))

4. If we can prove 3, we can prove that we can prove it:

   proves(
       "implies(
            eval(box),
            implies(
                proves(box, n1),
                eval(outputs(1))))",
        n2)

5. Pull "implies" outside of "proves", adding some length limits:

   implies(
       proves(box, n1),
       proves(
           "implies(
                proves(box, n1),
                eval(outputs(1)))",
           n3))

6. Push "proves" inside "implies", adding more limits:

   implies(
       proves(box, n1),
       implies(
           proves("proves(box, n1)", n4),
           proves(outputs(1), n5)))

7. If we know box has a short proof, that fact has a slightly 
   longer proof:

   implies(
       proves(box, n1),
       proves("proves(box, n1)", n2))

8. Logic on 6 and 7, using the fact that n2 < n4:

   implies(
       proves(box, n1),
       proves(outputs(1), n5))

9. Logic on 8 and 2, using the fact that n5 < n6:

   implies(
       proves(box, n1),
       eval(outputs(1)))

10. By luck, 9 is exactly the definition of box from 1:

    eval(box)

11. If we can prove 10, we can prove that we can prove it. 
    This is the crucial step that tells us how large n1 must be: 
    large enough that 11 follows from 10.

    proves(box, n1)

12. Logic on 9 and 11:

    eval(outputs(1))

Now, If the proof checker can prove only true statements, this 
means the program will in fact output 1. QED.



== Problem 2 ==

Consider two programs, each of which knows its own source code
via quining. The programs are playing a variant of the Prisoner's
Dilemma: each receives as input the source code of the other, and
outputs true for Cooperate or false for Defect. The algorithm of
each program is as follows: try all proofs up to a certain length
(the proof system and the max length depending on the program),
looking for a proof that both programs output the same value 
(i.e. that I cooperate if and only if the other guy cooperates). 
If a proof is found, the program outputs true, otherwise false.

The question is: will the two programs cooperate?


== Solution to problem 2 ==

Like in Problem 1, assume that the two programs A and B have parts 
named mainA and mainB, provesA and provesB, etc., accessible to
both programs. Define a new function "proves" as follows:

   function proves(code, maxsteps)
   {
       return provesA(code, maxsteps) && provesB(code, maxsteps);
   }

Now use the same solution as in Problem 1, except in the beginning:

1. By the Diagonal Lemma, construct a code string "box" so that 
   the following will be proved by both programs: 

   eval(box) == implies(
                    proves(box, n1),
                    (mainA() == mainB()))

2. Both programs can prove the following by inspecting the source
   of A and B (recall that "proves" implies provesA and provesB):

   implies(
       proves("mainA() == mainB()", n6),
       (mainA() == mainB()))

Steps 3 through 12 are the same as in the solution to Problem 1.
They use properties of the "proves" function that hold if both
proof systems are strong enough - they don't have to be equivalent.
Finally we see both programs will prove that mainA() == mainB(), 
which implies that they will both return true. QED.