Пропозициональная логика, расширяющая интуиционистскую логику
В математической логике суперинтуиционистская логика — это пропозициональная логика , расширяющая интуиционистскую логику . Классическая логика — самая сильная последовательная суперинтуиционистская логика; таким образом, последовательные суперинтуиционистские логики называются промежуточными логиками (логики являются промежуточными между интуиционистской логикой и классической логикой). [1]
Определение
Суперинтуиционистская логика — это множество L пропозициональных формул в счетном множестве переменных p i , удовлетворяющее следующим свойствам:
- 1. все аксиомы интуиционистской логики принадлежат L ;
- 2. если F и G — формулы такие, что F и F → G обе принадлежат L , то G также принадлежит L (замкнутость относительно modus ponens );
- 3. если F ( p 1 , p 2 , ..., p n ) является формулой языка L , а G 1 , G 2 , ..., G n являются любыми формулами, то F ( G 1 , G 2 , ..., G n ) принадлежит языку L (замкнутость относительно подстановки).
Такая логика является промежуточной, если к тому же
- 4. L не является множеством всех формул.
Свойства и примеры
Существует континуум различных промежуточных логик, и столько же таких логик демонстрируют свойство дизъюнкции (DP). Суперинтуиционистские или промежуточные логики образуют полную решетку с интуиционистской логикой в качестве основания и непоследовательной логикой (в случае суперинтуиционистских логик) или классической логикой (в случае промежуточных логик) в качестве вершины. Классическая логика является единственным коатомом в решетке суперинтуиционистских логик; решетка промежуточных логик также имеет уникальный коатом, а именно SmL [ требуется цитата ] .
Инструменты для изучения промежуточных логик аналогичны тем, которые используются для интуиционистской логики, например, семантика Крипке . Например, логика Гёделя–Даммета имеет простую семантическую характеристику в терминах полных порядков . Конкретные промежуточные логики могут быть заданы семантическим описанием.
Другие часто даются путем добавления одной или нескольких аксиом к
- Интуиционистская логика (обычно обозначается как интуиционистское пропозициональное исчисление IPC , но также Int , IL или H )
Вот несколько примеров:
- Классическая логика ( КПЛ , КЛ , КЛ ):
- = IPC + ¬¬ p → p (Устранение двойного отрицания, DNE)
- = IPC + (¬ p → p ) → p ( Consequentia mirabilis )
- = IPC + p ∨ ¬ p ( Принцип исключенного третьего , PEM)
Обобщенные варианты вышеизложенного (но фактически эквивалентные принципы интуиционистской логики) — это, соответственно,
- = IPC + (¬ p → ¬ q ) → ( q → p ) ( принцип обратного противопоставления )
- = IPC + (( p → q ) → p ) → p ( принцип Пирса PP, сравните с Consequentia mirabilis)
- = IPC + ( q → p ) → ((¬ q → p ) → p ) (еще одна схема, обобщающая Consequentia mirabilis)
- = IPC + p ∨ ( p → q ) (следует из PEM по принципу взрыва )
- Логика Сметанича ( SmL ):
- = IPC + (¬ q → p ) → ((( p → q ) → p ) → p ) (условный PP)
- = IPC + ( p → q ) ∨ ( q → p ) (принцип Дирка Джентли, DGP или линейность)
- = IPC + ( p → ( q ∨ r )) → (( p → q ) ∨ ( p → r )) (форма независимости предпосылки IP)
- = IPC + (( p ∧ q ) → r ) → (( p → r ) ∨ ( q → r )) (Обобщенный 4-й закон Де Моргана )
- Ограниченная глубина 2 ( BD 2 , см. обобщения ниже. Сравните с p ∨ ( p → q )):
- = МПК + p ∨ ( p → ( q ∨ ¬ q ))
- = IPC + ¬¬ p ∨ ¬ p (слабый PEM, он же WPEM)
- = IPC + ( p → q ) ∨ (¬ p → ¬ q ) (слабый DGP)
- = IPC + ( p → ( q ∨ ¬ r )) → (( p → q ) ∨ ( p → ¬ r )) (вариант, с отрицанием, формы IP)
- = IPC + ¬( p ∧ q ) → (¬ q ∨ ¬ p ) (4-й закон Де Моргана )
- = IPC + ((¬¬ p → p ) → ( p ∨ ¬ p )) → (¬¬ p ∨ ¬ p ) (условный WPEM)
- = IPC + (¬ p → ( q ∨ r )) → ((¬ p → q ) ∨ (¬ p → r )) (другой вариант, с отрицанием, формы IP)
Этот список, по большей части, не является каким-либо упорядочением. Например, известно , что LC не доказывает все теоремы SmL , но он не сравнивается напрямую по силе с BD 2 . Аналогично, например, KP не сравнивается с SL . Список равенств для каждой логики также ни в коем случае не является исчерпывающим. Например, как и в случае с WPEM и законом Де Моргана, можно выразить несколько форм DGP с использованием конъюнкции.
Даже (¬¬ p ∨ ¬ p ) ∨ (¬¬ p → p ), дальнейшее ослабление WPEM, не является теоремой IPC .
Также стоит отметить, что, принимая всю интуиционистскую логику как должное, равенства в значительной степени опираются на взрыв. Например, по сравнению с простой минимальной логикой , как принцип PEM уже эквивалентен Consequentia mirabilis, но не подразумевает более сильного DNE, ни PP, и не сопоставим с DGP.
Продолжается:
- логики ограниченной глубины ( BD n ):
- IPC + p n ∨ ( p n → ( p n −1 ∨ ( p n −1 → ... → ( p 2 ∨ ( p 2 → ( p 1 ∨ ¬ p 1 )))...)))
- ЛК + БД n −1
- = ЛК + ВС n −1
- логики ограниченной мощности ( BC n ):
- логика ограниченной верхней ширины ( BTW n ):
- логики ограниченной ширины, также известные как логика ограниченных антицепей, Оно (1972) ( БВ n , БА n ):
- логика ограниченного ветвления, Габбей и де Йонг (1969, 1974) ( T n , BB n ):
Более того:
- Логика реализуемости
- Логика конечных задач Медведева ( LM , ML ): семантически определенная как логика всех фреймов вида для конечных множеств X («булевы гиперкубы без вершины»), не известная как рекурсивно аксиоматизируемая
- ...
Пропозициональные логики SL и KP имеют свойство дизъюнкции DP. Логика реализуемости Клини и сильная логика Медведева также имеют его. Не существует уникальной максимальной логики с DP на решетке. Обратите внимание, что если непротиворечивая теория подтверждает WPEM, но все еще имеет независимые утверждения при допущении PEM, то она не может иметь DP.
Семантика
Если задана алгебра Гейтинга H , множество пропозициональных формул , действительных в H, является промежуточной логикой. Наоборот, если задана промежуточная логика, можно построить ее алгебру Линденбаума–Тарского , которая затем является алгеброй Гейтинга.
Интуиционистская шкала Крипке F — это частично упорядоченное множество , а модель Крипке M — это шкала Крипке с оценкой, такая что является верхним подмножеством F. Множество пропозициональных формул, которые действительны в F, является промежуточной логикой. При наличии промежуточной логики L можно построить модель Крипке M, такую, что логика M будет L (эта конструкция называется канонической моделью ). Шкала Крипке с этим свойством может и не существовать, но общая шкала всегда существует.
Отношение к модальным логикам
Пусть A — пропозициональная формула. Трансляция Гёделя– Тарского формулы A определяется рекурсивно следующим образом:
Если M — модальная логика, расширяющая S4 , то ρ M = { A | T ( A ) ∈ M } — суперинтуиционистская логика, и M называется модальным компаньоном ρ M . В частности:
- МПК = ρ S4
- КС = ρ S4.2
- ЛК = ρ S4.3
- КПК = ρ S5
Для каждой промежуточной логики L существует множество модальных логик M таких, что L = ρ M .
Смотрите также
Примечания
Ссылки
- Медведев, Ю. Т. (1962). "[Конечные задачи]" (PDF) . Советская математика . 3 (1): 227–230. doi :10.2307/2272084. JSTOR 2272084.
Английский перевод XXXVIII 356(20) Эллиота Мендельсона.
- Медведев, Ю. Т. (1963). "[Интерпретация логических формул с помощью конечных задач и ее связь с теорией читаемости]" (PDF) . Советская математика . 4 (1): 180–183. doi :10.2307/2272084. JSTOR 2272084.
Английский перевод XXXVIII 356(21) Сью Энн Уокер.
- Медведев, Ю. Т. (1966). "[Интерпретация логических формул с помощью конечных задач]" (PDF) . Советская математика . 7 (4): 857–860. doi :10.2307/2272084. JSTOR 2272084.
Английский перевод XXXVIII 356(22) Сью Энн Уокер
- Умэдзава, Тосио (июнь 1959 г.). «О логиках, промежуточных между интуиционистской и классической логикой предикатов». Журнал символической логики . 24 (2): 141–153. doi :10.2307/2964756. JSTOR 2964756. S2CID 13357205.
Внешние ссылки