Another question is, what if we had two proof systems, neither of which encompasses the other? (Most horrifyingly, what if one were PA plus the Gödel sentence of PA, and the other were PA plus the negation of the Gödel sentence?)
I think that works too. Call these proof systems PA+ and PA- and the FairBots using them FB+ and FB-. PA can prove that any theorem of PA is also a theorem of PA+ and PA-. So PA can prove:
“FB+(FB-)=C” is provable in PA implies “FB+(FB-)=C” is provable in PA-
“FB+(FB-)=C” is provable in PA implies FB-(FB+)=C (using 1 and looking at FB-)
and similarly for the other half of the Löbian circle. So FB+(FB-)=C and FB-(FB+)=C are theorems of PA and hence theorems of PA- and PA+.
I think that works too. Call these proof systems PA+ and PA- and the FairBots using them FB+ and FB-. PA can prove that any theorem of PA is also a theorem of PA+ and PA-. So PA can prove:
“FB+(FB-)=C” is provable in PA implies “FB+(FB-)=C” is provable in PA-
“FB+(FB-)=C” is provable in PA implies FB-(FB+)=C (using 1 and looking at FB-)
and similarly for the other half of the Löbian circle. So FB+(FB-)=C and FB-(FB+)=C are theorems of PA and hence theorems of PA- and PA+.