Естественный вычет

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

Мотивация [ править ]

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

Естественная дедукция в ее современной форме была независимо предложена немецким математиком Герхардом Гентценом в 1934 году в диссертации, представленной на факультете математических наук Геттингенского университета . ^[2] Термин естественная дедукция (или, скорее, его немецкий эквивалент 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". ^[3]
(Сначала я хотел построить формализм, максимально приближенный к реальным рассуждениям. Так возникло «исчисление естественной дедукции».)

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

При естественном выводе предложение выводится из набора предпосылок путем многократного применения правил вывода. Система, представленная в этой статье, представляет собой незначительный вариант формулировки Гентцена или Правица, но с более близким соответствием описанию логических суждений и связок Мартином-Лёфом . ^[5]

Суждения и предложения [ править ]

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

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

Суждение « A prop» определяет структуру действительных доказательств A , которая, в свою очередь, определяет структуру утверждений. По этой причине правила вывода для этого суждения иногда называют правилами формирования . Чтобы проиллюстрировать, если у нас есть два предложения A и B (то есть суждения « A prop» и « B prop» очевидны), то мы формируем составные предложения 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Правда B правда─────────────────── ∧I A ∧ B верно ────────── ∧E 1 Правда

────── тыПравда

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

────────── uA ∧ B верно

────────── u ─────────── uA ∧ B верно A ∧ B верно────────── ∧E 1 ─────────── ∧E 2 Правда B правда ──────────────────────── ∧I A ∧ B верно

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

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

Логика предыдущего раздела является примером односортированной логики, т. Е. Логики с единственным видом объекта: предложениями. Было предложено множество расширений этой простой структуры; в этом разделе мы расширим его, добавив в него людей или термины второго типа . Точнее, мы добавим новый вид суждения: « t - термин » (или « t term »), где t - схематический. Мы фиксируем счетное множество 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{ term}}}{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{ term}}}{\phi (t_{1},t_{2},\cdots ,t_{n}){\hbox{ prop}}}}{\hbox{ pred}}_{F}}$

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

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

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

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

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

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

${\displaystyle {\frac {[t/x]A{\hbox{ true}}}{\exists x.A{\hbox{ true}}}}\;\exists _{I}\qquad \qquad {\cfrac {{\begin{matrix}\\\\\\\\\exists x.A{\hbox{ true}}\\\end{matrix}}\qquad {\begin{matrix}{\cfrac {}{a{\hbox{ term}}}}{\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 , избегая захвата. ^[8] Как и прежде, верхние индексы в имени обозначают компоненты, которые выводятся: термин a не может встречаться в заключении ∀I (такие термины известны как собственные переменные или параметры ), а гипотезы с именами u и v в ∃E локализуются во второй посылке в гипотетическом выводе. Хотя логика высказываний предыдущих разделов была разрешимадобавление кванторов делает логику неразрешимой.

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

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

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

Различные представления естественной дедукции [ править ]

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

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

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

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

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

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

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

──── u 1 ──── u 2 ... ──── u n J 1 J 2 J n ⋮ J

u 1 : J 1 , u 2 : J 2 , ..., u n : J n ⊢ J

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

u ∈ V─────── proof-Fты доказательство

────────────────────── hypu: Истина ⊢ u: Истина

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

π 1 доказательство π 2 доказательство───────────────────── пара-F(π 1 , π 2 ) доказательство

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

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

π доказательство─────────── FST -F FST π доказательство

Γ ⊢ π: A ∧ B───────────── ∧E 1
Γ ⊢ FST π: A

π доказательство─────────── snd -F snd π proof

Γ ⊢ π: A ∧ B────────────── ∧E 2
Γ ⊢ snd π: B

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

π доказательство──────────── λ-Fλu. π доказательство

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

π 1 доказательство π 2 доказательство─────────────────── app-Fπ 1 π 2 доказательство

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

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

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

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

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

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

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

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

Γ ⊢ A тип Γ, x: A ⊢ B тип──────────────────────────────-FΓ ⊢ Πx: A. Тип B

Γ ⊢ A тип Γ, x: A ⊢ B тип───────────────────────────── Σ-FΓ ⊢ Σx: A. Тип B

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

Γ, 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──────────────── ΣE 1
Γ ⊢ FST π: A

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

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

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

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

Классическая и модальная логика [ править ]

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

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

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

─────────────── XM 1A ∨ ¬A правда

¬¬А правда────────── XM 2Правда

──────── u¬А правда⋮p правда────── XM 3 u, pПравда

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

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

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

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

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

Действительный──────── ◻I◻ Истинный

◻ Истинный──────── ◻EПравда

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

Ω; ⋅ ⊢ π: истинное───────────────────── ◻IΩ; ⋅ ⊢ box π: ◻ Истинный

Ω; Γ ⊢ π: ◻ Истинный──────────────────────── ◻EΩ; Γ ⊢ unbox π: истинное

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

────────────────────────────────────────────────────────────────────────────────────────────Ω, u: (A действительно); Γ ⊢ u: Истинный

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

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

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

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

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

Последовательное исчисление [ править ]

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

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

Γ ⇒ A───────── ∨R 1Γ ⇒ A ∨ B

Γ ⇒ B───────── ∨R 2Γ ⇒ 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 | | элим. правила | ↓ ─────────────────────── ↑ ↓ встречаются ↑ | | вступление. правила | заключение

 ──────────────────────────── 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────────────────────────────────── ∧L 1
Γ, v: (A ∧ B) ⇒ [ fst v / u ] π: C

Γ ⊢ π: A ∧ B───────────── ∧E 1
Γ ⊢ FST π: A

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

Γ ⊢ π: A ∧ B────────────── ∧E 2
Γ ⊢ snd π: B

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

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

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

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

В большинстве хорошо продуманных логик сокращение не требуется как правило вывода, хотя оно остается доказуемым как мета-теорема ; Избыточность правила отсечения обычно представляется как вычислительный процесс, известный как исключение отсечения . Это интересное приложение для естественного вывода; обычно чрезвычайно утомительно доказывать определенные свойства непосредственно с помощью естественного вывода из-за неограниченного числа случаев. Например, рассмотрите возможность показать, что данное предложение не соответствует действительности.доказуемо с помощью естественного вывода. Простой индуктивный аргумент не срабатывает из-за таких правил, как orE или 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.
• Мартин-Лёф, Пер (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.
• Prawitz, Dag (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) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9.

Внешние ссылки [ править ]

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