Semantic Anti-Realists hold that a claim has a (constructive) proof if the claim is true. I wonder whether this position runs into a version of Yablo's supposedly non-circular version of the liar paradox.

Recall that Yablo's paradox arises from what one may call Yablo sequences over some first-order language augmented with a truth predicate and rich enough to allow Gödel numbering. The Yablo sequence over such a language is simply a countably infinite sequence of formulas, where for every natural number i, the i-th member is the formula that intuitively says that for every j > i, the j-th sequence member is not true. It is easy to see that under the assumption of classical logic the first member of the sequence is both true and not true.

Now, we can augment the language with a constructively interpreted provability predicate and form P(rovability)-sequences: infinite sequences of formulas, where the i-th member says that for every j > i, the j-th member is not (constructively) provable.

If the first member of a given P-sequence is true then all greater sequence members are not provable, so the second is not provable.So, since truth entails provability, the second member is not true. So, there's some sequence member greater than the second that is provable. But this contradicts the truth of the first sequence member.

If the first member of the given P-sequence is not true, then there are sequence members greater than the first that are provable. Let A be the smallest such sequence member. Since provability clearly entails truth, A is true. But then all sequence members that follow A are not provable. In particular, A's immediate successor, A+1, is not provable, hence not true. So, after A+1 we find sequence members that are provable. But this contradicts the truth of A.

I suspect that anti-realists would simply deny that excluded middle holds at least for the first member of the P-sequence, thus eschewing contradiction, since the first member in some way involves infinite collections. I'm not sure, if this response is acceptable. But I suppose that in that case the above argument can be reworked to be compatible with constructivist assumptions (as has been shown for the simple liar paradox by Friedman and Sheard).

So my questions are: Is the above argument a paradox for the anti-realist? How could the argument be reworked, if it were the case that the original argument involved non-constructive assumptions?

• Anti-realism is the extension of intuitionism beyond mathematics. This does not just mean that they deny excluded middle, they also deny that the intuitive notion of proof can be captured by any formalism. This means that the provability predicate of any formal theory does not match the (intuitionistic) truth. And this is why neither Gödel incompleteness nor Yablo sequences are a problem for them. – Conifold Sep 18 '19 at 17:53
• This is not correct. This only applies to Brouwer's own conception of proof, but there's a large bunch of logics that try to capture different versions of constructive proof: for instance various intuionistic logics or Tennant's substructural logic. And of course provability predicates are available for intuitionists: Take [] A to mean that A is provable in Heyting Arithmetic and off you go.So the paradox still seems to apply. – sequitur Sep 18 '19 at 20:39
• This is Dummett's conception of anti-realism, and he coined "anti-realism". As for conceptions of constructive proof, there are many that are even perfectly compatible with classical logic, but they have little to do with philosophical anti-realism. Tait's paper is titled Against Intuitionism: Constructive Mathematics Is Part of Classical Mathematics, for example. Provability predicates are available to everyone, but none of them captures anti-realist truth, which is provability, but not in any formalism. – Conifold Sep 19 '19 at 2:09
• I'd like to see a reference concerning Dummett, since my reading of him deviates from yours in this respect. But of course there are anti-realists who aim to formalize their notions of proof: Dirk van Dalen, Göran Sundholm, Dag Prawitz, Neil Tennant. So,you can take my paradox to have as its target those anti-realists who think their notion of proof is formalizable. – sequitur Sep 20 '19 at 14:31
• It's quite clear that there are notions of constructiveness compatible with classical logic or math, since otherwise constructive proofs wouldn't be possible there. I never denied that. I also don't see what I am supposed to do with Tait's paper here. His main point is that constructive mathematics can be embedded in classical math. Again I didn't deny that and besides it's trivial, since intuistionistic logic is a sublogic of classical logic. – sequitur Sep 20 '19 at 14:33