Правило вывода - Rule of inference

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

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

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

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

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

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

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

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

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

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

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

записывается как .

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

(CA1) ⊢ A → (BA)
(CA2) ⊢ (A → (BC)) → ((AB) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(MP) A, ABB

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

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

(CA1) ⊢ A → (BA)
(LA2) ⊢ (AB) → ((BC) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(LA4) ⊢ ((A → ¬A) → A) → A
(MP) A, ABB

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

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

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

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

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

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

В этой новой системе все еще можно вывести правило двойного преемника. Однако правило поиска предшественника больше недопустимо, потому что нет возможности вывести его . Хрупкость допустимости проистекает из способа ее доказательства: поскольку доказательство может влиять на структуру выводов посылок, расширения системы добавляют к этому доказательству новые случаи, которые, возможно, больше не выполняются.

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

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

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