Unrestricted quantification and Tarskian truth

It is well-known—a feature and not a bug—that Tarski’s definition of truth needs to be given in a metalanguage rather than the object language. Here I want to note a feature of this that I haven’t seen before.

Let’s start by considering how Tarski’s definition of truth would work for set theory.

We can define satisfaction as a relation between finite gappy sequences of objects (i.e., sets) and formulas where the variables are x₁, .... We do this by induction on formulas.

How does this work? Following the usual way to formally create an inductive definition, we will do something like this:

1. A satisfaction-like relation is a relation between finite sequences of sets and formulas such that:

   1. the relation gets right the base cases, namely, a sequence s satisfies x_n ∈ x_m if and only if the nth entry of s is a member of the mth entry of s) and satisfies x_n = x_m if and only if the nth entry of s is identical to the mth entry

   2. the relation gets right the inductive cases (e.g., s satisfies ∃x_nϕ if and only if for every sequence s′ that includes an nth place and agrees with s on all the places other than the nth place we have s′ satisfying ϕ, etc.)

2. A sequence s satisfies a formula ϕ provided that every satisfaction-like relation holds between s and ϕ.

The problem is that in (2) we quantify over satisfaction-like relations. A satisfaction-like relation is not a set in ZF, since any satisfaction-like relation includes ((a),ϕ₌) for every set a, where (a) is the sequence whose only entry is a at the first location and ϕ₌ is x₁ = x₁. Thus, a satisfaction-like relation needs to be a proper class, and we are quantifying over these, which suggests ontological commitment to these proper classes. But ZF set theory does not have proper classes. It only has virtual classes, where we identify a class with the formula defining it. And if we do that, then (2) comes down to:

3. A sequence s satisfies ϕ if for every satisfaction-like formula F the sentence F(s,ϕ) is true.

And that presupposes the concept of truth. (Besides which, I don’t know if we can define a satisfaction-like formula.) So that’s a non-starter. We need genuine and not merely virtual classes to give a Tarski-style definition of truth for set theory. In other words, it looks like the meta-language in which we give the Tarski-style definition of truth for set theory not only needs a vocabulary that goes beyond the object-language’s vocabulary, but it needs a domain of quantification that goes beyond the object-language’s domain.

Now, suppose that we try to give such a Tarskian definition of truth for a language with unrestricted quantification, namely quantification over literally everything. This is very problematic. For now the satisfaction-like relation includes the pair ((a),ϕ₌) for literally every object a. This relation, then, can neither be a set, nor a class, nor a proper superclass, nor a supersuperclass, etc.

I wonder if there is a way of getting around this difficulty by having some kind of a primitive “inductive definition” operator instead of quantifying over satisfaction-like relations.

Another option would be to be a realist about sets but a non-realist about classes, and have some non-realist story about quantification over classes.

I bet people have written on this stuff, as it’s a well-explored area. Anybody here know?