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

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





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








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


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

С. А. Мелихов

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

Аннотация: По смыслу это будет несколько запоздавшим продолжением моего доклада в мае, но по форме - независимым докладом (т.е. знакомство с содержанием прошлых серий не требуется).
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$ интерпретируются классически, причём двузначно, притом, что сами они - интуиционистские. Ничто не мешает рассматривать "многозначную" семантику Тарского, в которой не только связки и кванторы, но также и метасвязки и метакванторы могут интерпретироваться многозначно. Например, если объектная логика - интуиционистская, оператор рефлексии ! может интерпретироваться подходящим отображением между топологическими пространствами, в одном из которых интерпретируются связки и кванторы, а в другом - метасвязки и метакванторы.
Но более интересна альтернативная теория моделей, основанная, в частности, на другом понимании семантического следования - по Колмогорову (входящем в его оригинальную задачную интерпретацию интуиционистской логики). Альтернативные интерпретации металогики тоже бывают "двузначные" и "многозначные" (не только на объектном, но и на мета-уровне). Более того, в альтернативном случае, с интуиционистской объектной логикой, оказывается вполне содержательной ситуация, в которой метасвязки и метакванторы интерпретируются по существу так же, как и соответствующие связки и квантор всеобщности. Это позволяет, наконец, придать некоторый вполне формальный смысл всей задачной интерпретации Колмогорова.
В том, что касается интерпретации формул и принципов, все рассматриваемые варианты обобщённых моделей логик по существу сводятся к обычным. Они ведут себя иначе лишь в части интерпретации правил (а также более сложных металогических конструкций, как, например, импликации между принципами). Это вполне относится, например, к топологическим моделям интуиционистской логики, но про "модели" реализуемостного типа (включая, например, "финитные задачи" Медведева) лучше сказать иначе: если их понимать как альтернативные модели, это ничего не меняет в том, какие в них выполняются принципы, но позволяет дать хоть какое-то разумное определение выполнения правил в таких моделях. Имеются и другие интересные примеры альтернативных моделей, в том числе, когда объектная логика - классическая.

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