When I was a graduate student at Berkeley in the early 90s, I had heard that Silver's approach to refuting ZFC involved the idea that somehow we make a mistake in our thinking about ZFC by conflating the internal idea of syntax and semantics, as undertaken internally to the object theory by representing formulas and syntax trees etc. as sets and then defining the notion of truth for them as in the Tarski recursion, and the external metatheoretic notions of syntax and semantics. Silver's idea, as I understood it, was that there was some subtle logical error that arises in our thinking about this.
This is all second-hand, and I never heard this view directly from Silver, however, as he rarely talked about his project.
The two notions do definitely pull apart in $\omega$-nonstandard models, and there are many interesting observations to make about the difference. For example, there is the beautiful theorem of Brice Halimi that every model of ZFC has an element that is a structure $\langle M,\varepsilon\rangle$, which when viewed externally as a model in the language of set theory, satisfies ZFC. In short, every model of ZFC has an element that is a model of ZFC. Understanding the statement and proof of this theorem requires one to distinguish carefully between the object-theoretic ZFC and the meta-theoretic ZFC, since the original model, of course, might satisfy ÂŹCon(ZFC), and yet still it has a model $\langle M,\varepsilon\rangle$ that satisfies every actual axiom of ZFC.
Meanwhile, let me also state as a fact that many mathematicians and set theorists do commonly conflate the internal and external approaches. Let me give three examples.
Truth predicates. One can commonly find incorrect definitions of what it means to have a class truth predicate. Namely, people sometimes say that a truth predicate in set theory is a class $T$ of pairs $\langle\varphi,\vec a\rangle$ such that $V\models\varphi[\vec a]$ or something like that, which is trying to use the external semantic notions internally. To formalize truth in Gödel-Bernays set theory or Kelley-Morse, however, one should speak of a satisfaction class that fulfills the disquotational Tarski recursion, and this will involve nonstandard formulas.
Forcing relation. Similar confusions surround much of the literature on the definition of the forcing relation, particularly in the case of class forcing. In many accounts, people try to define the forcing relation by saying $p\Vdash_{\mathbb{P}}\varphi$ over $M$ if for every $M$-generic filter $G\subset\mathbb{P}$ we have $M[G]\models\varphi$. But this account, which uses the meta-theoretic notion, is not generally correct; for example, some uncountable models $M$ may have no generic filters. Certainly it is not correct for defining the forcing relation over $V$ in a model of Gödel-Bernays set theory. The confusion often causes people to think incorrectly that we have a satisfactory forcing technology only over countable transitive models.
Meanwhile, in my paper with several co-authors
we provide what I view as the correct definition of what it means to have a forcing relation, namely, it means to have a class relation that fulfills the forcing recursion. This is exactly analogous to the difference between the internal/external account of what it means to have a truth predicate.
Elementarity of embeddings. In large cardinal set theory one often wants to refer to elementary embeddings defined on proper class domains or often $V$ itself, $j:V\to M$. But how does one express the elementarity requirement? Typically, in the literature one sees people say that $j$ is $\Sigma_1$-elementary and cofinal. This implies by induction (in the metatheory) that $j$ preserves the truth of any $\Sigma_n$ assertion, for any metatheoretically finite $n$. So one has that the embeddings are elementary, but only for meta-theoretically finite assertions, and so this notion falls short of what might be regarded as fully elementary. It is indeed a subtle matter to get elementarity for all assertions in the object theory. So again we see the distinction between the internal syntax/semantics and the external.
My point with all these examples is that people do sometimes make the mistake that I have claimed Silver highlights in his proof strategy.
Nevertheless, what is much less clear to me is how one will turn this into a refutation of ZFC, since I don't see the error being made in the axiom schemes of ZFC itself, but rather only in mistaken applications of it.
