Гуманитарные технологии Информационно-аналитический портал • ISSN 2310-1792
Гуманитарно-технологическая парадигма

Логический вывод

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

Логический вывод — это рассуждение (см. Рассуждение), в ходе которого осуществляется переход от исходного суждения (высказывания или системы высказываний) с помощью логических правил к заключению — новому суждению (высказыванию или системе высказываний).

К логическому выводу обычно предъявляются (совместно или по отдельности) два основных требования:

  1. Правила перехода должны воспроизводить отношение логического следования (ту или иную его разновидность);
  2. Переходы в логическом выводе должны осуществляться на основе учёта только синтаксических характеристик высказываний или систем высказываний.

В современной логике понятие логического вывода определяется для формальных систем, в которых высказывания представлены формулами. Обычно выделяют три основных типа формальных систем: аксиоматические исчисления, исчисления натурального вывода, исчисления секвенций. Стандартное определение логического вывода (из множества формул Г) для аксиоматического исчисления S таково: логический вывод в S из множества формул Г есть такая последовательность Α1An формул языка исчисления S, что для каждой Ai (1 ≤ i ≤ n) выполняется, по крайней мере, одно из следующих трёх условий:

  • Ai есть формула из Г;
  • Ai есть аксиома исчисления S;
  • Ai есть формула, получающаяся из предшествующей ей в последовательности A1 … An формулы или из предшествующих ей в этой последовательности формул по одному из правил вывода исчисления S.

Если α есть логический вывод в S из множества формул Г, то формулы из Г называются посылками α, a сам вывод α называется выводом в S из посылок Г; если при этом A есть последняя формула α, то α называется логическим выводом в S формулы A из посылок Г. Запись «Г ⊦ sA» означает, что существует логический вывод в S формулы A из посылок Г. Логический вывод в S из пустого множества формул называется доказательством в S. Запись «⊦ s A» означает, что существует доказательство в S формулы A. Формула A называется доказуемой в S, если ⊦ A.

В качестве примера рассмотрим аксиоматическое исчисление S1 со стандартным определением вывода, являющееся вариантом классической логики высказываний. Алфавит этого исчисления содержит только пропозициональные переменные p1p2, … pn, … логические связки ⊃, ⌉ и круглые скобки. Определение формулы в этом языке обычное. Аксиомы S1 — это формулы следующих шести видов (и только эти формулы):

I. (A ⊃ A);
II. (A ⊃ B) ⊃ (B ⊃ C) ⊃ (A ⊃ C);
III. (A ⊃ (B ⊃ C) ⊃ (B ⊃ (A ⊃ C)));
IV. (A ⊃ (⌉B)) ⊃ (B ⊃ (⌉A)));
V. (⌉ (⌉A) ⊃ A);
VI. (A ⊃ B) ⊃ A) ⊃ A).

Единственное правило исчисления S1 modus ponens: A ⊃ B ⊦ B.

Определение логического вывода для S1 является очевидной конкретизацией определения, данного выше. Следующая последовательность формул Ф1 — Ф6 является логическим выводом в S1 формулы (p1 ⊃ p2) ⊃ (p2) из посылок (p1).

Ф1. ((p1 ⊃ p2) ⊃ (p1 ⊃ p2),
Ф2. (((p1 ⊃ p2) ⊃ (p1 ⊃ p2) ⊃ (p1 ⊃ (p1 ⊃ p2) ⊃ p2),
Ф3. (p1 ⊃ (p1 ⊃ p2) ⊃ p2),
Ф4. p1,
Ф5. (p1 ⊃ p2) ⊃ p2).

Анализ: Ф1 есть аксиома вида I, Ф2 есть аксиома вида III, ФЗ получена по правилу modus ponens из Ф1 и Ф2, Ф4 есть посылка, Ф5 получена по правилу modus ponens из Ф4 и ФЗ. Итак, {p1} ⊦ s1 ((p1 ⊃ p2) ⊃ p2). Рассмотрев последовательность формул Φ1, Φ2, Ф3, убеждаемся, что ⊦ s1 (p1 ⊃ p2) ⊃ p2).

В ряде случаев логический вывод определяется так, что на использование некоторых правил накладываются ограничения. Например, в аксиоматических исчислениях, являющихся вариантами классической логики предикатов первого порядка (см. Логика предикатов) и содержащих среди правил вывода только modus ponens и правило обобщения, логический вывод часто определяется так, что на использование правила обобщения накладывается ограничение: любое применение правилам обобщения в α таково, что переменная, по которой проводится обобщение в этом применении правила обобщения, не входит ни в одну посылку, предшествующую в α нижней формуле этого применения правила обобщения. Цель этого ограничения обеспечить ряд полезных с точки зрения логики свойств вывода (например, выполнение для простых форм теоремы дедукции).

Существуют определения логического вывода (как для аксиоматических, так и для исчислений других типов), которые:

  • задают логический вывод не только из множества посылок, но допускают другие формы организации посылок (например, списки или последовательности);
  • структурируют вывод не только линейно, но, например, в форме дерева;
  • имеют явно выраженный индуктивный характер; при этом индуктивное определение вывода может вестись как по одной переменной (например, по длине вывода), так и по нескольким переменным (например, по длине логического вывода и по числу его посылок);
  • содержат формализацию зависимости между формулами в логическом выводе, и многие другие определения логического вывода, обусловленные иными способами формализации и аксиоматизации классических и неклассических систем логики.
Источник: Логический вывод. Гуманитарная энциклопедия [Электронный ресурс] // Центр гуманитарных технологий, 2010–2016 (последняя редакция: 30.10.2016). URL: http://gtmarket.ru/concepts/6918
Текст статьи: © В. М. Попов. Подготовка электронной публикации и общая редакция: Центр гуманитарных технологий.
Ограничения: Настоящая публикация охраняется в соответствии с законодательством Российской Федерации об авторском праве и предназначена только для некоммерческого использования в информационных, образовательных и научных целях. Копирование, воспроизведение и распространение текстовых, графических и иных материалов, представленных на данной странице, не разрешено.
Реклама:
Содержание раздела
Новые концепты
Базисные концепты