In the linked text file I tried to do just that, carefully tracking proof lengths and making sure the bounds stay bounded. But this could really use some checking.
The second problem uses the same trick, of course: “if we both prove that we output the same thing, then we output the same thing”, then move ahead using “we both prove” instead of “I prove” everywhere.
Does the obvious Lobian proof for 1 still go through if there’s a bound on the proof length built into all the sentences?
In the linked text file I tried to do just that, carefully tracking proof lengths and making sure the bounds stay bounded. But this could really use some checking.
The second problem uses the same trick, of course: “if we both prove that we output the same thing, then we output the same thing”, then move ahead using “we both prove” instead of “I prove” everywhere.