Т.е. "истинное в теории" = "доказуемое в метатеории" (в некой метатеории)?
Мне кажется, что это несколько прямолинейная точка зрения. Есть определенные нюансы, которые нужно учитывать, и которые можно проиллюстрировать на примере классического пропозиционального исчисления.
Рассмотрим язык пропозиционального исчисления над множеством из трех пропозициональных переменных

и над множеством пропозициональных связок

.
Множество всех правильно построенных формул (или “предложений”) этого языка обозначим через

. Это – наш “объектный” язык.
Говорить о предложениях объектного языка будем в метаязыке, содержащем переменные

, которые, как будем предполагать, пробегают по множеству

, и набор символов операций

, которые обозначают операции над элементами множества

, рассматриваемого как “абсолютно свободная алгебра” в духе польской школы:
http://www.px-pict.com/9/6/2/3/1/2/1.htmlПонятно, как работают операции

. Например, если

и

, то

.
Потом следует учесть, что пропозициональное исчисление это не только язык

, но еще и правила вывода, позволяющие определить на множестве

бинарное отношение “выводимости”. Чтобы говорить о нем в метаязыке, введем в него символ бинарного отношения

(атомарная формула метаязыка

содержательно читается как “из предложения объектного языка

выводимо предложение объектного языка

”).
Введем в наш метаязык еще один символ бинарного отношения

, выразив его через символ бинарного отношения

следующим образом:

тогда и только тогда, когда

и

.
Правила вывода классического пропозиционального исчисления подобраны таким образом, чтобы отношение

оказалось бы некоторым отношением эквивалентности на множестве

и, более того, – некоторой конгруэнцией на множестве

, рассматриваемом как “абсолютно свободная алгебра”.
Кроме того, правила вывода классического пропозиционального исчисления подобраны еще и таким образом, чтобы факторалгебра

абсолютно свободной алгебры

по конгруэнции

оказалась бы булевой алгеброй. В нашем конкретном случае, когда объектный пропозициональный язык содержит три пропозициональные переменные, это будет свободная булева алгебра с тремя образующими, содержащая, как известно, в точности

элементов.
Следовательно, мы можем говорить в нашей метатеории о всех конструкциях этой булевой алгебры и, в частности, о ее единичном элементе. Поскольку наша булева алгебра реализована как некоторая фактор-алгебра, то ее единичным элементом будет некоторое подмножество множества

предложений объектного языка. Обозначим это подмножество символом

. Теперь мы можем ввести в метаязыке символ унарного отношения

(атомарная формула метаязыка

содержательно читается как “предложение

объектного языка является общезначимым”) следующим образом:

тогда и только тогда, когда

.
Так что, если отождествить истинность предложения

объектного языка с его общезначимостью, то тогда действительно будет, что

-- истинно, тогда и только тогда, когда в метатеории доказуема формула

.
Но это слишком сильное определение истинности для предложений пропозиционального исчисления. Будут формулы (например,

), которые не являются ни истинными, ни ложными в этом смысле.
Обычно, говоря об истинности или ложности некоторого предложения пропозиционального исчисления, неявно подразумевают эту истинность или ложность не вообще, а относительно того или иного “возможного мира” (в терминологии Витгенштейна; суть этой терминологии можно посмотреть здесь:
http://www.px-pict.com/preprints/1.html).
В построенной выше булевой алгебре мы можем отождествить “возможные миры” с максимальными фильтрами булевой алгебры. Значит, мы можем говорить о них в метатеории. Предложение

объектного языка истинно в “возможном мире” (или максимальном фильтре)

тогда и только тогда, когда

.
Теперь мы можем доказать в нашей метатеории такую теорему об истинности-ложности предложений объектного языка: “В любом “возможном мире”

каждое предложение

объектного языка является либо истинным, либо ложным”. Однако мы не можем доказать в метатеории факт истинности или ложности конкретного предложения

объектного языка, поскольку теперь эта истинность зависит от конкретного “возможного мира”.