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?