In this blog post J.D.Hamkins shows that KM set theory can define truth predicate for first-order set theory, which means, I believe, that there is a second-order definition of such predicate and KM shows that it is indeed what we want it to be.
Author claims that it's easy to define partial truth predicates for all $\Sigma_n$, but it's in no way clear to me how such construction would work in ZFC. Even then, to define full truth predicate, we need a way of defining these predicates in second order language with uniform complexity, so that we can then combine them.
I tried looking for such constructions, however I wasn't really successful. My question is then:
How do we define full truth predicate in second order set theory?
I have tried to define such predicate by using a class of witnesses when adding existential quantifiers and similar construction for existential ones, but I didn't manage to make it work.
Let's say that a formula $\Phi(x, y)$ is a satisfaction predicate for $\mathcal L_\in$ if is satisfies the Tarski clauses; that is, if:
($\in$) $\Phi(``x_i\in x_j", a) \leftrightarrow a(i)\in a(j)$
($=$) $\Phi(``x_i = x_j", a) \leftrightarrow a(i) = a(j)$
($\wedge$) $\Phi(``\phi \wedge \psi", a) \leftrightarrow \Phi(``\phi", a) \wedge \Phi(``\psi", a)$
($\neg$) $\Phi(``\neg\phi", a)\leftrightarrow \neg\Phi(``\phi", a)$
($\exists$) $\Phi(``\exists x_i\phi", a)\leftrightarrow \exists a'=_{i} a\Phi(``\phi", a')$
where $\phi,\psi\in\mathcal L_\in$, $a$ is a function with domain $\omega$, and $a=_{i} a'$ means that $a$ and $a'$ agree except possibly at $i$. We assume that $\Phi(x, y)$ only applies to formula/assignment pairs.
Then we want to show that there is such a predicate in second-order set theory. I like to do this in two steps. First, I define $X$ to be a satisfaction class for $\phi\in\mathcal L_\in$ if $X$ satisfies the Tarski clauses for subformulas of $\phi$ and I prove by induction that any two satisfaction classes for $\phi$ are co-extensive. Second, I prove by induction that every formula in $\mathcal L_\in$ has a satisfaction class. One can then conclude that $\Phi(x, y) =$ "there is a satisfaction class $X$ for $x$ such that $\langle x, y\rangle\in X$" is a satisfaction predicate for $\mathcal L_\in$.
Here's how the second induction goes for the $\exists$ case. Suppose that $X$ is a satisfaction class for $\phi$. Now by predicative comprehension, we define $Y = X \cup \{\langle ``\exists x_i\phi", a\rangle: \exists a'=_{i} a(\langle ``\phi",a'\rangle\in X)\}$. Since $X$ is a satisfaction class for $\phi$, it is easy to see that $Y$ is a satisfaction class for $\exists x_i\phi$, as required.
(It might be interesting to note that this argument doesn't require the full power of MK. In particular, it only uses predicative instances of comprehension. What it requires beyond NBG is separation for $\Sigma^1_1$ formulas (in order to run the inductions in the two steps). But this is an assumption about the sets, not about the classes. In other words, the argument will go through even if you think there are relatively few classes, so long as you think that sets satisfy separation for $\Sigma^1_1$ formulas.)