Допустимое правило

В логике правило вывода допустимо в формальной системе , если набор теорем системы не изменяется при добавлении этого правила к существующим правилам системы. Другими словами, каждая формула , которая может быть выведена с использованием этого правила, уже выводима без этого правила, поэтому, в некотором смысле, она избыточна. Понятие допустимого правила было введено Полом Лоренценом (1955).

Определения

Допустимость систематически изучалась только в случае структурных (т.е. замкнутых относительно подстановки ) правил в пропозициональных неклассических логиках , которые мы опишем далее.

Пусть набор основных пропозициональных связок фиксирован (например, в случае суперинтуиционистских логик или в случае мономодальных логик ). Правильно построенные формулы строятся свободно с использованием этих связок из счетно бесконечного набора пропозициональных переменных p ₀ , p ₁ , .... Подстановка σ — это функция из формул в формулы, которая коммутирует с применениями связок, т.е. ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$ ${\displaystyle \{\to ,\bot ,\Box \}}$

${\displaystyle \sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})}$

для каждой связки f и формул A ₁ , ... , A _n . (Мы также можем применять подстановки к наборам Γ формул, делая σ Γ = { σA : A ∈ Γ}. ) Отношение следствия в стиле Тарского ^[1] — это отношение между наборами формул и формулами, такое, что ${\displaystyle \vdash }$

1. ${\displaystyle A\vdash A,}$
2. если то («ослабление») ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \Gamma ,\Delta \vdash A,}$
3. если и тогда («композиция») ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \Delta ,A\vdash B}$ ${\displaystyle \Gamma ,\Delta \vdash B,}$

для всех формул A , B и наборов формул Γ, Δ. Отношение следствия такое, что

4. если тогда ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \sigma \Gamma \vdash \sigma A}$

для всех подстановок σ называется структурным . (Обратите внимание, что термин «структурный», используемый здесь и далее, не связан с понятием структурных правил в секвенциальных исчислениях .) Структурное отношение следования называется пропозициональной логикой . Формула A является теоремой логики , если . ${\displaystyle \vdash }$ ${\displaystyle \varnothing \vdash A}$

Например, мы отождествляем суперинтуиционистскую логику L с ее стандартным отношением следствия, порожденным modus ponens и аксиомами, а нормальную модальную логику — с ее глобальным отношением следствия, порожденным modus ponens, необходимостью и (как аксиомами) теоремами логики. ${\displaystyle \vdash _{L}}$ ${\displaystyle \vdash _{L}}$

Правило структурного вывода ^[2] (или просто правило для краткости) задается парой (Γ, B ), обычно записываемой как

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,}$

где Γ = { A ₁ , ... , A _n } — конечный набор формул, а B — формула. Примером правила является

${\displaystyle \sigma A_{1},\dots ,\sigma A_{n}/\sigma B}$

для подстановки σ . Правило Γ/ B выводимо в , если . Оно допустимо, если для каждого экземпляра правила σB является теоремой всякий раз, когда все формулы из σ Γ являются теоремами. ^[3] Другими словами, правило допустимо, если оно при добавлении к логике не приводит к новым теоремам. ^[4] Мы также пишем , если Γ/ B допустимо. (Заметим, что является структурным отношением следствия само по себе.) ${\displaystyle \vdash }$ ${\displaystyle \Gamma \vdash B}$ ${\displaystyle \Gamma \mathrel {|\!\!\!\sim } B}$ ${\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}$

Каждое выводимое правило допустимо, но не наоборот в общем случае. Логика структурно полна, если каждое допустимое правило выводимо, т.е. . ^[5] ${\displaystyle {\vdash }={\,|\!\!\!\sim }}$

В логиках с хорошо ведущейся связкой конъюнкции (таких как суперинтуиционистская или модальная логика) правило эквивалентно в отношении допустимости и выводимости. Поэтому принято иметь дело только с унарными правилами A / B . ${\displaystyle A_{1},\dots ,A_{n}/B}$ ${\displaystyle A_{1}\land \dots \land A_{n}/B}$

Примеры

• Классическое исчисление высказываний ( CPC ) структурно полно. ^[6] Действительно, предположим, что A / B — невыводимое правило, и зафиксируем присваивание v, такое, что v ( A ) = 1 и v ( B ) = 0. Определим подстановку σ, такую, что для каждой переменной p , σp = если v ( p ) = 1 и σp = если v ( p ) = 0. Тогда σA — теорема, но σB — нет (на самом деле, ¬ σB — теорема). Таким образом, правило A / B также недопустимо. (Тот же аргумент применим к любой многозначной логике L, полной относительно логической матрицы, все элементы которой имеют имя на языке L. ) ${\displaystyle \top }$ ${\displaystyle \bot }$
• Правило Крейзеля - Патнэма (также известное как правило Харропа или правило независимости посылок )

${\displaystyle ({\mathit {KPR}})\qquad {\frac {\neg p\to q\lor r}{(\neg p\to q)\lor (\neg p\to r)}}}$

допустимо в интуиционистском пропозициональном исчислении ( ИПС ). Фактически, оно допустимо в любой суперинтуиционистской логике. ^[7] С другой стороны, формула

${\displaystyle (\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))}$

не является интуиционистской теоремой; следовательно, KPR невыводима в IPC . В частности, IPC не является структурно полной.

• Правило

${\displaystyle {\frac {\Box p}{p}}}$

допустимо во многих модальных логиках, таких как K , D , K 4 , S 4 , GL (см. эту таблицу для названий модальных логик). Оно выводимо в S 4 , но не выводимо в K , D , K 4 или GL .

• Правило

${\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}}$

допустимо в нормальной логике . ^[8] Оно выводимо в GL и S 4.1, но не выводимо в K , D , K 4 , S 4 или S 5. ${\displaystyle L\supseteq S4.3}$

• Правило Лёба

${\displaystyle ({\mathit {LR}})\qquad {\frac {\Box p\to p}{p}}}$

допустимо (но не выводимо) в базовой модальной логике K и выводимо в GL . Однако LR недопустимо в K 4. В частности, в общем случае неверно , что правило, допустимое в логике L, должно быть допустимым в ее расширениях.

• Логика Гёделя –Даммета ( LC ) и модальная логика Grz .3 являются структурно полными. ^[9] Нечеткая логика произведения также является структурно полной. ^[10]

Разрешимость и сокращенные правила

Основной вопрос о допустимых правилах данной логики заключается в том, разрешимо ли множество всех допустимых правил . Обратите внимание, что проблема нетривиальна, даже если сама логика (т. е. ее множество теорем) разрешима : определение допустимости правила A / B включает неограниченный всеобщий квантор по всем пропозициональным подстановкам. Следовательно, априори мы знаем только, что допустимость правила в разрешимой логике (т. е. ее дополнение рекурсивно перечислимо ). Например, известно, что допустимость в бимодальных логиках K _u и K 4 _u (расширения K или K 4 с универсальной модальностью) неразрешима. ^[11] Примечательно, что разрешимость допустимости в базовой модальной логике K является крупной открытой проблемой. ${\displaystyle \Pi _{1}^{0}}$

Тем не менее, известно, что допустимость правил разрешима во многих модальных и суперинтуиционистских логиках. Первые процедуры принятия решений для допустимых правил в базовых транзитивных модальных логиках были построены Рыбаковым с использованием редуцированной формы правил . ^[12] Модальное правило от переменных p ₀ , ... , p _k называется редуцированным, если оно имеет вид

${\displaystyle {\frac {\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j=0}^{k}\neg _{i,j}^{0}p_{j}\land \bigwedge _{j=0}^{k}\neg _{i,j}^{1}\Box p_{j}{\bigr )}}{p_{0}}},}$

где каждое из них либо пустое, либо отрицание . Для каждого правила r мы можем эффективно построить сокращенное правило s (называемое сокращенной формой r ), такое, что любая логика допускает (или выводит) r тогда и только тогда, когда она допускает (или выводит) s , вводя переменные расширения для всех подформул в A и выражая результат в полной дизъюнктивной нормальной форме . Таким образом, достаточно построить алгоритм принятия решения о допустимости сокращенных правил. ${\displaystyle \neg _{i,j}^{u}}$ ${\displaystyle \neg }$

Пусть будет приведенным правилом, как указано выше. Мы отождествляем каждую конъюнкцию с множеством ее конъюнктов. Для любого подмножества W множества всех конъюнкций определим модель Крипке следующим образом: ${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$ ${\displaystyle \varphi _{i}}$ ${\displaystyle \{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}}$ ${\displaystyle \{\varphi _{i}\mid i\leq n\}}$ ${\displaystyle M=\langle W,R,{\Vdash }\rangle }$

${\displaystyle \varphi _{i}\Vdash p_{j}\iff p_{j}\in \varphi _{i},}$

${\displaystyle \varphi _{i}\,R\,\varphi _{i'}\iff \forall j\leq k\,(\Box p_{j}\in \varphi _{i}\Rightarrow \{p_{j},\Box p_{j}\}\subseteq \varphi _{i'}).}$

Тогда следующее дает алгоритмический критерий допустимости в K 4: ^[13]

Теорема . Правило недопустимо в K 4 тогда и только тогда , когда существует множество такое, что ${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$ ${\displaystyle W\subseteq \{\varphi _{i}\mid i\leq n\}}$

1. ${\displaystyle \varphi _{i}\nVdash p_{0}}$для некоторых ${\displaystyle i\leq n,}$
2. ${\displaystyle \varphi _{i}\Vdash \varphi _{i}}$для каждого ${\displaystyle i\leq n,}$
3. для каждого подмножества D из W существуют элементы, такие что эквивалентности ${\displaystyle \alpha ,\beta \in W}$

${\displaystyle \alpha \Vdash \Box p_{j}}$тогда и только тогда, когда для каждого ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ ${\displaystyle \varphi \in D}$

${\displaystyle \alpha \Vdash \Box p_{j}}$тогда и только тогда, когда и для каждого ${\displaystyle \alpha \Vdash p_{j}}$ ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ ${\displaystyle \varphi \in D}$

справедливо для всех j .

Аналогичные критерии можно найти для логик S4 , GL и Grz . ^[14] Более того, допустимость в интуиционистской логике можно свести к допустимости в Grz с помощью перевода Гёделя–МакКинси–Тарского : ^[15]

${\displaystyle A\,|\!\!\!\sim _{IPC}B}$если и только если ${\displaystyle T(A)\,|\!\!\!\sim _{Grz}T(B).}$

Рыбаков (1997) разработал гораздо более сложные методы для демонстрации разрешимости допустимости, которые применяются к надежному (бесконечному) классу транзитивных (т.е. расширяющих K 4 или IPC ) модальных и суперинтуиционистских логик, включая, например, S 4.1, S 4.2, S 4.3, KC , T _k (а также вышеупомянутые логики IPC , K 4, S 4, GL , Grz ). ^[16]

Несмотря на разрешимость, проблема допустимости имеет относительно высокую вычислительную сложность , даже в простых логиках: допустимость правил в базовых транзитивных логиках IPC , K4 , S4 , GL , Grz является coNEXP -полной. ^[17] Это следует противопоставить проблеме выводимости (для правил или формул) в этих логиках, которая является PSPACE -полной. ^[18]

Проективность и унификация

Допустимость в пропозициональных логиках тесно связана с унификацией в эквациональной теории модальных или гейтинговых алгебр . Связь была разработана Гиларди (1999, 2000). В логической установке унификатор формулы A в языке логики L ( сокращенно L -унификатор) — это подстановка σ такая, что σA — теорема L. (Используя это понятие, мы можем перефразировать допустимость правила A / B в L как «каждый L -унификатор A является L -унификатором B ».) L - унификатор σ менее общий , чем L -унификатор τ , записываемый как σ ≤ τ , если существует подстановка υ такая, что

${\displaystyle \vdash _{L}\sigma p\leftrightarrow \upsilon \tau p}$

для каждой переменной p . Полный набор унификаторов формулы A — это набор S L -унификаторов A такой, что каждый L -унификатор A менее общий, чем некоторый унификатор из S . Самый общий унификатор (MGU) A — это унификатор σ такой, что { σ } — полный набор унификаторов A . Отсюда следует, что если S — полный набор унификаторов A , то правило A / B является L -допустимым тогда и только тогда, когда каждый σ в S является L -унификатором B . Таким образом, мы можем охарактеризовать допустимые правила, если мы можем найти хорошо ведущие себя полные наборы унификаторов.

Важным классом формул, имеющих наиболее общий объединитель, являются проективные формулы : это формулы A , такие, что существует объединитель σ формулы A, такой что

${\displaystyle A\vdash _{L}B\leftrightarrow \sigma B}$

для каждой формулы B . Обратите внимание, что σ является МГУ A . В транзитивных модальных и суперинтуиционистских логиках со свойством конечной модели можно семантически охарактеризовать проективные формулы как те, набор конечных L -моделей которых имеет свойство расширения : ^[19] если M является конечной L -моделью Крипке с корнем r , кластер которого является синглетоном , и формула A верна во всех точках M , за исключением r , то мы можем изменить оценку переменных в r так, чтобы сделать A истинной и в r . Более того, доказательство дает явное построение МГУ для заданной проективной формулы A .

В основных транзитивных логиках IPC , K4 , S4 , GL , Grz (и, в более общем смысле, в любой транзитивной логике со свойством конечной модели, множество конечной рамки которой удовлетворяет другому виду свойства расширения) мы можем эффективно построить для любой формулы A ее проективное приближение Π( A ): ^[20] конечное множество проективных формул, такое что

1. ${\displaystyle P\vdash _{L}A}$для каждого ${\displaystyle P\in \Pi (A),}$
2. каждый объединитель A является объединителем формулы из Π( A ).

Отсюда следует, что множество MGU элементов Π( A ) является полным множеством унификаторов A . Кроме того, если P является проективной формулой, то

${\displaystyle P\,|\!\!\!\sim _{L}B}$если и только если ${\displaystyle P\vdash _{L}B}$

для любой формулы B. Таким образом, мы получаем следующую эффективную характеристику допустимых правил: ^[21]

${\displaystyle A\,|\!\!\!\sim _{L}B}$если и только если ${\displaystyle \forall P\in \Pi (A)\,(P\vdash _{L}B).}$

Основы допустимых правил

Пусть L — логика. Множество R L -допустимых правил называется базисом ^[22] допустимых правил, если каждое допустимое правило Γ/ B может быть выведено из R и выводимых правил L с помощью подстановки, композиции и ослабления. Другими словами, R является базисом тогда и только тогда, когда — наименьшее структурное отношение следования, включающее и R . ${\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}}$ ${\displaystyle \vdash _{L}}$

Обратите внимание, что разрешимость допустимых правил разрешимой логики эквивалентна существованию рекурсивных (или рекурсивно перечислимых ) базисов: с одной стороны, множество всех допустимых правил является рекурсивным базисом, если допустимость разрешима. С другой стороны, множество допустимых правил всегда ко-рекурсивно перечислимо, и если у нас далее есть рекурсивно перечислимый базис, множество допустимых правил также рекурсивно перечислимо; следовательно, оно разрешимо. (Другими словами, мы можем решить о допустимости A / B с помощью следующего алгоритма : мы запускаем параллельно два исчерпывающих поиска , один для подстановки σ , которая объединяет A, но не B , и один для вывода A / B из R и . Один из поисков должен в конечном итоге дать ответ.) Помимо разрешимости, явные базы допустимых правил полезны для некоторых приложений, например, при оценке сложности доказательств . ^[23] ${\displaystyle \vdash _{L}}$

Для данной логики мы можем спросить, имеет ли она рекурсивный или конечный базис допустимых правил, и предоставить явный базис. Если логика не имеет конечного базиса, она тем не менее может иметь независимый базис : базис R такой, что ни одно собственное подмножество R не является базисом.

В общем, очень мало можно сказать о существовании баз с желаемыми свойствами. Например, в то время как табличные логики, как правило, хорошо себя ведут и всегда конечно аксиоматизируемы, существуют табличные модальные логики без конечного или независимого базиса правил. ^[24] Конечные базисы относительно редки: даже базовые транзитивные логики IPC , K4 , S4 , GL , Grz не имеют конечного базиса допустимых правил, ^[25] хотя они имеют независимые базисы. ^[26]

Примеры баз

• Пустое множество является базой L -допустимых правил тогда и только тогда, когда L структурно полно.
• Каждое расширение модальной логики S 4.3 (включая, в частности, S 5) имеет конечную основу, состоящую из одного правила ^[27]

${\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}.}$

• Правила Виссера  [nl]

${\displaystyle {\frac {\displaystyle {\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{n+1}\lor p_{n+2}{\Bigr )}\lor r}{\displaystyle \bigvee _{j=1}^{n+2}{\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{j}{\Bigr )}\lor r}},\qquad n\geq 1}$

являются основой допустимых правил в МПК или КС . ^[28]

• Правила

${\displaystyle {\frac {\displaystyle \Box {\Bigl (}\Box q\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (q\land \Box q\to p_{i})\lor r}},\qquad n\geq 0}$

являются основой допустимых правил GL . ^[29] (Обратите внимание, что пустая дизъюнкция определяется как .) ${\displaystyle \bot }$

• Правила

${\displaystyle {\frac {\displaystyle \Box {\Bigl (}\Box (q\to \Box q)\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (\Box q\to p_{i})\lor r}},\qquad n\geq 0}$

являются основой допустимых правил S 4 или Grz . ^[30]

Семантика допустимых правил

Правило Γ/ B справедливо в модальной или интуиционистской системе Крипке , если для каждой оценки в F справедливо следующее : ${\displaystyle F=\langle W,R\rangle }$ ${\displaystyle \Vdash }$

если для всех , то . ${\displaystyle A\in \Gamma }$ ${\displaystyle \forall x\in W\,(x\Vdash A)}$ ${\displaystyle \forall x\in W\,(x\Vdash B)}$

( При необходимости определение легко обобщается на общие рамки .)

Пусть X — подмножество W , а t — точка в W. Мы говорим, что t — это

• рефлексивный плотный предшественник X , если для каждого y в W : t R y тогда и только тогда, когда t = y или для некоторого x в X : x = y или x R y ,
• иррефлексивный плотный предшественник X , если для каждого y из W : t R y тогда и только тогда, когда для некоторого x из X : x = y или x R y .

Мы говорим , что фрейм F имеет рефлексивных (иррефлексивных) плотных предшественников, если для каждого конечного подмножества X из W существует рефлексивный (иррефлексивный) плотный предшественник X в W.

У нас есть: ^[31]

• правило допустимо в МПК тогда и только тогда, когда оно действительно во всех интуиционистских фреймах, имеющих рефлексивных плотных предшественников,
• правило допустимо в K 4 тогда и только тогда, когда оно действительно во всех транзитивных фреймах, имеющих рефлексивных и иррефлексивных плотных предшественников,
• правило допустимо в S 4 тогда и только тогда, когда оно действительно во всех транзитивных рефлексивных фреймах, имеющих рефлексивных плотных предшественников,
• Правило допустимо в GL тогда и только тогда, когда оно действительно во всех транзитивных обратных вполне обоснованных фреймах, имеющих нерефлексивных плотных предшественников.

Обратите внимание, что, за исключением нескольких тривиальных случаев, фреймы с плотными предшественниками должны быть бесконечными. Следовательно, допустимые правила в базовых транзитивных логиках не обладают свойством конечной модели.

Структурная завершенность

Хотя общая классификация структурно полных логик — непростая задача, мы хорошо разбираемся в некоторых частных случаях.

Интуиционистская логика сама по себе не является структурно полной, но ее фрагменты могут вести себя по-разному. А именно, любое правило без дизъюнкций или правило без импликаций, допустимое в суперинтуиционистской логике, выводимо. ^[32] С другой стороны, правило Минца

${\displaystyle {\frac {(p\to q)\to p\lor r}{((p\to q)\to p)\lor ((p\to q)\to r)}}}$

допустимо в интуиционистской логике, но невыводимо и содержит только импликации и дизъюнкции.

Мы знаем максимальные структурно неполные транзитивные логики. Логика называется наследственно структурно полной , если любое расширение структурно полно. Например, классическая логика, а также логики LC и Grz .3, упомянутые выше, являются наследственно структурно полными. Полное описание наследственно структурно полных суперинтуиционистских и транзитивных модальных логик было дано соответственно Циткиным и Рыбаковым. А именно, суперинтуиционистская логика является наследственно структурно полной тогда и только тогда, когда она не верна ни в одной из пяти рамок Крипке ^[9]

Аналогично, расширение K4 является наследственно структурно полным тогда и только тогда, когда оно недействительно ни в одной из двадцати определенных систем Крипке (включая пять интуиционистских систем, указанных выше). ^[9]

Существуют структурно полные логики, которые не являются наследственно структурно полными: например, логика Медведева структурно полна, ^[33] но она входит в структурно неполную логику KC .

Варианты

Правило с параметрами — это правило вида

${\displaystyle {\frac {A(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}{B(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}},}$

чьи переменные делятся на "обычные" переменные p _i и параметры s _i . Правило является L -допустимым, если каждый L -объединитель σ для A такой, что σs _i  =  s _i для каждого i, является также унификатором B . Основные результаты разрешимости для допустимых правил также переносятся на правила с параметрами. ^[34]

Правило множественного вывода — это пара (Γ,Δ) двух конечных наборов формул, записанная как

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B_{1},\dots ,B_{m}}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B_{1},\dots ,B_{m}.}$

Такое правило допустимо, если каждый объединитель Γ является также объединителем некоторой формулы из Δ. ^[35] Например, логика L непротиворечива , если и только если она допускает правило

${\displaystyle {\frac {\;\bot \;}{}},}$

и суперинтуиционистская логика имеет свойство дизъюнкции тогда и только тогда, когда она допускает правило

${\displaystyle {\frac {p\lor q}{p,q}}.}$

Опять же, основные результаты по допустимым правилам легко обобщаются на правила множественного вывода. ^[36] В логиках с вариантом свойства дизъюнкции правила множественного вывода имеют ту же выразительную силу, что и правила единственного вывода: например, в S 4 правило выше эквивалентно

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{\Box B_{1}\lor \dots \lor \Box B_{m}}}.}$

Тем не менее, правила множественных выводов часто можно использовать для упрощения аргументов.

В теории доказательств допустимость часто рассматривается в контексте секвенциальных исчислений , где основными объектами являются секвенции, а не формулы. Например, можно перефразировать теорему об исключении сечения , сказав, что секвенциальное исчисление без сечения допускает правило сечения

${\displaystyle {\frac {\Gamma \vdash A,\Delta \qquad \Pi ,A\vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}.}$

(Иногда, злоупотребляя языком, говорят, что (полное) секвенциальное исчисление допускает разрез, имея в виду его версию без разрезов.) Однако допустимость в секвенциальном исчислении обычно является лишь вариантом обозначения допустимости в соответствующей логике: любое полное исчисление для (скажем) интуиционистской логики допускает правило секвенции тогда и только тогда, когда IPC допускает правило формулы, которое мы получаем, переводя каждую секвенцию в ее характеристическую формулу . ${\displaystyle \Gamma \vdash \Delta }$ ${\displaystyle \bigwedge \Gamma \to \bigvee \Delta }$

Примечания

1. Блок и Пигоцци (1989), Крахт (2007)
2. Рыбаков (1997), Опр. 1.1.3
3. Рыбаков (1997), Опр. 1.7.2
4. От теоремы де Йонга к интуиционистской логике доказательств
5. Рыбаков (1997), Опр. 1.7.7
6. Чагров и Захарьящев (1997), Thm. 1,25
7. Prucnal (1979), см. Iemhoff (2006)
8. Рыбаков (1997), стр. 439
9. Рыбаков (1997), Теория 5.4.4, 5.4.8
10. Синтула и Меткалф (2009)
11. Вольтер и Захарьящев (2008)
12. Рыбаков (1997), §3.9
13. Рыбаков (1997), Теория 3.9.3
14. Рыбаков (1997), Теория 3.9.6, 3.9.9, 3.9.12; ср. Чагров и Захарьящев (1997), §16.7
15. Рыбаков (1997), Теория 3.2.2
16. Рыбаков (1997), §3.5
17. Ержабек (2007)
18. Чагров и Захарьящев (1997), §18.5
19. Гиларди (2000), Теория 2.2
20. Гиларди (2000), стр. 196
21. Гиларди (2000), Теория 3.6
22. Рыбаков (1997), Опр. 1.4.13
23. Минц и Кожевников (2004)
24. Рыбаков (1997), Теория 4.5.5
25. Рыбаков (1997), §4.2
26. Ержабек (2008)
27. Рыбаков (1997), Кор. 4.3.20
28. Йемхофф (2001, 2005), Розьер (1992)
29. Ержабек (2005)
30. Ержабек (2005, 2008)
31. Иемхофф (2001), Ержабек (2005)
32. Рыбаков (1997), Thms. 5.5.6, 5.5.9
33. Прукнал (1976)
34. Рыбаков (1997), §6.1
35. Ержабек (2005); ср. Крахт (2007), §7
36. Ержабек (2005, 2007, 2008)

Ссылки

• В. Блок, Д. Пигоцци, Алгебраизуемые логики , Мемуары Американского математического общества 77 (1989), № 396, 1989.
• А. Чагров и М. Захарьящев, Модальная логика , Oxford Logic Guides т. 35, Oxford University Press, 1997. ISBN  0-19-853779-4
• П. Синтула и Г. Меткалф, Структурная полнота в нечетких логиках , Notre Dame Journal of Formal Logic 50 (2009), № 2, стр. 153–182. doi :10.1215/00294527-2009-004
• А.И. Циткин, О структурно полных суперинтуиционистских логиках , Советская математика - Доклады, т. 19 (1978), с. 816–819.
• S. Ghilardi, Унификация в интуиционистской логике , Журнал символической логики 64 (1999), № 2, стр. 859–880. Проект Euclid JSTOR
• S. Ghilardi, Лучшее решение модальных уравнений , Annals of Pure and Applied Logic 102 (2000), № 3, стр. 183–198. doi :10.1016/S0168-0072(99)00032-9
• Р. Йемхофф , О допустимых правилах интуиционистской пропозициональной логики , Журнал символической логики 66 (2001), № 1, стр. 281–294. Проект Евклид JSTOR
• Р. Йемхофф, Промежуточные логики и правила Виссера , Notre Dame Journal of Formal Logic 46 (2005), № 1, стр. 65–81. doi :10.1305/ndjfl/1107220674
• Р. Иемхофф, О правилах промежуточной логики , Архив математической логики , 45 (2006), № 5, стр. 581–599. doi :10.1007/s00153-006-0320-8
• Э. Ержабек, Допустимые правила модальной логики , Журнал логики и вычислений 15 (2005), № 4, стр. 411–431. doi :10.1093/logcom/exi029
• Э. Ержабек, Сложность допустимых правил , Архив математической логики 46 (2007), № 2, стр. 73–92. doi :10.1007/s00153-006-0028-9
• Э. Ержабек, Независимые основания допустимых правил , Logic Journal of the IGPL 16 (2008), № 3, стр. 249–267. doi :10.1093/jigpal/jzn004
• M. Kracht, Modal Consequence Relations , в: Handbook of Modal Logic (P. Blackburn, J. van Benthem, and F. Wolter, eds.), Studies of Logic and Practical Reasoning, т. 3, Elsevier, 2007, стр. 492–545. ISBN 978-0-444-51690-9 
• П. Лоренцен, Einführung in die оперативной логике и математике , Grundlehren der mathematischen Wissenschaften vol. 78, Спрингер-Верлаг, 1955.
• Минц Г., Кожевников А., Интуиционистские системы Фреге полиномиально эквивалентны , Записки научных семинаров ПОМИ 316 (2004), стр. 129–146. сжатый PS
• Т. Прукнал, Структурная полнота исчисления высказываний Медведева , Отчеты по математической логике 6 (1976), стр. 103–105.
• T. Prucnal, О двух проблемах Харви Фридмана , Studia Logica 38 (1979), № 3, стр. 247–262. doi :10.1007/BF00405383
• П. Розьер, «Правила, допустимые в интуитивных вычислениях» , доктор философии. диссертация, Парижский университет VII , 1992. PDF
• В. В. Рыбаков, Допустимость правил логического вывода , Исследования по логике и основаниям математики, т. 136, Elsevier, 1997. ISBN 0-444-89505-1 
• Ф. Вольтер, М. Захарьящев, Неразрешимость проблем унификации и допустимости для модальных и дескриптивных логик , ACM Transactions on Computational Logic 9 (2008), № 4, статья № 25. doi :10.1145/1380572.1380574 PDF