RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Ближайшие семинары
Календарь семинаров
Список семинаров
Архив по годам
Регистрация семинара

Поиск
RSS
Ближайшие семинары





Для просмотра файлов Вам могут потребоваться








Семинар отдела математической логики «Теория доказательств»
16 мая 2016 г., г. Москва, МИАН, ауд. 530
 


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

С. А. Мелихов

Количество просмотров:
Эта страница:87

Аннотация: Рассматривается металогика Л.Полсона, в терминах которой в известном пруфчекере 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-интерпретации интуиционистской логики, включающее данную самим Колмогоровым интерпретацию производных правил вывода (а также интерпретации стабильной допустимости правил и отношения следования между правилами, найденные докладчиком до того, как он узнал о существовании металогики Паулсона). Различие между этими двумя семантиками имеет некоторое отношение к известным разногласиям между Гильбертом и Фреге.

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019