Loading AI tools
класс логических исчислений, использующих древовидный вывод и секвенции (условные суждения) Из Википедии, свободной энциклопедии
Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций . Наиболее известные исчисления секвенций — и для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.
В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведётся в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к генценовскому типу, в противоположность аксиоматическим гильбертовским исчислениям[англ.], в которых при развитом наборе аксиом количество правил вывода сведено к минимуму.
Основное свойство секвенциальной формы — симметричное устройствоустранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств.
, обеспечивающее удобство доказательстваПонятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц (нем. Paul Hertz; 1881–1940)[1], но целостного исчисления для какой-либо логической теории в его трудах построено не было[2]. В работе 1932 года Генцен попытался развить подход Герца[3], но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода и для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы и . Для и Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта трансфинитной индукцией до ординала . Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.
Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Ойвой Кетоненом (фин. Oiva Ketonen; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости[4][5]. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа[6][7].
В 1952 году Стивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода[8], там же ввёл исчисления генценовского типа и , в которых не требовались структурные правила вывода[9], и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов[4].
Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Гаиси Такеути (яп. 竹内外史; 1926—2017) построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Уильям Тэйт (англ. род. 1929) доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси[10] и Дага Правица (швед. Dag Prawitz; род. 1936). В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Жирар[фр.] — для системы F.
Начиная с 1980-х годов секвенциальные системы играют ключевую роль в развитии систем автоматического доказательства, в частности, разработанное Тьерри Коканом и Жераром Юэ в 1986 году секвенциальное исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта — используется как основа программной системы Coq.
Секвенцией называется выражение вида , где и — конечные (возможно пустые) последовательности логических формул, называемые цедентами: — антецедентом, а — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию — если выполнена конъюнкция формул антецедента , то имеет место (выводится) дизъюнкция формул сукцедента . Иногда вместо стрелки в обозначении секвенции используется знак выводимости () или знак импликации ().
Если антецедент пуст (), то подразумевается выполнение дизъюнкции формул сукцедента ; пустой сукцедент () интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде или , где — последовательность формул, а — формула, означает добавление формулы в цедент (возможно, в ещё одном экземпляре).
Аксиомами считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях и задаётся только одна схема аксиом — . Правила вывода в секвенциальной форме записываются как следующие выражения:
интерпретируются они как утверждение о выводимости из верхней секвенции (верхних секвенций и ) нижней секвенции . Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:
где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции , означает её выводимость в данной логической системе: .
Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система , построенная Генценом в 1934 году. В системе одна схема аксиом — и 21 правило вывода, которые делятся на структурные и логические[11].
Структурные правила (, — формулы, , , , — списки формул):
Логические пропозициональные правила предназначены для добавления в вывод пропозициональных связок:
Логические кванторные правила вводят кванторы всеобщности и существования в вывод ( — формула со свободной переменной , — произвольный терм, а — замена всех вхождений свободной переменной на терм ):
Дополнительное условие в кванторных правилах — невхождение свободной переменной в нижние формулы секвенций в правилах -справа и -слева.
Пример -вывода закона исключённого третьего:
— в нём вывод начат с единственной аксиомы, далее — последовательно применены правила -справа, -справа, перестановка справа, -справа и сокращение справа.
Исчисление эквивалентно классическому исчислению предикатов первой ступени: формула общезначима в исчислении предикатов тогда и только тогда, когда в выводима секвенция . Ключевой результат, который назван Генценом «основной теоремой» (нем. Hauptsatz) — возможность провести любой -вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства , в том числе корректность, непротиворечивость и полнота.
Исчисление получается из добавлением ограничения на сукцеденты секвенций в правилах вывода: в них допустимо использование только одной формулы, а правила перестановки справа и сокращения справа (оперирующие с нескольким формулами в сукцедентах) исключаются. Таким образом, при минимальных модификациях получается система, в которой невыводимы законы двойного отрицания и исключённого третьего, но действуют все прочие основные логические законы, и, например, выводима эквивалентность . Полученная система эквивалентна интуиционистскому исчислению предикатов с аксиоматикой Гейтинга. В исчислении также устранимы сечения, оно также корректно, непротиворечиво и полно, притом последний результат для интуиционистского исчисления предикатов впервые получен именно для .
Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса (англ. Patrick Suppes; 1922–2014) 1957 года[12] (почерпнутая из замечаний Фейса[англ.] и Ладриера[фр.] к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Леммоном (англ. John Lemmon; 1930–1966)[13], устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена[14]. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом (нем. Hans Hermes; 1912–2003)[15]: в его системе для классической логики применены две аксиомы ( и , а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях[16].
Этот раздел не завершён. |
Секвенциальным исчислениям присуща симметрия, естественно выражающая двойственность, в аксиоматических теориях формулируемую законами де Моргана.
Этот раздел не завершён. |
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.