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

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

Например, правило вывода, называемое 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) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP)  A, A → B ⊢ B

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

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

(CA1) ⊢ A → (B → A)

(LA2) ⊢ (A → B) → ((B → C) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(LA4) ⊢ ((A → ¬A) → A) → A

(MP)  A, A → B ⊢ B

Эта последовательность отличается от классической логики изменением аксиомы 2 и добавлением аксиомы 4. Классическая теорема о дедукции не справедлива для этой логики, однако имеет место модифицированная форма, а именно A ⊢ B тогда и только тогда, когда ⊢ A → ( A → Б ). ^[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). Вычислимость и логика . Кембридж: Издательство Кембриджского университета. п. 364 . ISBN 978-0-521-87752-7 .
^ Джон К. Рейнольдс (2009) [1998]. Теории языков программирования . Издательство Кембриджского университета. п. 12. ISBN 978-0-521-10697-9 .
^ Коста Досен (1996). «Логическое следствие: поворот в стиле» . В Марии Луизе Далла Кьяра ; Кес Доэтс; Даниэле Мундичи; Йохан ван Бентем (ред.). Логика и научные методы: первый том Десятого Международного конгресса по логике, методологии и философии науки, Флоренция, август 1995 г. Спрингер. п. 290. ИСБН 978-0-7923-4383-7 . препринт (с разной нумерацией страниц)
^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантику, алгебры и системы вывода . Издательство Кембриджского университета. п. 100 . ISBN 978-0-521-88128-9 .
^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантику, алгебры и системы вывода . Издательство Кембриджского университета. п. 114 . ISBN 978-0-521-88128-9 .

[1] Булос, Джордж; Берджесс, Джон; Джеффри, Ричард С. (2007). Вычислимость и логика . Кембридж: Издательство Кембриджского университета. п. 364 . ISBN 978-0-521-87752-7 .

[Reynolds2009-2] Джон К. Рейнольдс (2009) [1998]. Теории языков программирования . Издательство Кембриджского университета. п. 12. ISBN 978-0-521-10697-9 .

[ChiaraDoets1996-3] Коста Досен (1996). «Логическое следствие: поворот в стиле» . В Марии Луизе Далла Кьяра ; Кес Доэтс; Даниэле Мундичи; Йохан ван Бентем (ред.). Логика и научные методы: первый том Десятого Международного конгресса по логике, методологии и философии науки, Флоренция, август 1995 г. Спрингер. п. 290. ИСБН 978-0-7923-4383-7 . препринт (с разной нумерацией страниц)

[4] Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантику, алгебры и системы вывода . Издательство Кембриджского университета. п. 100 . ISBN 978-0-521-88128-9 .

[5] Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантику, алгебры и системы вывода . Издательство Кембриджского университета. п. 114 . ISBN 978-0-521-88128-9 .

[1]

[2]

[3]

[4]

[5]