Лекция
Привет, Вы узнаете о том , что такое секвенция, Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое секвенция, исчисление секвенций , настоятельно рекомендую прочитать все из категории Теория цифровых автоматов.
секвенция (англ. sequention) — упорядоченная двоичная последовательность в асинхронной секвенциальной логике.
Секвенция (теория доказательств) (англ. sequent, нем. sequenz) — формула генценовской системы исчисления в теории доказательств.
Секвенцией называется выражение вида 
, где 
и 
— конечные (возможно пустые) последовательности логических формул, называемые цедентами: — антецедентом, а — сукцедентом (иногда — консеквентом) Интуитивный смысл, закладываемый в секвенцию 
— если выполнена конъюнкция формул антецедента 
, то имеет место (выводится) дизъюнкция формул сукцедента 
. Иногда вместо стрелки в обозначении секвенции используется знак выводимости (
) или знак импликации (
).
Если антецедент пуст (
), то подразумевается выполнение дизъюнкции формул сукцедента ; пустой сукцедент (
) интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция 
означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде 
или 
, где — последовательность формул, а 
— формула, означает добавление формулы в цедент (возможно, в еще одном экземпляре).
Аксиомами считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях 
и 
задается только одна схема аксиом — 
. Правила вывода в секвенциальной форме записываются как следующие выражения:
и 
,
интерпретируются они как утверждение о выводимости из верхней секвенции 
(верхних секвенций и 
) нижней секвенции 
. Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:
,
где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции 
, означает ее выводимость в данной логической системе: 
.
исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций[⇨]. Наиболее известные исчисления секвенций — 
[⇨] и 
[⇨] для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.
В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведется в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к генценовскому типу, в противоположность аксиоматическим гильбетровским исчислениям[en], в которых при развитом наборе аксиом количество правил вывода сведено к минимуму.
Основное свойство секвенциальной формы — симметричное устройство[⇨], обеспечивающее удобство доказательства устранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств.
Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввел в 1929 году немецкий физик и логик Пауль Герц (нем. Paul Hertz; 1881—1940) , но целостного исчисления для какой-либо логической теории в его трудах построено не было . Об этом говорит сайт https://intellect.icu . В работе 1932 года Генцен попытался развить подход Герца , но в 1934 году отказался от наработок Герца: ввел системы натурального вывода 
и 
для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы и . Для и Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив ее с помощью секвенциального варианта трансфинитной индукцией до ординала 
. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Геделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить ее собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.
Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Ойвой Кетоненом (фин. Oiva Ketonen; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости . Опубликованное в 1949 году в диссертации Романа Сушко (польск. Roman Suszko; 1919—1979) безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа.
В 1952 году Стивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода , там же ввел исчисления генценовского типа 
и 
, в которых не требовались структурные[⇨] правила вывода, и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов .
Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Гаиси Такеути (яп. 竹内外史; 1926—2017) построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Уильям Тэйт (англ. род. 1929) доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси[10] и Дага Правица (швед. Dag Prawitz; род. 1936). В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Жирар[fr] — для системы F.
Начиная с 1980-х годов секвенциальные системы играют ключевую роль в развитии систем автоматического доказательства, в частности, разработанное Тьерри Коканом и Жераром Юэ в 1986 году секвенциальное исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта — используется как основа программной системы Coq.
Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система , построенная Генценом в 1934 году. В системе одна схема аксиом — и 21 правило вывода, которые делятся на структурные и логические[11].
Структурные правила (, 
— формулы, , , 
, 
— списки формул):
и справа: 
;
и справа: 
;
и справа: 
,
.Логические пропозициональные правила предназначены для добавления в вывод пропозициональных связок:
-слева: 
; -справа: 
;
-слева: 
и 
; -справа: 
,
-слева: 
; -справа: 
и 
,
-слева: 
и -справа: 
.Логические кванторные правила вводят кванторы всеобщности и существования в вывод (
— формула со свободной переменной 
, 
— произвольный терм, а 
— замена всех вхождений свободной переменной на терм ):
-слева: 
и -справа: 
;
-слева: 
и -справа: 
.Дополнительное условие в кванторных правилах — невхождение свободной переменной в нижние формулы секвенций в правилах -справа и -слева.
Пример -вывода закона исключенного третьего:
— в нем вывод начат с единственной аксиомы, далее — последовательно применены правила -справа, -справа, перестановка справа, -справа и сокращение справа.
Исчисление эквивалентно классическому исчислению предикатов первой ступени: формула общезначима в исчислении предикатов тогда и только тогда, когда в выводима секвенция 
. Ключевой результат, который назван Генценом «основной теоремой» (нем. Hauptsatz) — возможность провести любой -вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства , в том числе корректность, непротиворечивость и полнота.
Исчисление получается из добавлением ограничения на сукцеденты секвенций в правилах вывода: в них допустимо использование только одной формулы, а правила перестановки справа и сокращения справа (оперирующие с нескольким формулами в сукцедентах) исключаются. Таким образом, при минимальных модификациях получается система, в которой невыводимы законы двойного отрицания и исключенного третьего, но действуют все прочие основные логические законы, и, например, выводима эквивалентность 
. Полученная система эквивалентна интуиционистскому исчислению предикатов с аксиоматикой Гейтинга. В исчислении также устранимы сечения, оно также корректно, непротиворечиво и полно, притом последний результат для интуиционистского исчисления предикатов впервые получен именно для .
Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционисткой логик. Часть таких исчислений наследует построение Генцена, примененное при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса (англ. Patrick Suppes; 1922—2014) 1957 года[12] (почерпнутая из замечаний Фейса[en] и Ладриера[fr] к французскому переводу статьи Генцена), и ее усовершенствованная версия, опубликованная в 1965 году Леммоном (англ. John Lemmon; 1930—1966)[13], устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена[14]. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом (нем. Hans Hermes; 1912—2003)[15]: в его системе для классической логики применены две аксиомы ( и 
, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях[16].
Секвенциальным исчислениям присуща симметрия, естественно выражающая двойственность, в аксиоматических теориях формулируемую законами де Моргана
Исследование, описанное в статье про секвенция, подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое секвенция, исчисление секвенций и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Теория цифровых автоматов
Комментарии
Оставить комментарий
Теория цифровых автоматов
Термины: Теория цифровых автоматов