...можно проиллюстрировать на примере классического пропозиционального исчисления.
Мне кажется, что то, о чём Вы далее пишете, является во многом излишним усложнением.
Рассмотрим язык пропозиционального исчисления над множеством из трех пропозициональных переменных
и над множеством пропозициональных связок
.
Множество всех правильно построенных формул (или “предложений”) этого языка обозначим через
. Это – наш “объектный” язык.
Говорить о предложениях объектного языка будем в метаязыке, содержащем переменные
, которые, как будем предполагать, пробегают по множеству
, и набор символов операций
, которые обозначают операции над элементами множества
, рассматриваемого как “абсолютно свободная алгебра” в духе польской школы:
http://www.px-pict.com/9/6/2/3/1/2/1.htmlПонятно, как работают операции
. Например, если
и
, то
.
Потом следует учесть, что пропозициональное исчисление это не только язык
, но еще и правила вывода, позволяющие определить на множестве
бинарное отношение “выводимости”. Чтобы говорить о нем в метаязыке, введем в него символ бинарного отношения
(атомарная формула метаязыка
содержательно читается как “из предложения объектного языка
выводимо предложение объектного языка
”).
Введем в наш метаязык еще один символ бинарного отношения
, выразив его через символ бинарного отношения
следующим образом:
тогда и только тогда, когда
и
.
Всё это понятно. Только зачем для метатеории сочинять синтаксис, который бы ни в чём не пересекался с синтаксисом (и даже с алфавитом) предметной теории? Если уж мы привыкли в предметной теории употреблять логические связки
,
,
,
и
, то зачем их обязательно заменять на
,
,
,
и
? По-моему, метаязык по своей структуре не обязан ничем отличаться от предметного языка. Единственно, должна быть предусмотрена возможность однозначного указания того, когда речь идёт о формулах предметной теории. Естественно, это может потребовать некоторых дополнительных по отношению к предметному языку выразительных возможностей, но не обязательно ревизии всего его в целом, вплоть до алфавита. Например, утверждение о том, что в предметной теории
действует правило вывода modus ponens, можно записать так:
Здесь
читается: "Строка A является правильным высказыванием в языке теории T", а
читается как: "Высказывание A является теоремой теории T".
Как видите, символы импликации используют и предметная теория, и метатеория, причём в одинаковых смыслах, и при правильно расставленных скобках это не должно приводить к путанице.
А в остальном, как я понимаю, изложеный Вами подход к построению высказываний метаязыка ничем принципиальным не отличается.
Кроме того, правила вывода классического пропозиционального исчисления подобраны еще и таким образом, чтобы факторалгебра
абсолютно свободной алгебры
по конгруэнции
оказалась бы булевой алгеброй.
Почему именно булевой? Чем объясняется особая любовь к булевой алгебре?
Так что, если отождествить истинность предложения
объектного языка с его общезначимостью, то тогда действительно будет, что
-- истинно, тогда и только тогда, когда в метатеории доказуема формула
.
Честно говоря, я не до конца понял смысла такого витиеватого и формального подхода к определению "истинности в теории". По моим понятиям "истинность" - это теоретическая концепция, а значит говорить о том, что истинно, нам должна теория. Естественно, так или иначе принятая нами (а не любая спорная) теория. Поэтому задача метатеории (применительно к понятию истинности) заключается только в том, чтобы сказать, какая(ие) теория(ии) "принята(ы)". В таком случае любое доказанное в теории высказывание автоматически считается "истинным".
Обычно, говоря об истинности или ложности некоторого предложения пропозиционального исчисления, неявно подразумевают эту истинность или ложность не вообще, а относительно того или иного “возможного мира” (в терминологии Витгенштейна; суть этой терминологии можно посмотреть здесь:
http://www.px-pict.com/preprints/1.html).
В построенной выше булевой алгебре мы можем отождествить “возможные миры” с максимальными фильтрами булевой алгебры. Значит, мы можем говорить о них в метатеории. Предложение
объектного языка истинно в “возможном мире” (или максимальном фильтре)
тогда и только тогда, когда
.
Естественно, большая часть теорий имеют ограниченную сферу применения, поэтому для них неправильно будет говорить что они "приняты вообще", т.е. доказанные ими высказывания истинны в любом "возможном мире". В таком случае задача метатеории усложняется: Она должна не просто сказать, какая теория принята, а определить, применительно к какой предметной области.
Теперь мы можем доказать в нашей метатеории такую теорему об истинности-ложности предложений объектного языка: “В любом “возможном мире”
каждое предложение
объектного языка является либо истинным, либо ложным”. Однако мы не можем доказать в метатеории факт истинности или ложности конкретного предложения
объектного языка, поскольку теперь эта истинность зависит от конкретного “возможного мира”.
Опять же, я здесь не вполне понял какую ценность имеет доказательство этого утверждения (согласно Вашей формулировке это ни что иное, как закон исключённого третьего). Вам так важно, чтобы логические значения подчинялись именно булевой алгебре, т.е. чтобы их было строго два?