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

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

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

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

• 1 Стандартная форма
• 2 Пример: системы Гильберта для двух логик высказываний
• 3 Допустимость и выводимость
• 4 См. Также
• 5 ссылки

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

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

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

${\ Displaystyle от A \ до B}$

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

${\ Displaystyle B \!}$

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

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

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

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

записывается как. ${\ displaystyle ({\ 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

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

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

(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 → Б).

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

${\ displaystyle {\ begin {matrix} {\ begin {array} {c} \\\ hline {\ mathbf {0} \, \, {\ mathsf {nat}}} \ end {array}} amp; {\ begin {массив} {c} {n \, \, {\ mathsf {nat}}} \\\ hline {\ mathbf {s (} n \ mathbf {)} \, \, {\ mathsf {nat}}} \ конец {массив}} \ конец {матрица}}}$

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

${\ displaystyle {\ begin {array} {c} {n \, \, {\ mathsf {nat}}} \\\ hline {\ mathbf {s (s (} n \ mathbf {))} \, \, {\ mathsf {нат}}} \ end {массив}}}$

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

${\ displaystyle {\ begin {array} {c} {\ mathbf {s (} n \ mathbf {)} \, \, {\ mathsf {nat}}} \\\ hline {n \, \, {\ mathsf {нат}}} \ конец {массив}}}$

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

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

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

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

• Схема аргументации
• Немедленный вывод
• Возражение против вывода
• Закон мысли
• Список правил вывода
• Логическая правда
• Структурное правило