Структурное правило

Правило математической логики

В логической дисциплине теории доказательств структурное правило — это правило вывода исчисления последовательностей , которое не ссылается ни на одну логическую связку , а вместо этого напрямую работает с последовательностями . ^{[1] [2]} Структурные правила часто имитируют предполагаемые метатеоретические свойства логики. Логики, отрицающие одно или несколько структурных правил, классифицируются как субструктурные логики .

Общие структурные правила

Три общих структурных правила: ^[3]

• Ослабление , где гипотезы или заключение последовательности могут быть расширены дополнительными членами. В символической форме правила ослабления могут быть записаны как слева от турникета , так и справа. Известно как монотонность вывода в классической логике. ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}}$
• Сокращение , когда два равных (или унифицируемых) члена на одной стороне секвенции могут быть заменены одним членом (или общим экземпляром). Символически: и . Также известно как факторизация в автоматизированных системах доказательства теорем с использованием резолюции . Известно как идемпотентность вывода в классической логике. ${\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}$
• Обмен , где два члена на одной стороне секвенции могут быть обменены. Символически: и . (Это также известно как правило перестановки .) ${\displaystyle {\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}}$

Логика без каких-либо из вышеперечисленных структурных правил интерпретировала бы стороны секвенции как чистые последовательности ; при обмене их можно рассматривать как мультимножества ; а при сокращении и обмене их можно рассматривать как множества .

Это не единственные возможные структурные правила. Известное структурное правило известно как разрез . ^[1] Значительные усилия тратятся теоретиками доказательств на то, чтобы показать, что правила разреза излишни в различных логиках. Точнее, показано, что разрез является лишь (в некотором смысле) инструментом для сокращения доказательств и не добавляется к теоремам, которые могут быть доказаны. Успешное «удаление» правил разреза, известное как устранение разреза , напрямую связано с философией вычисления как нормализации (см. соответствие Карри–Ховарда ); оно часто дает хорошее представление о сложности решения данной логики.

Смотрите также

• Аффинная логика  – субструктурная логика, теория доказательств которой отвергает структурное правило сокращения.Страницы, отображающие описания викиданных в качестве резерва
• Линейная логика  – Система ресурсо-ориентированной логики
• Упорядоченная логика (линейная логика)
• Релевантная логика  – математическая логическая система, которая накладывает определенные ограничения на импликацию.Страницы, отображающие описания викиданных в качестве резерва
• Логика разделения

Ссылки

1. Генцен, Герхард (1935). «Untersuchungen über das logische Schließen. I, Mathematische Zeitschrift». Mathematische Zeitschrift (на немецком языке). 39 (1): 176–210. дои : 10.1007/BF01201353. ISSN  0025-5874.
2. Szabo, ME (1969). Сборник статей Герхарда Генцена . Место издания не указано: Elsevier. ISBN 978-0-444-53419-4.
3. Якобс, Барт (1994). «Семантика ослабления и сжатия». Annals of Pure and Applied Logic . 69 (1): 73–106. doi :10.1016/0168-0072(94)90020-5.