Формальная металогика логик первого порядка и её формальная семантика

Рассматривается металогика Л.Полсона, в терминах которой в известном пруфчекере Isabelle формализован широкий спектр различных логик и теорий (от классической логики первого порядка с теорией множеств Цермело-Френкеля до исчисления секвенций Генцена и теории типов Мартин-Лёфа). Точнее, мы ограничимся слегка упрощённым вариантом этой металогики (достаточным для логик первого порядка), который сам по себе можно рассматривать как фрагмент обычной интуиционистской логики второго порядка. Имеется обширная литература о металогиках теорий типов, известных как logical frameworks, но несмотря на широкую известность Изабели, известная автору литература о металогике Полсона и вообще металогиках логик первого порядка сводится к оригинальной статье Полсона "The foundation of a generic theorem prover" и руководствам пользователя к Isabelle. В частности, семантика таких металогик, по-видимому, вообще никем не обсуждалась.
Зачем логике первого порядка вообще нужна формальная металогика? Во-первых, для прояснения неявно подразумеваемых в литературе мета-логических понятий и утверждений, которые ввиду их постоянного использования обычно никак не комментируются, что с точки зрения буквоеда (игнорирующего неявно подразумеваемое) зачастую выглядит как путаница и двусмысленности. Так, например, в литературе принято говорить о "синтаксическом следовании" как о вполне конкретном понятии, хотя синтаксическое следование в смысле учебников Шёнфилда и Мендельсона неэквивалентно синтаксическому следованию в смысле учебников Чёрча, Колмогорова-Драгалина, Трулстры и ван Далена, тогда как Клини и А.Аврон рассматривали оба варианта одновременно, а также соответствующие им два варианта семантического следования, указывая на наличие обоих вариантов в примерах из элементарной математики. (В действительности, один вариант отличается от другого присутствием неявно подразумеваемого метаквантора первого порядка.) Другой пример: хотя в интуиционистской логике из принципа двойного отрицания выводим принцип исключённого третьего (в силу выводимости схемы \neg\neg(\gamma\lor\neg\gamma)), из схемы, соответствующей первому (\neg\neg\alpha\to\alpha) схема, соответствующая второму (\alpha\lor\neg\alpha) невыводима (поскольку при \alpha=\neg\beta первая выводима, а вторая - нет); таким образом, распространённая в литературе практика формулировать принципы в виде схем (т.е. писать схемы, называя их при этом "принципами"), строго говоря, некорректна. (В действительности, различие между принципами и схемами связано с присутствием неявно подразумеваемого метаквантора второго порядка, явное использование которого, впрочем, делает излишним и само употребление метапеременных в подобных случаях.)
Во-вторых, металогика позволяет рассматривать правила вывода как объекты некоторой формальной системы (а именно, как метаформулы специального вида), в том числе устраняя необходимость в побочных условиях, таких как "где t свободен для x в F" и "где x не входит свободно в F". При традиционной записи схем и правил с помощью побочных условий оказывается нетривиальным вопрос о том, какое выражение следует считать правилом, а какое - нет, и это приводит к тому, что вопросы о допустимых, стабильно допустимых и т.п. правилах формулируются и решаются почти исключительно для пропозициональных логик (где побочных условий не возникает вообще). Причём даже для пропозициональных логик остаётся неясным, что в общем случае соответствует подобным синтаксическим вопросам на уровне моделей. Мы рассмотрим две формальных семантики рассматриваемой металогики: "семантику Тарского", обобщающую традиционные соглашения, принятые в теории моделей (и по существу сводящуюся к ним), и "семантику Колмогорова", которая формализует мета-логическое расширение BHK-интерпретации интуиционистской логики, включающее данную самим Колмогоровым интерпретацию производных правил вывода (а также интерпретации стабильной допустимости правил и отношения следования между правилами, найденные докладчиком до того, как он узнал о существовании металогики Паулсона). Различие между этими двумя семантиками имеет некоторое отношение к известным разногласиям между Гильбертом и Фреге.