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

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

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

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

Стандартная форма правил вывода

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

Помещение # 1
Помещение # 2
        ...
Помещение № n
Вывод

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

${\displaystyle A\to B}$

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

${\displaystyle B\!}$

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

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

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

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

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

(CA1) ⊢ А → (B → А)
(CA2) ⊢ (А → (B → C)) → ((А → B) → (А → C))
(CA3) ⊢ (¬А → ¬B) → (B → А)
(МП) А, А → B ⊢ B

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

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

(CA1) ⊢ А → (B → А)
(LA2) ⊢ (А → B) → ((B → C) → (А → C))
(CA3) ⊢ (¬А → ¬B) → (B → А)
(LA4) ⊢ ((А → ¬А) → А) → А
(МП) А, А → B ⊢ B

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

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

Основная статья: Допустимое правило

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

${\displaystyle {\begin{matrix}{\frac {}{\mathbf {0} \,\,{\mathsf {nat}}}}&{\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}}\\\end{matrix}}}$

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

${\displaystyle {\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}}}$

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

${\displaystyle {\frac {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}{n\,\,{\mathsf {nat}}}}}$

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

${\displaystyle {\frac {}{\mathbf {s(-3)} \,\,{\mathsf {nat}}}}}$

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

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

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

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

Рекомендации

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