Isn’t this just saying that not all proofs are constructive? That is, just because you can prove the existence of an object doesn’t mean you necessarily have a

Isn’t this just saying that not all proofs are constructive? That is, just because you can prove the existence of an object doesn’t mean you necessarily have a method for identifying it. Also, there is some vague appeal to a substructural logic here, since by mixing up the forgery with the genuine article, you’re destroying the information about their origins, which is what prevents you from identifying the forgery afterward. I’m not up on my modal logic, but I think this can be expressed as ◻∃x.P(x) ↛ ∃x.◻P(x)—proving the existence of some x for which P is true does not imply that there exists any particular x for which P is provable.