Правило вывода

В логике и философии логики , в частности в дедуктивном рассуждении , правило вывода , правило вывода или правило преобразования — это логическая форма, состоящая из функции, которая берет посылки, анализирует их синтаксис и возвращает заключение (или заключения ).

Например, правило вывода, называемое modus ponens, берет две посылки, одну в форме «Если p, то q», а другую в форме «p», и возвращает заключение «q». Правило справедливо по отношению к семантике классической логики (а также семантике многих других неклассических логик ), в том смысле, что если посылки истинны (при интерпретации), то истинным является и заключение.

Обычно правило вывода сохраняет истину, семантическое свойство. В многозначной логике оно сохраняет общее обозначение. Но действие правила вывода является чисто синтаксическим и не нуждается в сохранении какого-либо семантического свойства: любая функция от наборов формул к формулам считается правилом вывода. Обычно важны только правила, которые являются рекурсивными ; т. е. правила, такие, что существует эффективная процедура для определения того, является ли любая данная формула заключением данного набора формул в соответствии с правилом. Примером правила, которое не является эффективным в этом смысле, является бесконечное ω-правило . ^[1]

Популярные правила вывода в пропозициональной логике включают modus ponens , modus tollens и контрапозицию . Логика предикатов первого порядка использует правила вывода для работы с логическими кванторами .

Стандартная форма

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

  Предпосылка №1
  Предпосылка №2
        ...
  Предпосылка №n
  Заключение

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

A\to B

{\underline {A\quad \quad \quad }}\,\!

B\!

Это правило modus ponens пропозициональной логики . Правила вывода часто формулируются как схемы, использующие метапеременные . ^[2] В правиле (схеме) выше метапеременные A и B могут быть инстанциированы для любого элемента вселенной (или иногда, по соглашению, ограниченного подмножества, такого как предложения ), чтобы сформировать бесконечный набор правил вывода.

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

Пример: системы Гильберта для двух пропозициональных логик

В системе Гильберта посылки и заключение правил вывода являются просто формулами некоторого языка, обычно использующими метапеременные. Для графической компактности представления и для подчеркивания различия между аксиомами и правилами вывода в этом разделе используется секвенциальная нотация ( ) вместо вертикального представления правил. В этой нотации $\vdash$

${\begin{array}{c}{\text{Premise }}1\\{\text{Premise }}2\\\hline {\text{Conclusion}}\end{array}}$

записывается как . $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$

Формальный язык классической пропозициональной логики может быть выражен только с помощью отрицания (¬), импликации (→) и пропозициональных символов. Хорошо известная аксиоматизация, включающая три схемы аксиом и одно правило вывода ( modus ponens ), выглядит так:

(CA1) ⊢ А → ( Б → А ) 
(CA2) ⊢ ( А → ( Б → С )) → (( А → В ) → ( А → С )) 
(CA3) ⊢ (¬ А → ¬ В ) → ( Б → А ) 
(МП) А , А → В ⊢ В

Может показаться излишним иметь два понятия вывода в этом случае, ⊢ и →. В классической пропозициональной логике они действительно совпадают; теорема дедукции утверждает, что A ⊢ B тогда и только тогда, когда ⊢ A → B . Однако есть различие, которое стоит подчеркнуть даже в этом случае: первая нотация описывает дедукцию , то есть деятельность по переходу от предложений к предложениям, тогда как A → B — это просто формула, сделанная с логической связкой , импликацией в этом случае. Без правила вывода (например, modus ponens в этом случае) нет ни дедукции, ни вывода. Этот момент проиллюстрирован в диалоге Льюиса Кэрролла под названием « Что сказала черепаха Ахиллесу » ^[3] , а также в более поздних попытках Бертрана Рассела и Питера Уинча разрешить парадокс, представленный в диалоге.

Для некоторых неклассических логик теорема дедукции не выполняется. Например, трехзначная логика Лукасевича может быть аксиоматизирована следующим образом: ^[4]

(CA1) ⊢ А → ( В → А ) 
(LA2) ⊢ ( А → В ) → (( В → С ) → ( А → С )) 
(CA3) ⊢ (¬ А → ¬ В ) → ( В → А ) 
(LA4) ⊢ (( А → ¬ А ) → А ) → А

(МП) А , А → В ⊢ В

Эта последовательность отличается от классической логики изменением аксиомы 2 и добавлением аксиомы 4. Классическая теорема о дедукции не верна для этой логики, однако ее измененная форма верна, а именно A ⊢ B тогда и только тогда, когда ⊢ A → ( A → B ). ^[5]

Допустимость и выводимость

В наборе правил правило вывода может быть избыточным в том смысле, что оно допустимо или выводимо . Выводимое правило — это правило, заключение которого может быть выведено из его предпосылок с использованием других правил. Допустимое правило — это правило, заключение которого выполняется всякий раз, когда выполняются предпосылки. Все выводимые правила допустимы. Чтобы оценить разницу, рассмотрим следующий набор правил для определения натуральных чисел ( суждение утверждает тот факт, что является натуральным числом): $n\,\,{\mathsf {nat}}$ $n$

{\begin{matrix}{\begin{array}{c}\\\hline {\mathbf {0} \,\,{\mathsf {nat}}}\end{array}}&{\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\end{array}}\end{matrix}}

Первое правило гласит, что 0 является натуральным числом, а второе гласит, что s( n ) является натуральным числом, если n является натуральным числом. В этой системе доказательств выводится следующее правило, демонстрирующее, что второй последующий элемент натурального числа также является натуральным числом:

{\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}\end{array}}

Его вывод — это композиция двух использований правила преемника выше. Следующее правило для утверждения существования предшественника для любого ненулевого числа просто допустимо:

{\begin{array}{c}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\\\hline {n\,\,{\mathsf {nat}}}\end{array}}

Это истинный факт натуральных чисел, как можно доказать индукцией . (Чтобы доказать, что это правило допустимо, предположим вывод посылки и проведем индукцию по нему, чтобы получить вывод .) Однако он невыводим, поскольку зависит от структуры вывода посылки. Из-за этого выводимость стабильна при дополнениях к системе доказательств, тогда как допустимость — нет. Чтобы увидеть разницу, предположим, что следующее бессмысленное правило было добавлено к системе доказательств: $n\,\,{\mathsf {nat}}$

{\begin{array}{c}\\\hline {\mathbf {s(-3)} \,\,{\mathsf {nat}}}\end{array}}

В этой новой системе правило двойного преемника все еще выводимо. Однако правило нахождения предшественника больше не является допустимым, поскольку нет способа вывести . Хрупкость допустимости исходит из способа ее доказательства: поскольку доказательство может быть индукцией по структуре выводов посылок, расширения системы добавляют новые случаи к этому доказательству, которые могут больше не выполняться. $\mathbf {-3} \,\,{\mathsf {nat}}$

Допустимые правила можно рассматривать как теоремы системы доказательств. Например, в последовательном исчислении , где выполняется исключение разреза , правило разреза является допустимым.

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

Ссылки

^ Булос, Джордж; Берджесс, Джон; Джеффри, Ричард К. (2007). Вычислимость и логика. Кембридж: Cambridge University Press. стр. 364. ISBN 978-0-521-87752-7.
^ Джон К. Рейнольдс (2009) [1998]. Теории языков программирования. Cambridge University Press. стр. 12. ISBN 978-0-521-10697-9.
^ Коста Досен (1996). "Логическое следствие: поворот в стиле". В Maria Luisa Dalla Chiara ; Kees Doets; Daniele Mundici; Johan van Benthem (ред.). Логика и научные методы: Том первый Десятого международного конгресса по логике, методологии и философии науки, Флоренция, август 1995 г. Springer. стр. 290. ISBN 978-0-7923-4383-7.препринт (с другой пагинацией)
^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантика, алгебры и системы вывода . Cambridge University Press. стр. 100. ISBN 978-0-521-88128-9.
^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантика, алгебры и системы вывода . Cambridge University Press. стр. 114. ISBN 978-0-521-88128-9.