Промежуточная логика

В математической логике суперинтуиционистская логика — это пропозициональная логика , расширяющая интуиционистскую логику . Классическая логика — самая сильная последовательная суперинтуиционистская логика; таким образом, последовательные суперинтуиционистские логики называются промежуточными логиками (логики являются промежуточными между интуиционистской логикой и классической логикой). ^[1]

Суперинтуиционистская логика — это множество L пропозициональных формул в счетном множестве переменных p _{i ,} удовлетворяющее следующим свойствам:

1. все аксиомы интуиционистской логики принадлежат L ;

2. если F и G — формулы такие, что F и F → ​​G обе принадлежат L , то G также принадлежит L (замкнутость относительно modus ponens );

3. если F ( p ₁ , p ₂ , ..., p _n ) является формулой языка L , а G ₁ , G ₂ , ..., G _n являются любыми формулами, то F ( G ₁ , G ₂ , ..., 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)

• Логика Гёделя-Даммета ( Даммет 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 ₂ , см. обобщения ниже. Сравните с p ∨ ( p → q )):

= МПК + p ∨ ( p → ( 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 ₂ . Аналогично, например, 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 ₂ ∨ ( p ₂ → ( p ₁ ∨ ¬ p ₁ )))...)))

• Гёделевские n -значные логики ( G _n ):

ЛК + БД _{n −1}

= ЛК + ВС _{n −1}

• логики ограниченной мощности ( BC _n ):

${\displaystyle \textstyle \mathbf {МПК} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to p_{i}{\bigr )}}$

• логика ограниченной верхней ширины ( BTW _n ):

${\displaystyle \textstyle \mathbf {МПК} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to \neg \neg p_{i}{\bigr )}}$

• логики ограниченной ширины, также известные как логика ограниченных антицепей, Оно (1972) ( БВ _n , БА _n ):

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j\neq i}p_{j}\to p_{i}{\bigr )}}$

• логика ограниченного ветвления, Габбей и де Йонг (1969, 1974) ( T _n , BB _n ):

${\displaystyle \textstyle \mathbf {МПК} +\bigwedge _{i=0}^{n}{\bigl (}{\bigl (}p_{i}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{i=0}^{n}p_{i}}$

Более того:

• Логика реализуемости
• Логика конечных задач Медведева ( LM , ML ): ^{[3] [4] [5]} семантически определенная как логика всех фреймов вида для конечных множеств X («булевы гиперкубы без вершины»), не известная как рекурсивно аксиоматизируемая${\displaystyle \langle {\mathcal {P}}(X)\setminus \{X\},\subseteq \rangle }$
• ...

Пропозициональные логики SL и KP имеют свойство дизъюнкции DP. Логика реализуемости Клини и сильная логика Медведева также имеют его. Не существует уникальной максимальной логики с DP на решетке. Обратите внимание, что если непротиворечивая теория подтверждает WPEM, но все еще имеет независимые утверждения при допущении PEM, то она не может иметь DP.

Если задана алгебра Гейтинга H , множество пропозициональных формул , действительных в H, является промежуточной логикой. Наоборот, если задана промежуточная логика, можно построить ее алгебру Линденбаума–Тарского , которая затем является алгеброй Гейтинга.

Интуиционистская шкала Крипке F — это частично упорядоченное множество , а модель Крипке M — это шкала Крипке с оценкой, такая что является верхним подмножеством F. Множество пропозициональных формул, которые действительны в F, является промежуточной логикой. При наличии промежуточной логики L можно построить модель Крипке M, такую, что логика M будет L (эта конструкция называется канонической моделью ). Шкала Крипке с этим свойством может и не существовать, но общая шкала всегда существует.${\displaystyle \{x\mid M,x\Vdash p\}}$

Пусть A — пропозициональная формула. Трансляция Гёделя– Тарского формулы A определяется рекурсивно следующим образом:

• ${\displaystyle T(p_{n})=\Box p_{n}}$
• ${\displaystyle T(\отрицательный A)=\Box \отрицательный T(A)}$
• ${\displaystyle T(A\land B)=T(A)\land T(B)}$
• ${\displaystyle T(A\vee B)=T(A)\vee T(B)}$
• ${\displaystyle T(A\to B)=\Box (T(A)\to T(B))}$

Если M — модальная логика, расширяющая S4 , то ρ M = { A | T ( A ) ∈ M } — суперинтуиционистская логика, и M называется модальным компаньоном ρ M . В частности:

• МПК = ρ S4
• КС = ρ S4.2
• ЛК = ρ S4.3
• КПК = ρ S5

Для каждой промежуточной логики L существует множество модальных логик M таких, что L  = ρ M .

• Список логических систем

• Чагров, Александр; Захарьящев, Михаил (1997). Модальная логика . Оксфорд: Clarendon Press . С. 605. ISBN 9780198537793.

• Медведев, Ю. Т. (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) Сью Энн Уокер

• Тервейн, Себастьян А. (2006). «Конструктивная логика и решетка Медведева». Журнал формальной логики Нотр-Дама . 47 (1): 73–82. дои : 10.1305/ndjfl/1143468312.

• Умэдзава, Тосио (июнь 1959 г.). «О логиках, промежуточных между интуиционистской и классической логикой предикатов». Журнал символической логики . 24 (2): 141–153. doi :10.2307/2964756. JSTOR  2964756. S2CID  13357205.

• «Промежуточная логика», Энциклопедия математики , EMS Press , 2001 [1994]