I have been looking at Tarski's work and asked a question here:
Can truth be defined by a 'same-level' language according to Tarski's undefinability theorem?
I am trying to refine my question as follows: if a 'meta-language' L* is meta- only as far as one predicate is concerned, can the truth of that predicate in the lower language L be proven? Or is it essential that L* contains all of L (plus more), to prove the truth of something in L?