Естественный вычет - Natural deduction

В логике и теории доказательств , естественно вычет является своего рода доказательством исчисления , в котором логическое мышление выражается правил вывода , тесно связанных с «естественным путем» рассуждений. Это контрастирует с системами в стиле Гильберта , которые вместо этого в максимально возможной степени используют аксиомы для выражения логических законов дедуктивного мышления .

Мотивация

Естественная дедукция выросла из контекста неудовлетворенности аксиоматизацией дедуктивного мышления, общей для систем Гильберта , Фреге и Рассела (см., Например, систему Гильберта ). Такие аксиоматизации наиболее широко использовались Расселом и Уайтхедом в их математическом трактате Principia Mathematica . Вдохновленный серией семинаров Лукасевича в Польше в 1926 году, которые отстаивали более естественное отношение к логике, Яськовский предпринял первые попытки дать определение более естественной дедукции, сначала в 1929 году с использованием схематической записи, а затем обновив свое предложение в последовательности. бумаги в 1934 и 1935. Его предложения привели к различным обозначениям , таким как Fitch стиль исчисление (или диаграммы Fitch,) или Суппес метод " , для которого Леммон дал вариант под названием системы L .

Естественная дедукция в ее современной форме была независимо предложена немецким математиком Герхардом Гентценом в 1934 году в диссертации, представленной на факультете математических наук Геттингенского университета . Термин естественная дедукция (или, скорее, его немецкий эквивалент natürliches Schließen ) был придуман в этой статье:

Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens" .
(Сначала я хотел построить формализм, максимально приближенный к реальным рассуждениям. Так возникло «исчисление естественной дедукции».)

Генцен был мотивирован желанием установить непротиворечивость теории чисел . Он был не в состоянии доказать основной результат , необходимый для результата непротиворечивости, то устранение покроя теорема -The Hauptsatz-непосредственно для естественного вывода. По этой причине он представил свою альтернативную систему, секвенция исчисления , для которых он доказал Hauptsatz как для классической и интуиционистской логики . В серии семинаров в 1961 и 1962 годах Правиц дал исчерпывающий обзор исчислений естественной дедукции и перенес большую часть работы Гентцена с последовательными исчислениями в рамки естественной дедукции. Его монография 1965 Естественная дедукция: исследование корректуры Теоретической должны была стать справочником по естественным дедукции, а также включены приложениям для модального и логики второго порядка .

При естественном выводе предложение выводится из набора предпосылок путем многократного применения правил вывода. Система представлены в данной статье , является небольшим изменением формулировки Генцена или Prawitz, но с более близким следованием Мартины-LOF описанием «s логических суждений и связок.

Суждения и предложения

Суждение является то , что познаваемо, то есть объект познания. Это очевидно, если знать это на самом деле. Таким образом, « идет дождь » - это приговор, который очевиден для того, кто знает, что на самом деле идет дождь; в этом случае можно легко найти доказательства вынесенного приговора, посмотрев в окно или выйдя из дома. Однако в математической логике свидетельства часто не так непосредственно наблюдаемы, а скорее выводятся из более основных очевидных суждений. Процесс дедукции составляет доказательство ; другими словами, приговор очевиден, если есть доказательства.

Наиболее важные суждения в логике имеют форму « А верно ». Буква А обозначает любое выражение, представляющее предложение ; Таким образом, суждения об истинности требуют более примитивного суждения: « А - это высказывание ». Были изучены многие другие суждения; например, « A ложно » (см. классическую логику ), « A истинно в момент t » (см. временную логику ), « A обязательно истинно » или « A, возможно, истинно » (см. модальную логику ), « программа M имеет тип τ »(см. Языки программирования и теорию типов ),« A достижимо из доступных ресурсов »(см. Линейную логику ) и многие другие. Для начала, мы должны относиться к себе с простейшими двух суждений « А является предложение » и « А правда », сокращенно « опора» и « правда» соответственно.

Суждение « A prop» определяет структуру действительных доказательств A , которая, в свою очередь, определяет структуру утверждений. По этой причине правила вывода для этого суждения иногда называют правилами формирования . Чтобы проиллюстрировать, если мы имеем два предложений A и B (то есть, суждение « проп» и « Б проп» очевидно), то мы формируем соединение суждение А и В , написанном символический как « ». Мы можем записать это в виде правила вывода: ${\ Displaystyle A \ клин B}$

${\ displaystyle {\ frac {A {\ hbox {prop}} \ qquad B {\ hbox {prop}}} {(A \ wedge B) {\ hbox {prop}}}} \ \ wedge _ {F}}$

где скобки опущены, чтобы сделать правило вывода более лаконичным:

${\ displaystyle {\ frac {A {\ hbox {prop}} \ qquad B {\ hbox {prop}}} {A \ wedge B {\ hbox {prop}}}} \ \ wedge _ {F}}$

Это правило вывода схематично : экземпляры A и B можно создать с помощью любого выражения. Общая форма правила вывода:

${\ displaystyle {\ frac {J_ {1} \ qquad J_ {2} \ qquad \ cdots \ qquad J_ {n}} {J}} \ {\ hbox {name}}}$

где каждый является суждением, а правило вывода называется «имя». Суждения над чертой называются предпосылками , а суждения под чертой - выводами . Другими распространенными логическими предложениями являются дизъюнкция ( ), отрицание ( ), импликация ( ) и логические константы истина ( ) и ложь ( ). Правила их формирования ниже. ${\ displaystyle J_ {i}}$${\ displaystyle A \ vee B}$${\ displaystyle \ neg A}$${\ Displaystyle A \ supset B}$${\ displaystyle \ top}$${\ displaystyle \ bot}$

${\ displaystyle {\ frac {A {\ hbox {prop}} \ qquad B {\ hbox {prop}}} {A \ vee B {\ hbox {prop}}}} \ \ vee _ {F} \ qquad { \ frac {A {\ hbox {prop}} \ qquad B {\ hbox {prop}}} {A \ supset B {\ hbox {prop}}}} \ \ supset _ {F}}$

${\ displaystyle {\ frac {\ hbox {}} {\ top {\ hbox {prop}}}} \ \ top _ {F} \ qquad {\ frac {\ hbox {}} {\ bot {\ hbox {prop }}}} \ \ bot _ {F} \ qquad {\ frac {A {\ hbox {prop}}} {\ neg A {\ hbox {prop}}}} \ \ neg _ {F}}$

Введение и устранение

Теперь мы обсудим « А истинное» суждение. Правила вывода, которые вводят логическую связку в заключение, известны как правила введения . Чтобы ввести союзы, т. Е. Сделать вывод « A и B истинны» для предложений A и B , требуется свидетельство « A истинно» и « B истинно». В качестве правила вывода:

Следует понимать, что в таких правилах объекты являются предложениями. То есть приведенное выше правило на самом деле является сокращением для:

Это также можно записать:

В этой форме первая посылка может быть удовлетворена правилом формирования, дающим первые две посылки предыдущей формы. В этой статье мы опустим «опорные» суждения, в которых они понимаются. В нулевом случае истину нельзя вывести ни из каких предпосылок. ${\ displaystyle \ wedge _ {F}}$

Если истинность предложения может быть установлена ​​более чем одним способом, соответствующая связка имеет несколько правил введения.

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

Двойственные правила введения - это правила исключения, описывающие, как деконструировать информацию о составном предложении в информацию о его составляющих. Таким образом, из « A ∧ B true» мы можем сделать вывод « A true» и « B true»:

В качестве примера использования правил вывода рассмотрим коммутативность конъюнкции. Если A ∧ B истинно, то B ∧ A истинно; этот вывод можно сделать, составив правила вывода таким образом, чтобы посылки более низкого вывода совпадали с выводом следующего более высокого вывода.

Цифры вывода, которые мы видели до сих пор, недостаточны, чтобы сформулировать правила введения импликации или исключения дизъюнкции ; для этого нам понадобится более общее понятие гипотетического вывода .

Гипотетические выводы

Распространенная операция в математической логике - это рассуждение на основе предположений . Например, рассмотрим следующий вывод:

Этот вывод не устанавливает истинность B как такового; скорее, он устанавливает следующий факт:

Если A ∧ (B ∧ C) истинно, то B истинно .

В логике говорят: « Предполагая, что A ∧ (B ∧ C) истинно, мы показываем, что B истинно »; другими словами, суждение « B истинно» зависит от предполагаемого суждения « A ∧ (B ∧ C) истинно». Это гипотетический вывод , который мы запишем следующим образом:

Интерпретация такова: « B true выводится из A ∧ (B ∧ C) true ». Конечно, в этом конкретном примере мы на самом деле знаем происхождение « B истинно» от « A ∧ (B ∧ C) истинно», но в целом мы можем не знать это происхождение априори . Общая форма гипотетического вывода:

Каждая гипотетическая деривация имеет набор предшествующих дериваций ( D _i ), записанных в верхней строке, и последующее суждение ( J ), написанное в нижней строке. Каждое из посылок само по себе может быть гипотетическим производным. (Для простоты мы рассматриваем суждение как вывод без предпосылок.)

Понятие гипотетического суждения интернализируется как связующее звено импликации. Правила введения и исключения следующие.

В правиле введения, предшествующее имя у будет выписан в заключении. Это механизм для ограничения объема гипотезы: ее единственная причина существования - установить « B истинно»; его нельзя использовать для каких-либо других целей, в частности, его нельзя использовать после введения. В качестве примера рассмотрим вывод « A ⊃ (B ⊃ (A ∧ B)) true»:

В этом полном выводе нет неудовлетворенных предпосылок; однако суб-производные являются гипотетическими. Например, вывод « B ⊃ (A ∧ B) true» является гипотетическим с предшествующим « A true» (названным u ).

С помощью гипотетических выводов мы теперь можем написать правило исключения для дизъюнкции:

На словах, если A ∨ B истинно, и мы можем вывести « C true» как из « A true», так и из « B true», то C действительно истинно. Обратите внимание, что это правило не принимает ни « A true», ни « B true». В нулевом случае, т.е. в случае ложности, получаем следующее правило исключения:

Это читается как: если ложь верна, то любое суждение C верно.

Отрицание похоже на импликацию.

Правило , введение разряжается как название гипотезы ˙U и сукцедент р , то есть , предложение р не должен происходить в заключении А . Поскольку эти правила схематичны, интерпретация правила введения следующая: если из « А истинно» мы можем вывести для каждого предложения p, что « p истинно», то A должно быть ложным, то есть « не A истинным». Что касается исключения, если доказано, что истинны и A, и не A , то возникает противоречие, и в этом случае каждое предложение C истинно. Поскольку правила импликации и отрицания очень похожи, должно быть довольно легко увидеть, что не A и A ⊃ ⊥ эквивалентны, т. Е. Каждый выводится из другого.

Последовательность, полнота и нормальные формы

Теория называется непротиворечивой , если ложь не выводима (от каких - либо предположений) и является полным , если каждая теорема или его отрицание доказуемо с помощью правил вывода логики. Это утверждения обо всей логике, обычно связанные с определенным понятием модели . Однако существуют местные понятия согласованности и полноты, которые представляют собой чисто синтаксическую проверку правил вывода и не требуют обращения к моделям. Первым из них является локальная согласованность, также известная как локальная сводимость, которая гласит, что любой вывод, содержащий введение связки с последующим ее удалением, может быть превращен в эквивалентный вывод без этого обходного пути. Это проверка на силу правил исключения: они не должны быть настолько сильными, чтобы включать в себя знания, которых еще нет в их предпосылках. В качестве примера рассмотрим союзы.

────── u   ────── w
A true     B true
────────────────── ∧I
    A ∧ B true
    ────────── ∧E1
      A true

────── u
A true

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

────────── u
A ∧ B true

────────── u    ────────── u
A ∧ B true      A ∧ B true
────────── ∧E1  ────────── ∧E2
  A true          B true
  ─────────────────────── ∧I
       A ∧ B true

Эти понятия точно соответствуют β-редукции (бета-редукция) и η-преобразованию (эта-преобразование) в лямбда-исчислении с использованием изоморфизма Карри – Ховарда . По локальной полноте мы видим, что каждый вывод может быть преобразован в эквивалентный вывод, в котором вводится главная связка. Фактически, если весь вывод подчиняется этому порядку исключений, за которым следуют введения, то он считается нормальным . При нормальном выводе все исключения происходят выше введения. В большинстве логик каждый вывод имеет эквивалентный нормальный вывод, называемый нормальной формой . Существование нормальных форм , как правило , трудно доказать , используя естественный вывод один, хотя такие счета существуют в литературе, в первую очередь по Дагу Проиц в 1961 году гораздо проще показать это косвенно с помощью разреза свободной секвенции исчисления презентации .

Расширения первого и более высокого порядка

Краткое изложение системы первого порядка

Логика предыдущего раздела является примером односортированной логики, т. Е. Логики с единственным видом объекта: предложениями. Было предложено множество расширений этой простой структуры; в этом разделе мы расширим его, добавив в него людей или термины второго типа . Точнее, мы добавим новый вид суждения, « т термин » (или « термин т ») , где т схематично. Мы фиксируем счетное множество V из переменных , еще счетного множества F из функциональных символов и термины построить со следующими правилами формирования:

${\ displaystyle {\ frac {v \ in V} {v {\ hbox {term}}}} {\ hbox {var}} _ {F}}$

а также

${\ displaystyle {\ frac {f \ in F \ qquad t_ {1} {\ hbox {term}} \ qquad t_ {2} {\ hbox {term}} \ qquad \ cdots \ qquad t_ {n} {\ hbox {термин}}} {f (t_ {1}, t_ {2}, \ cdots, t_ {n}) {\ hbox {term}}}} {\ hbox {app}} _ {F}}$

Для предложений, мы рассмотрим третий счетное множество P из предикатов , а также определить атомные предикаты над термами со следующим правилом образования:

${\ displaystyle {\ frac {\ phi \ in P \ qquad t_ {1} {\ hbox {term}} \ qquad t_ {2} {\ hbox {term}} \ qquad \ cdots \ qquad t_ {n} {\ hbox {термин}}} {\ phi (t_ {1}, t_ {2}, \ cdots, t_ {n}) {\ hbox {prop}}}} {\ hbox {pred}} _ {F}}$

Первые два правила формирования дают определение термина, которое фактически совпадает с определением термина в алгебре терминов и теории моделей , хотя фокус этих областей исследования сильно отличается от естественного вывода. Третье правило формирования эффективно определяет атомарную формулу , как в логике первого порядка , так и снова в теории моделей.

К ним добавляется пара правил формирования, определяющих обозначение количественных предложений; один для универсальной (∀) и экзистенциальной (∃) количественной оценки:

${\ displaystyle {\ frac {x \ in V \ qquad A {\ hbox {prop}}} {\ forall xA {\ hbox {prop}}}} \; \ forall _ {F} \ qquad \ qquad {\ frac {x \ in V \ qquad A {\ hbox {prop}}} {\ exists xA {\ hbox {prop}}}} \; \ exists _ {F}}$

Квантор имеет свои правила вводные и элиминации:

${\ displaystyle {\ begin {matrix} {\ cfrac {} {a {\ hbox {term}}}} {\ hbox {u}} \\\ vdots \\ {\ cfrac {[a / x] A {\ hbox {true}}} {\ forall xA {\ hbox {true}}}} \; \ forall _ {I ^ {u, a}} \ end {matrix}} \ qquad \ qquad {\ frac {\ forall xA {\ hbox {true}} \ qquad t {\ hbox {term}}} {[t / x] A {\ hbox {true}}}} \; \ forall _ {E}}$

У квантификатора существования есть правила введения и исключения:

${\ displaystyle {\ frac {[t / x] A {\ hbox {true}}} {\ exists xA {\ hbox {true}}}} \; \ exists _ {I} \ qquad \ qquad {\ cfrac { {\ begin {matrix} \\\\\\\\\ существует xA {\ hbox {true}} \\\ end {matrix}} \ qquad {\ begin {matrix} {\ cfrac {} {a {\ hbox {термин}}}} {\ hbox {u}} \ qquad {\ cfrac {} {[a / x] A {\ hbox {true}}}} {\ hbox {v}} \\\ vdots \\ C {\ hbox {true}} \\\ end {matrix}}} {C {\ hbox {true}}}} \ exists _ {E ^ {a, u, v}}}$

В этих правилах обозначение [ t / x ] A означает замену t для каждого (видимого) экземпляра x в A , избегая захвата. Как и раньше, верхние индексы в имени обозначают компоненты, которые выводятся: термин a не может встречаться в заключении ∀I (такие термины известны как собственные переменные или параметры ), а гипотезы с именами u и v в ∃E локализованы для вторая посылка в гипотетическом выводе. Хотя логика высказываний предыдущих разделов была разрешимой , добавление кванторов делает ее неразрешимой.

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

${\ displaystyle {\ cfrac {\ begin {matrix} {\ cfrac {} {p {\ hbox {prop}}}} {\ hbox {u}} \\\ vdots \\ A {\ hbox {prop}} \ \\ end {matrix}} {\ forall pA {\ hbox {prop}}}} \; \ forall _ {F ^ {u}} \ qquad \ qquad {\ cfrac {\ begin {matrix} {\ cfrac {} {p {\ hbox {prop}}}} {\ hbox {u}} \\\ vdots \\ A {\ hbox {prop}} \\\ end {matrix}} {\ exists pA {\ hbox {prop} }}} \; \ exists _ {F ^ {u}}}$

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

Различные представления естественного вывода

Древовидные презентации

Сбрасывающие аннотации Генцена , используемые для интернализации гипотетических суждений можно избежать пути представления доказательств в виде дерева секвенции Γ ⊢A вместо дерева истинного суждения.

Последовательные презентации

Представления Jaśkowski в естественной дедукции привели к различным обозначениям , таким как Fitch , в стиле исчисление (или диаграммы Fitch,) или Суппес метод ', из которых Леммон дал вариант под названием Системы л . Такие системы представления, которые более точно описываются как табличные, включают следующее.

• 1940: В учебнике Куайн обозначал предшествующие зависимости номерами строк в квадратных скобках, предвосхищая нотацию номеров строк Суппеса 1957 года.
• 1950: В учебнике Куайн (1982 , стр. 241–255) продемонстрировал метод использования одной или нескольких звездочек слева от каждой строки доказательства для обозначения зависимостей. Это эквивалент вертикальных полос Клини. (Не совсем ясно, появилась ли звездочка Куайна в оригинальном издании 1950 года или была добавлена ​​в более позднем издании.)
• 1957: Введение в практическую логику доказательства теорем в учебнике Суппеса (1999 , стр. 25–150). Это указывало на зависимости (т. Е. Предшествующие утверждения) номерами строк слева от каждой строки.
• 1963: Столл (1979 , стр. 183–190, 215–219) использует наборы номеров строк для обозначения предшествующих зависимостей строк последовательных логических аргументов, основанных на правилах естественного вывода.
• 1965: Весь учебник Леммона (1965) представляет собой введение в логические доказательства с использованием метода, основанного на методе Суппеса.
• 1967: В учебнике Клини (2002 , стр. 50–58, 128–130) вкратце продемонстрировал два вида практических логических доказательств: одна система использует явные цитаты предшествующих суждений слева от каждой строки, другая система использует вертикальную черту. -линии слева для обозначения зависимостей.

Доказательства и теория типов

Изложение естественного вывода до сих пор концентрировалось на природе предложений без предоставления формального определения доказательства . Чтобы формализовать понятие доказательства, мы немного изменим представление гипотетических выводов. Мы помечаем антецеденты переменными доказательства (из некоторого счетного набора переменных V ) и украшаем преемник фактическим доказательством. Антецеденты или гипотезы отделяются от преемников с помощью турникета (⊢). Эта модификация иногда называют локализованными гипотезами . На следующей диаграмме показаны изменения.

──── u1 ──── u2 ... ──── un
 J1      J2          Jn
              ⋮
              J

u1:J1, u2:J2, ..., un:Jn ⊢ J

Набор гипотез будет записан как Γ, если их точный состав не имеет значения. Для того, чтобы доказательства явной, мы переходим от корректуры менее суд « Истинный » к суждению: «π является доказательством (Истинный) », который записывается символически как «я: Истинный ». Следуя стандартному подходу, доказательства задаются своими собственными правилами формирования суждения «π доказательство ». Простейшее возможное доказательство - использование помеченной гипотезы; в этом случае свидетельством является сама этикетка.

u ∈ V
─────── proof-F
u proof

───────────────────── hyp
u:A true ⊢ u : A true

Для краткости в оставшейся части статьи мы опустим оценочную метку « истинно» , т.е. напишем «Γ ⊢ π: A ». Давайте еще раз рассмотрим некоторые связки с явными доказательствами. Что касается конъюнкции, мы смотрим на вводное правило ∧I, чтобы узнать форму доказательств конъюнкции: они должны быть парой доказательств двух конъюнктов. Таким образом:

π1 proof    π2 proof
──────────────────── pair-F
(π1, π2) proof

Γ ⊢ π1 : A    Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

Правила исключения ∧E ₁ и ∧E ₂ выбирают либо левое, либо правое соединение; таким образом, доказательства представляют собой пару проекций - первая ( fst ) и вторая ( snd ).

π proof
─────────── fst-F
fst π proof

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

π proof
─────────── snd-F
snd π proof

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

Для импликации вводная форма локализует или связывает гипотезу, записанную с использованием λ; это соответствует разряженной этикетке. В правиле «Γ, u : A » обозначает набор гипотез Γ вместе с дополнительной гипотезой u .

π proof
──────────── λ-F
λu. π proof

Γ, u:A ⊢ π : B
───────────────── ⊃I
Γ ⊢ λu. π : A ⊃ B

π1 proof   π2 proof
─────────────────── app-F
π1 π2 proof

Γ ⊢ π1 : A ⊃ B    Γ ⊢ π2 : A
──────────────────────────── ⊃E
Γ ⊢ π1 π2 : B

Имея явно доступные доказательства, можно манипулировать доказательствами и рассуждать о них. Ключевой операцией при доказательстве является замена одного доказательства предположением, используемым в другом доказательстве. Это широко известный как теорема замещения , и может быть доказана индукцией по глубине (или структуры) второго суждения.

Теорема подстановки

Если Γ ⊢ π ₁  : A и Γ, u : A ⊢ π ₂  : B , то Γ ⊢ [π ₁ / u ] π ₂  : B.

До сих пор решение «Γ ⊢ π: » была чисто логическая интерпретация. В теории типов логический взгляд заменен более вычислительным взглядом на объекты. Предложения в логической интерпретации теперь рассматриваются как типы , а доказательства как программы в лямбда-исчислении . Таким образом, «π: A » интерпретируется как « программа π имеет тип A ». Логические связки также имеют другое прочтение: соединение рассматривается как продукт (×), импликация - как стрелка функции (→) и т. Д. Однако различия носят чисто косметический характер. Теория типов имеет естественное представление дедукции в терминах правил формирования, введения и исключения; фактически, читатель может легко восстановить так называемую теорию простых типов из предыдущих разделов.

Разница между логикой и теорией типов заключается, прежде всего, в смещении фокуса с типов (предложений) на программы (доказательства). Теория типов в основном заинтересована в конвертируемости или сводимости программ. Для каждого типа существуют несводимые канонические программы этого типа; они известны как канонические формы или значения . Если каждую программу можно привести к каноническому виду, то теория типов называется нормализующей (или слабо нормализующей ). Если каноническая форма единственна, то теория называется сильно нормализующей . Нормализуемость - редкая черта большинства нетривиальных теорий типов, что сильно отличается от мира логики. (Напомним, что почти каждое логическое происхождение имеет эквивалентное нормальное происхождение.) Чтобы обрисовать причину: в теориях типов, допускающих рекурсивные определения, можно писать программы, которые никогда не сводятся к значению; таким программам цикла обычно можно присвоить любой тип. В частности, зацикливание программа имеет тип ⊥, хотя нет никакого логического доказательства «⊥ правды ». По этой причине предложения как типы; Доказательства как программная парадигма работает только в одном направлении, если вообще работает: интерпретация теории типов как логики обычно дает противоречивую логику.

Пример: теория зависимых типов

Подобно логике, теория типов имеет множество расширений и вариантов, включая версии первого и высшего порядка. Одна ветвь, известная как теория зависимых типов , используется в ряде компьютерных систем доказательства . Теория зависимых типов позволяет кванторам распространяться среди самих программ. Эти количественные типы записываются как Π и Σ вместо ∀ и ∃ и имеют следующие правила формирования:

Γ ⊢ A type    Γ, x:A ⊢ B type
───────────────────────────── Π-F
Γ ⊢ Πx:A. B type

Γ ⊢ A type  Γ, x:A ⊢ B type
──────────────────────────── Σ-F
Γ ⊢ Σx:A. B type

Эти типы являются обобщениями типов стрелок и продуктов соответственно, о чем свидетельствуют их правила введения и исключения.

Γ, x:A ⊢ π : B
──────────────────── ΠI
Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π1 : Πx:A. B   Γ ⊢ π2 : A
───────────────────────────── ΠE
Γ ⊢ π1 π2 : [π2/x] B

Γ ⊢ π1 : A    Γ, x:A ⊢ π2 : B
───────────────────────────── ΣI
Γ ⊢ (π1, π2) : Σx:A. B

Γ ⊢ π : Σx:A. B
──────────────── ΣE1
Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B
──────────────────────── ΣE2
Γ ⊢ snd π : [fst π/x] B

Теория зависимых типов в полной общности очень мощна: она способна выразить практически любые мыслимые свойства программ непосредственно в типах программы. За эту общность приходится платить высокой ценой - либо проверка типов неразрешима ( теория экстенсиональных типов ), либо более сложные экстенсиональные рассуждения ( теория интенсиональных типов ). По этой причине некоторые теории зависимых типов не допускают количественной оценки по произвольным программам, а скорее ограничиваются программами заданной разрешимой области индекса , например целыми числами, строками или линейными программами.

Поскольку теории зависимых типов позволяют типам зависеть от программ, возникает естественный вопрос: возможно ли, чтобы программы зависели от типов или любой другой комбинации. На такие вопросы есть много разных ответов. Популярный подход в теории типов - позволить количественную оценку программ по типам, также известный как параметрический полиморфизм ; из этого есть два основных вида: если типы и программы хранятся отдельно, то получается несколько более хорошо управляемая система, называемая предикативным полиморфизмом ; если различие между программой и типом стирается, получается теоретико-типовой аналог логики высшего порядка, также известный как импредикативный полиморфизм . Различные комбинации зависимости и полиморфизма были рассмотрены в литературе, наиболее известными из которых лямбда - куба из Барендрегт .

Пересечение логики и теории типов - обширная и активная область исследований. Новые логики обычно формализуются в рамках общей теории типов, известной как логическая структура . Популярные современные логические структуры, такие как исчисление конструкций и LF , основаны на теории зависимых типов более высокого порядка с различными компромиссами с точки зрения разрешимости и выразительной силы. Эти логические структуры сами всегда определяются как системы естественной дедукции, что свидетельствует о универсальности подхода естественной дедукции.

Классическая и модальная логика

Для простоты представленная логика была интуиционистской . Классическая логика расширяет интуиционистскую логику дополнительной аксиомой или принципом исключенного третьего :

Для любого предложения p предложение p ∨ ¬p верно.

Это утверждение, очевидно, не является ни введением, ни устранением; действительно, он включает в себя две различные связки. Первоначальная трактовка исключенного среднего, предложенная Генценом, предписывала одну из следующих трех (эквивалентных) формулировок, которые уже присутствовали в аналогичных формах в системах Гильберта и Гейтинга :

────────────── XM1
A ∨ ¬A true

¬¬A true
────────── XM2
A true

──────── u
¬A true
⋮
p true
────── XM3u, p
A true

(XM ₃ - это просто XM _2, выраженная в терминах E.) Такая трактовка исключенного среднего, помимо того, что она нежелательна с точки зрения пуриста, вносит дополнительные сложности в определение нормальных форм.

Сравнительно более удовлетворительная трактовка классической естественной дедукции только с точки зрения правил введения и исключения была впервые предложена Париго в 1992 году в форме классического лямбда-исчисления под названием λμ . Ключевой идеей его подхода была замена ориентированного на истину суждения A true более классическим понятием, напоминающим исчисление секвенций : в локализованной форме вместо Γ ⊢ A он использовал Γ ⊢ ∆, где ∆ - набор утверждений. аналогично Γ. Γ рассматривался как конъюнкция, а ∆ как дизъюнкция. Эта структура по существу поднимается непосредственно от классических исчислений секвенциальных , но инновации в Й ^ должны были дать вычислительный смысл классических доказательства естественного вывода в терминах callcc или механизм броска / улове видел в LISP и его потомках. (См. Также: первоклассный контроль .)

Еще одно важное расширение касалось модальных и других логик, которые нуждаются не только в базовом суждении об истине. Впервые они были описаны для алетических модальных логик S4 и S5 в стиле естественной дедукции Правитцем в 1965 году и с тех пор накопили большое количество связанных работ. Приведу простой пример: модальная логика S4 требует одного нового суждения « Действителен », которое категорично по отношению к истине:

Если «А верно» без предположений формы «В верно», то «А верно».

Это категориальное суждение усвоено как унарная связка ◻ A (читается как « обязательно А ») со следующими правилами введения и исключения:

A valid
──────── ◻I
◻ A true

◻ A true
──────── ◻E
A true

Обратите внимание, что посылка « Действителен » не имеет определяющих правил; вместо этого используется категориальное определение действительности. Этот режим становится более ясным в локализованной форме, когда гипотезы явны. Мы пишем «Ω; Γ ⊢ A true », где Γ, как и раньше, содержит истинные гипотезы, а Ω содержит действительные гипотезы. Справа - единственное суждение « Истина »; валидность здесь не требуется, поскольку «Ω ⊢ A действительный » по определению то же самое, что «Ω; ⋅ ⊢ A true ». Формы введения и исключения:

Ω;⋅ ⊢ π : A true
──────────────────── ◻I
Ω;⋅ ⊢ box π : ◻ A true

Ω;Γ ⊢ π : ◻ A true
────────────────────── ◻E
Ω;Γ ⊢ unbox π : A true

Модальные гипотезы имеют свою собственную версию правила гипотез и теоремы замещения.

─────────────────────────────── valid-hyp
Ω, u: (A valid) ; Γ ⊢ u : A true

Теорема о модальной подстановке

Если Ω; ⋅ ⊢ π ₁  : A истинно и Ω, u : ( A действительно ); Γ ⊢ π ₂  : C истинно , тогда Ω; Γ ⊢ [π ₁ / u ] π ₂  : C истинно .

Эта структура разделения суждений на отдельные наборы гипотез, также известная как многозонный или полиадический контексты, очень эффективна и расширяема; она применяется для различных модальных логик, а также для линейных и других субструктурных логик , чтобы дать несколько примеров. Однако относительно немного систем модальной логики могут быть формализованы непосредственно с помощью естественной дедукции. Чтобы дать теоретико-доказательственные характеристики этих систем, расширения, такие как маркировка или системы глубокого вывода.

Добавление меток к формулам позволяет более точно контролировать условия, при которых применяются правила, позволяя применять более гибкие методы аналитических таблиц , как это было сделано в случае помеченного вывода . Метки также позволяют именовать миры в семантике Крипке; Симпсон (1993) представляет эффективный метод преобразования условий фрейма модальных логик в семантике Крипке в правила вывода в формализации естественного вывода гибридной логики . Stouppa (2004) обозревает применение многих пробных теорий, таких как Avron и POTTINGER в hypersequents и Белнапа в дисплей логики таких модальных логик как S5 и B.

Сравнение с другими основополагающими подходами

Последовательное исчисление

Последовательное исчисление - главная альтернатива естественному выводу как основе математической логики . При естественной дедукции поток информации является двунаправленным: правила исключения передают информацию вниз путем деконструкции, а правила введения передают информацию вверх путем сборки. Таким образом, у доказательства естественного вывода нет чисто восходящего или нисходящего чтения, что делает его непригодным для автоматизации при поиске доказательства. Чтобы обратиться к этому факту, Генцен в 1935 году предложил свое последовательное исчисление , хотя первоначально он задумал его как техническое средство для прояснения непротиворечивости логики предикатов . Клини в своей основополагающей книге 1952 года « Введение в метаматематику» дал первую формулировку секвенциального исчисления в современном стиле.

В последовательном исчислении все правила вывода имеют чисто восходящее чтение. Правила вывода могут применяться к элементам с обеих сторон турникета . ( Для того, чтобы отличить от естественного вывода, эта статья использует двойную стрелку ⇒ вместо правильной липкости ⊢ для секвенции.) Правила введения природных дедукций рассматриваются как правильные правила в исчислении секвенций, и структурно очень похожи. С другой стороны, правила исключения превращаются в левые правила в исчислении секвенций. В качестве примера рассмотрим дизъюнкцию; правильные правила знакомы:

Γ ⇒ A
───────── ∨R1
Γ ⇒ A ∨ B

Γ ⇒ B
───────── ∨R2
Γ ⇒ A ∨ B

Налево:

Γ, u:A ⇒ C       Γ, v:B ⇒ C
─────────────────────────── ∨L
Γ, w: (A ∨ B) ⇒ C

Вспомните правило естественного вывода ∨E в локализованной форме:

Γ ⊢ A ∨ B    Γ, u:A ⊢ C    Γ, v:B ⊢ C
─────────────────────────────────────── ∨E
Γ ⊢ C

Утверждение A ∨ B , которое является преемником посылки в E, превращается в гипотезу заключения в левом правиле L. Таким образом, левые правила можно рассматривать как своего рода перевернутое правило исключения. Это наблюдение можно проиллюстрировать следующим образом:

 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion

 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion

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

────────── init
Γ, u:A ⇒ A

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

Обоснованность ⇒ ср. ⊢

Если Г ⇒ А , то Γ ⊢ A .

Полнота ⇒ ср. ⊢

Если Г ⊢ A , то Γ ⇒ A .

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

Γ ⇒ π1 : A     Γ ⇒ π2 : B
─────────────────────────── ∧R
Γ ⇒ (π1, π2) : A ∧ B

Γ ⊢ π1 : A      Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

Однако левое правило выполняет некоторые дополнительные замены, которые не выполняются в соответствующих правилах исключения.

Γ, u:A ⇒ π : C
──────────────────────────────── ∧L1
Γ, v: (A ∧ B) ⇒ [fst v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

Γ, u:B ⇒ π : C
──────────────────────────────── ∧L2
Γ, v: (A ∧ B) ⇒ [snd v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

Таким образом, виды доказательств, полученные в исчислении секвенций, довольно сильно отличаются от доказательств естественного вывода. Исчисление секвенций дает доказательства в так называемой β-нормальной η-длинной форме, которая соответствует каноническому представлению нормальной формы доказательства естественного вывода. Если попытаться описать эти доказательства, используя саму естественную дедукцию, то получится так называемое исчисление интеркаляции (впервые описанное Джоном Бирнсом), которое можно использовать для формального определения понятия нормальной формы для естественного вывода.

Теорема подстановки естественного вывода принимает форму структурного правила или структурной теоремы, известной как сокращение в секвенциальном исчислении.

Вырезать (замена)

Если Г ⇒ тг ₁  : А и Г, у : ⇒ π ₂  : С , то Г ⇒ [л ₁ / и] л ₂  : С .

В большинстве хорошо организованных логик сокращение не требуется как правило вывода, хотя оно остается доказуемым как мета-теорема ; Избыточность правила отсечения обычно представляется как вычислительный процесс, известный как исключение отсечения . Это интересное приложение для естественного вывода; обычно очень утомительно доказывать определенные свойства непосредственно с помощью естественного вывода из-за неограниченного числа случаев. Например, рассмотрите возможность показать, что данное предложение не доказуемо с помощью естественного вывода. Простой индуктивный аргумент не работает из-за таких правил, как ∨E или E, которые могут вводить произвольные предложения. Однако мы знаем, что исчисление секвенций полно относительно естественного вывода, поэтому достаточно показать эту недоказуемость в исчислении секвенций. Теперь, если сокращение недоступно в качестве правила вывода, тогда все правила секвенции либо вводят связку справа, либо слева, так что глубина вывода секвенции полностью ограничена связками в окончательном заключении. Таким образом, показать недоказуемость намного проще, потому что необходимо рассмотреть лишь конечное число случаев, и каждый случай полностью состоит из подпунктов заключения. Простым примером этого является теорема о глобальной непротиворечивости : «⋅ ⊢ ⊥ true » не доказуемо. В версии исчисления последовательностей это явно верно, потому что не существует правила, которое могло бы иметь «⋅ ⇒ ⊥» в качестве заключения! Теоретики доказательства часто предпочитают работать с формулировками последовательного исчисления без сечения из-за таких свойств.

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

Примечания

использованная литература

• Баркер-Пламмер, Дэйв; Барвайз, Джон ; Этчменди, Джон (2011). Доказательство языка и логика (2-е изд.). Публикации CSLI. ISBN 978-1575866321.
• Галлье, Жан (2005). "Конструктивная логика. Часть I: Учебное пособие по системам доказательства и типизированным λ-исчислениям" . Проверено 12 июня 2014 .
• Генцен, Герхард Карл Эрих (1934). "Untersuchungen über das logische Schließen. I" . Mathematische Zeitschrift . 39 (2): 176–210. DOI : 10.1007 / BF01201353 . S2CID  121546341 . (Английский перевод « Исследования логической дедукции в М.Э. Сабо. Собрание сочинений Герхарда Гентцена. Издательство Северной Голландии», 1969.)
• Генцен, Герхард Карл Эрих (1935). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3): 405–431. DOI : 10.1007 / bf01201363 . S2CID  186239837 .
• Жирар, Жан-Ив (1990). Доказательства и типы . Кембриджские трактаты в теоретической информатике. Издательство Кембриджского университета, Кембридж, Англия. Архивировано из оригинала на 2016-07-04 . Проверено 20 апреля 2006 . Перевод и приложения Пола Тейлора и Ива Лафонта.
• Яськовский, Станислав (1934). О правилах предположений в формальной логике .Перепечатано в польской логике 1920–39 гг. , Изд. Сторрс МакКолл.
• Клини, Стивен Коул (1980) [1952]. Введение в метаматематику (Одиннадцатое изд.). Северная Голландия. ISBN 978-0-7204-2103-3.
• Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Ishi Press International. ISBN 978-0-923891-57-2.
• Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-42533-7.
• Леммон, Эдвард Джон (1965). Начиная логику . Томас Нельсон. ISBN 978-0-17-712040-4.
• Мартин-Löf Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Северный журнал философской логики . 1 (1): 11–60. Конспект лекций к короткому курсу в Università degli Studi di Siena, апрель 1983 г.
• Пфеннинг, Франк; Дэвис, Роуэн (2001). «Оценочная реконструкция модальной логики» (PDF) . Математические структуры в компьютерных науках . 11 (4): 511–540. CiteSeerX  10.1.1.43.1611 . DOI : 10.1017 / S0960129501003322 . S2CID  16467268 .
• Prawitz, Даг (1965). Естественная дедукция: теоретико-доказательное исследование . Acta Universitatis Stockholmiensis, Стокгольмские исследования философии 3. Стокгольм, Гетеборг, Упсала: Almqvist & Wicksell.
• Правиц, Даг (2006) [1965]. Естественная дедукция: теоретико-доказательное исследование . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-44655-4.
• Куайн, Уиллард Ван Орман (1981) [1940]. Математическая логика (пересмотренная ред.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-55451-1.
• Куайн, Уиллард Ван Орман (1982) [1950]. Методы логики (Четвертое изд.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-57176-1.
• Симпсон, Алекс (1993). Теория доказательства и семантика интуиционистской модальной логики (PDF) . Эдинбургский университет. Кандидатская диссертация.
• Столл, Роберт Рот (1979) [1963]. Теория множеств и логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-63829-4.
• Ступпа, Финики (2004). Дизайн модальных Доказательство теорий: Случай S5 . Дрезденский университет. CiteSeerX  10.1.1.140.1858 . Магистерская диссертация.
• Суппес, Патрик полковник (1999) [1 957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9.

внешние ссылки

• Лаборео, Даниэль Клементе, « Введение в естественную дедукцию ».
• Домино на кислоте. Естественная дедукция, представленная в виде игры в домино.
• Пеллетье, Джефф, " История естественной дедукции и учебники элементарной логики ".
• Леви, Мишель, Доказательство высказываний.