Промежуточная логика
В математической логике суперинтуиционистская логика — это логика высказываний, расширяющая интуиционистскую логику . Классическая логика — это сильнейшая непротиворечивая суперинтуиционистская логика; таким образом, непротиворечивые суперинтуиционистские логики называются промежуточными логиками (логики занимают промежуточное положение между интуиционистской логикой и классической логикой). [1]
Определение [ править ]
Суперинтуиционистская логика — это множество L пропозициональных формул в счетном множествепеременные p i, удовлетворяющие следующим свойствам:
- 1. все аксиомы интуиционистской логики принадлежат L ;
- 2. если F и G — формулы такие, что F и F → G обе принадлежат L , то G также принадлежит L (замыкание относительно modus ponens );
- если F ( p1 произвольные , p2 , ..., pn ) формула L а G1 3. , G2 ( ,..., — Gn формулы, F то G1 , , G2 , — ..., G n ) принадлежит L (замыкание при замене).
Такая логика является промежуточной, если, кроме того,
- 4. L не является множеством всех формул.
Свойства и примеры [ править ]
Существует континуум различных промежуточных логик, и столько же таких логик обладают свойством дизъюнкции (DP). Суперинтуиционистские или промежуточные логики образуют полную решетку, в которой интуиционистская логика находится внизу , а противоречивая логика (в случае суперинтуиционистских логик) или классическая логика (в случае промежуточных логик) — наверху. Классическая логика — единственный слой в решетке суперинтуиционистских логик; решетка промежуточных логик также имеет уникальный коатом, а именно SmL [ нужна ссылка ] .
Инструменты для изучения промежуточной логики аналогичны тем, которые используются для интуиционистской логики, например семантики Крипке . Например, логика Гёделя-Даммета имеет простую семантическую характеристику в терминах общего количества порядков . Конкретная промежуточная логика может быть задана посредством семантического описания.
Другие часто задаются путем добавления одной или нескольких аксиом к
- Интуиционистская логика (обычно обозначается как интуиционистское исчисление высказываний IPC , но также Int , IL или H )
Примеры включают в себя:
- Классическая логика ( CPC , Cl , CL ):
- = IPC + ¬¬ p → p (исключение двойного отрицания, DNE)
- = IPC + (¬ p → p ) → p ( Чудесное последствие )
- = IPC + p ∨ ¬ p ( Принцип исключенного третьего , PEM)
Обобщенные варианты вышесказанного (но фактически эквивалентные принципы по сравнению с интуиционистской логикой) таковы, соответственно:
- = IPC + (¬ p → ¬ q ) → ( q → p ) обратного противопоставления ) ( принцип
- = IPC + (( p → q ) → p ) → p ( принцип Пирса PP, сравните с Consequencia mirabilis)
- = IPC + ( q → p ) → ((¬ q → p ) → p ) (еще одна схема, обобщающая чудесное следствие)
- = IPC + p ∨ ( p → q ) (следуя ПЭМ по принципу взрыва )
- Логика Сметанича ( SmL ):
- = IPC + (¬ q → p ) → ((( p → q ) → p ) → p ) (условное ПП)
- Логика Гёделя-Даммета ( Dummett 1959) ( LC или G , см. расширения ниже):
- = 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 )):
- = МПК + п ∨ ( п → ( q ∨ ¬ q ))
- Янкова (1968) Логика [2] или Де Моргана логика ( KC ):
- = 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-й закон Де Моргана )
- Скотта Логика ( SL ):
- = 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 -значные логики ( G n ):
- ЛК + БД n −1
- = LC + BC n −1
- логики ограниченной мощности ( BC n ):
- логика ограниченной ширины вершины ( кстати n ):
- логики ограниченной ширины, также известные как логика ограниченных антицепей, Оно (1972) ( BW n , BA n ):
- логика ограниченного ветвления, Габбай и де Йонг (1969, 1974) ( T n , BB n ):
Более того:
- реализуемости Логика
- ЛМ Логика конечных задач Медведева ( , МЛ ) : [3] [4] [5] семантически определяется как логика всех фреймов формы для конечных множеств 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
- LC = ρ S4.3
- КПК = ρ S5
Для каждой промежуточной логики L существует множество модальных логик M таких, что L = ρ M .
См. также [ править ]
Примечания [ править ]
- ^ «Промежуточная логика» , Математическая энциклопедия , EMS Press , 2001 [1994] .
- ^ Тервейн 2006 .
- ^ Медведев 1962 .
- ^ Медведев 1963 .
- ^ Медведев 1966 .
Ссылки [ править ]
- Чагров, Александр; Захарьящев, Михаил (1997). Модальная логика . Оксфорд: Кларендон Пресс . п. 605. ИСБН 9780198537793 .
- Медведев Ю Т. (1962). «[Конечные задачи]» (PDF) . Советская математика (на русском языке). 3 (1): 227–230. дои : 10.2307/2272084 . JSTOR 2272084 .
Английский перевод XXXVIII 356 (20) Эллиота Мендельсона.
- Медведев Ю Т. (1963). «[Интерпретация логических формул посредством конечных задач и ее связь с теорией читаемости]» (PDF) . Советская математика (на русском языке). 4 (1): 180–183. дои : 10.2307/2272084 . JSTOR 2272084 .
Английский перевод XXXVIII 356 (21), сделанный Сью Энн Уокер.
- Медведев Ю Т. (1966). «[Интерпретация логических формул посредством конечных задач]» (PDF) . Советская математика (на русском языке). 7 (4): 857–860. дои : 10.2307/2272084 . JSTOR 2272084 .
Английский перевод XXXVIII 356 (22) Сью Энн Уокер
- Тервейн, Себастьян А. (2006). «Конструктивная логика и решетка Медведева» . Журнал формальной логики Нотр-Дама . 47 (1): 73–82. дои : 10.1305/ndjfl/1143468312 .
- Умедзава, Тосио (июнь 1959 г.). «О логике, промежуточной между интуиционистской и классической логикой предикатов». Журнал символической логики . 24 (2): 141–153. дои : 10.2307/2964756 . JSTOR 2964756 . S2CID 13357205 .
Внешние ссылки [ править ]
- «Промежуточная логика» , Энциклопедия математики , EMS Press , 2001 [1994]