Stewart Shapiro’s 1998 paper “Induction and indefinite extensibility: The Gödel sentence is true, but did someone change the subject?” makes a really nice point that I hadn’t thought about before. Let’s say that you’re attracted to the following two kinds of claims.

1) Autonomy in logic – A logical truth should be provable using the logical rules for just the connectives in that truth.
2) Logicism in mathematics – Mathematical truths are logically true, in a properly extended sense of ‘logically’.

Several writers, tracing back at least to Dummett, have used (1) to argue against classical logic. The problem is that Pierce’s Law, i.e. ((p → q) → p) → p, is a classical theorem. But, they say, it can’t be proven given just the appropriate logical rules for →. The latter claim is controversial, but plausible.

The problem is that if you don’t like Pierce’s Law for this reason, you should think that ∃x ∃y (x ≠ y) should be provable using just the logical rules for ∃ and ≠, at least if it is a logical truth. Now on the one hand, it doesn’t seem plausible that the rules for ∃ and ≠ suffice to prove ∃x ∃y (x ≠ y). Certainly the intuitionist rules for ∃ and ≠ don’t suffice.

On the other hand, 0 ≠ 1 is a mathematical truth. So ∃x ∃y (x ≠ y) is a mathematic truth. So, given logicism, it is a logical truth. So given autonomy, it should be provable by considerations purely about ∃ and ≠.

Of course, there’s a lot that can be said about various ways out of this puzzle you might try while holding on to something like (1) and (2). But ∃x ∃y (x ≠ y) isn’t the only case where there’s a conflict between (1) and (2), so the ways out have to do a lot of work. Shapiro’s paper is a very nice study of what the options are here, and why they all look fairly problematic. I recommend the paper to anyone who is interested in these issues. (Though, to be fair, there probably aren’t that many people like me who both are interested in these issues and haven’t read the paper already!)