Opps, I made an error when I said: "It is clear that (X->Y)->X does not imply (not X)->X, so your little trick doesn't work." This is false. This implication does exist, so we get:

((not ◻C)->(◻C))

This sentence is true just in case C is in fact provable, so we don't have a problem with your 2=1 cases.

The problem is that while Lob's theorem says that whenever we have ((◻C)->C), C is provable, it does not mean that there is a proof of C from ((◻C)->C). This means that you're use of the deduction theorem is incorrect. You can only say (((◻C)->C)->(◻C)). It is clear that (X->Y)->X does not imply (not X)->X, so your little trick doesn't work.

This has been mentioned many times, by Peter Singer, for instance, but one way towards moral progress is by expanding the domain over which we feel morally obligated. While we may have evolved to feel morally responsible in our dealings with close relatives and tribesmen, it is harder to hold ourselves to the same standards when dealing with whoever we consider to be not part of this group. Maybe we can attribute some of moral progress to a widening of who we consider to be a part of our tribe, which would be driven by technology forcing us to live and interact with and identify with larger and more diverse groups of people. Clearly this doesn't solve all the problems of moral progress, but I think this idea could chip away at parts of the problem.