I think [t]he concept of definability...only makes sense from an outside-the-universe perspective [because of] Tarski's theorem on the non-definability of truth is not adequately argued for in this answer, since many people (such as myself) believe that, in fact, definitions in SOL can be perfectly adequate, it is only that SOL is not a proper logic as it lacks a semi-decidable proof theory. The claim that every definition must come equipped with a complete set of proof conditions is one that I dispute. Henkin showed that SOL, like PA, is a sound-but-incomplete multi-sorted FOL.

@CMCDragonkai - I really should put together some of these diagrams. A short, well-illustrated white paper on the topic would indeed make this point of view easier to explain. I have put this on my list of "hope to dos"