Tarski's truth sentences and MIRI's AI — LessWrong