Семантика металогики. (Часть 1)

По смыслу это будет несколько запоздавшим продолжением моего доклада в мае, но по форме - независимым докладом (т.е. знакомство с содержанием прошлых серий не требуется).
1. Рассматривается металогика логик первого порядка (в смысле Л. Полсона и его системы Isabelle, с некоторыми упрощениями за счёт ограничения класса объектных логик). Сама по себе эта металогика - это по существу фрагмент интуиционистской логики второго порядка, с помощью связок и кванторов которой формализуются, например, горизонтальная черта и запятая в правилах вывода объектной логики. Например, правила модус поненс и обобщения из объектной логики записывается в этом формализме так:
$\forall_0 A \forall_0 B ((!A \bigwedge !(A\to B))\Rightarrow !B)$ и
$\forall_1 A ((\forall x !A(x))\Rightarrow !(\forall x A(x))),$
где $\to$ и $\forall$ - импликация и квантор всеобщности объектной логики, $\Rightarrow$, $\bigwedge$, $\mathbf{\forall}$ и $\forall_n$ - соответственно метаимпликация, метаконъюнкция, метаквантор первого порядка и n-арный метаквантор второго порядка, а ! - оператор рефлексии, формально конвертирующий произвольную формулу в атомарную метаформулу (его, в принципе, можно было бы и не писать, т.к. все его вхождения тривиально восстанавливаются).
При этом никаких условий на свободные переменные ни в правиле обобщения, ни в каких-либо других правилах, принципах и формулах объектных логик не подразумевается - они оказываются не нужны (или, точнее, переезжают на мета-уровень - в мета-правила вывода, задающие саму металогику, а именно в те из них, которые по существу выражают "правило подстановки" для объектной логики). Это позволяет формализовать в рамках металогики не только запятую и горизонтальную черту, но и всю дедуктивную систему объектной логики (ибо вся она записывается одной метаформулой), а также многое другое: выводимость заданного принципа или правила в объектной логике, импликацию между принципами (а не между выражающими их формулами или схемами), фиксированные переменные (в смысле Клини) и т.д.
2. В обычной теории моделей, основанной, в частности, на понимании семантического следования по Тарскому, метасвязки и метакванторы $\Rightarrow$, $\bigwedge$, $\forall$ и $\forall_n$ интерпретируются классически, причём двузначно, притом, что сами они - интуиционистские. Ничто не мешает рассматривать "многозначную" семантику Тарского, в которой не только связки и кванторы, но также и метасвязки и метакванторы могут интерпретироваться многозначно. Например, если объектная логика - интуиционистская, оператор рефлексии ! может интерпретироваться подходящим отображением между топологическими пространствами, в одном из которых интерпретируются связки и кванторы, а в другом - метасвязки и метакванторы.
Но более интересна альтернативная теория моделей, основанная, в частности, на другом понимании семантического следования - по Колмогорову (входящем в его оригинальную задачную интерпретацию интуиционистской логики). Альтернативные интерпретации металогики тоже бывают "двузначные" и "многозначные" (не только на объектном, но и на мета-уровне). Более того, в альтернативном случае, с интуиционистской объектной логикой, оказывается вполне содержательной ситуация, в которой метасвязки и метакванторы интерпретируются по существу так же, как и соответствующие связки и квантор всеобщности. Это позволяет, наконец, придать некоторый вполне формальный смысл всей задачной интерпретации Колмогорова.
В том, что касается интерпретации формул и принципов, все рассматриваемые варианты обобщённых моделей логик по существу сводятся к обычным. Они ведут себя иначе лишь в части интерпретации правил (а также более сложных металогических конструкций, как, например, импликации между принципами). Это вполне относится, например, к топологическим моделям интуиционистской логики, но про "модели" реализуемостного типа (включая, например, "финитные задачи" Медведева) лучше сказать иначе: если их понимать как альтернативные модели, это ничего не меняет в том, какие в них выполняются принципы, но позволяет дать хоть какое-то разумное определение выполнения правил в таких моделях. Имеются и другие интересные примеры альтернативных моделей, в том числе, когда объектная логика - классическая.