| Правила трансформации |
|---|
| Исчисление высказываний |
| Правила вывода |
| Правила замены |
| Логика предикатов |
Правило вывода , правил вывода или правило преобразования является логической формой , состоящей из функции , которая принимает объект, анализирует их синтаксис и возвращает вывод (или выводы ). Например, правило вывода, называемое modus ponens, принимает две посылки, одну в форме «Если p, то q», а другую в форме «p», и возвращает заключение «q». Правило справедливо в отношении семантики классической логики (а также семантики многих других неклассических логик ) в том смысле, что если посылки верны (при интерпретации), то таков и вывод.
Обычно правило вывода сохраняет истину, семантическое свойство. В многозначной логике сохраняет общее обозначение. Но действие правила вывода является чисто синтаксическим и не требует сохранения каких-либо семантических свойств: любая функция от наборов формул до формул считается правилом вывода. Обычно важны только рекурсивные правила ; т.е. такие правила, что существует эффективная процедура для определения того, является ли какая-либо данная формула выводом данного набора формул в соответствии с правилом. Примером правила, неэффективного в этом смысле, является бесконечное ω-правило . [1]
Популярные правила вывода в логике высказываний включают modus ponens , modus tollens и противопоставление . Логика предикатов первого порядка использует правила вывода для работы с логическими квантификаторами .
Стандартная форма правил вывода [ править ]
В формальной логике (и во многих смежных областях) правила вывода обычно приводятся в следующей стандартной форме:
Предпосылка № 1
Предпосылка № 2
...
Предпосылка № n
Заключение
Это выражение утверждает, что всякий раз, когда в ходе некоторого логического вывода были получены данные посылки, указанный вывод также можно считать само собой разумеющимся. Точный формальный язык, который используется для описания как предпосылок, так и выводов, зависит от фактического контекста выводов. В простом случае можно использовать логические формулы, например:
Это правило логики высказываний modus ponens . Правила вывода часто формулируются как схемы, использующие метапеременные . [2] В приведенном выше правиле (схеме) метапеременные A и B могут быть конкретизированы для любого элемента вселенной (или иногда, по соглашению, ограниченного подмножества, такого как предложения ), чтобы сформировать бесконечный набор правил вывода.
Система доказательств формируется из набора правил, объединенных в цепочку для формирования доказательств, также называемых выводами . Любой вывод имеет только один окончательный вывод - утверждение, доказанное или выведенное. Если при выводе посылки остаются неудовлетворенными, то вывод является доказательством гипотетического утверждения: « если посылки верны, то вывод верен».
Пример: системы Гильберта для двух логик высказываний [ править ]
В системе Гильберта предпосылки и выводы правил вывода - это просто формулы некоторого языка, обычно использующие метапеременные. Для графической компактности представления и подчеркивания различия между аксиомами и правилами вывода в этом разделе вместо вертикального представления правил используется секвенциальная нотация ( ).
Формальный язык классической логики высказываний может быть выражен с помощью отрицания (¬), импликации (→) и пропозициональных символов. Хорошо известная аксиоматизация, включающая три схемы аксиом и одно правило вывода ( 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 ) нет дедукции или вывода. Этот момент проиллюстрирован вДиалог Льюиса Кэрролла под названием « Что черепаха сказала Ахиллу » [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]
Допустимость и выводимость [ править ]
В наборе правил правило вывода может быть избыточным в том смысле, что оно допустимо или выводимо . Выводимое правило - это правило, заключение которого может быть получено из его предпосылок с использованием других правил. Допустимое правило - это правило, вывод которого выполняется всякий раз, когда выполняются посылки. Допустимы все выводимые правила. Чтобы оценить разницу, рассмотрите следующий набор правил для определения натуральных чисел ( суждение утверждает тот факт, что это натуральное число):
Первое правило гласит, что 0 - натуральное число, а второе утверждает, что s (n) - натуральное число, если n есть. В этой системе доказательств выводится следующее правило, демонстрирующее, что второй последователь натурального числа также является натуральным числом:
Его происхождение - это комбинация двух применений правила преемника, описанного выше. Следующее правило утверждения существования предшественника для любого ненулевого числа просто допустимо:
Это истинный факт для натуральных чисел, что можно доказать по индукции . (Чтобы доказать, что это правило допустимо, предположите вывод посылки и проведите по ней индукцию, чтобы получить вывод .) Однако это не выводимо, потому что это зависит от структуры вывода посылки. Из-за этого выводимость стабильна при дополнениях к системе доказательства, в то время как допустимость - нет. Чтобы увидеть разницу, предположим, что в систему доказательства было добавлено следующее бессмысленное правило:
В этой новой системе все еще можно вывести правило двойного преемника. Однако правило поиска предшественника больше недопустимо, потому что нет возможности вывести его . Хрупкость допустимости проистекает из способа ее доказательства: поскольку доказательство может влиять на структуру выводов посылок, расширения системы добавляют к этому доказательству новые случаи, которые, возможно, больше не выполняются.
Допустимые правила можно рассматривать как теоремы системы доказательств. Например, в исчислении секвенций , где ликвидация покроя держится, вырезать правило допустимо.
См. Также [ править ]
- Схема аргументации
- Немедленный вывод
- Возражение против вывода
- Закон мысли
- Список правил вывода
- Логическая правда
- Структурное правило
Ссылки [ править ]
- ^ Булос, Джордж; Берджесс, Джон; Джеффри, Ричард С. (2007). Вычислимость и логика . Кембридж: Издательство Кембриджского университета. п. 364 . ISBN 0-521-87752-0.
- ^ Джон С. Рейнольдс (2009) [1998]. Теории языков программирования . Издательство Кембриджского университета. п. 12. ISBN 978-0-521-10697-9.
- ^ Kosta Dosen (1996). «Логическое следствие: поворот в стиле». В Марии Луизе Далла Кьяре ; Кис Доетс; Даниэле Мундичи; Йохан ван Бентем (ред.). Логика и научные методы: Том Один из десятого Международного конгресса по логике, методологии и философии науки, Флоренции, август 1995 года . Springer. п. 290. ISBN 978-0-7923-4383-7. препринт (с разной нумерацией страниц)
- ^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантика, алгебры и системы вывода . Издательство Кембриджского университета. п. 100 . ISBN 978-0-521-88128-9.
- ^ Бергманн, Мерри (2008). Введение в многозначную и нечеткую логику: семантика, алгебры и системы вывода . Издательство Кембриджского университета. п. 114 . ISBN 978-0-521-88128-9.
