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

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

Основные понятия

В основе любого правила вывода лежит отношение логического следования. Если из набора посылок \( A_1, A_2, \ldots, A_n \) логически следует заключение \( B \), то правило вывода, имеющее вид:

\[ \frac{A_1, A_2, \ldots, A_n}{B} \]

считается корректным (или дедуктивно верным) при условии, что в любой интерпретации, в которой истинны все посылки, истинно и заключение. Само правило не утверждает истинности посылок — оно лишь устанавливает, что заключение может быть выведено, если посылки приняты.

Различают несколько типов правил вывода:

• Дедуктивные — гарантируют истинность заключения при истинности посылок.
• Индуктивные — позволяют делать вероятностные или обобщающие выводы, но не гарантируют абсолютной истинности.
• Абдуктивные — выводят наиболее правдоподобное объяснение наблюдаемым фактам.

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

Классические правила вывода

Modus Ponens (правило отделения)

Одно из наиболее фундаментальных правил. Если истинна импликация «Если A, то B» и истинно A, то можно заключить B.

\[ \frac{A \to B, \ A}{B} \]

Пример: «Если идёт дождь, то земля мокрая. Дождь идёт. Следовательно, земля мокрая».

Modus Tollens (правило отрицания)

Если истинна импликация «Если A, то B» и ложно B, то можно заключить, что ложно A.

\[ \frac{A \to B, \ \neg B}{\neg A} \]

Пример: «Если идёт дождь, то земля мокрая. Земля не мокрая. Следовательно, дождь не идёт».

Правило силлогизма (транзитивность импликации)

Если из A следует B, а из B следует C, то из A следует C.

\[ \frac{A \to B, \ B \to C}{A \to C} \]

Пример: «Если число делится на 6, то оно делится на 3. Если число делится на 3, то оно делится на 9?» — этот пример ошибочен; правильный пример: «Если число делится на 6, то оно чётное. Если число чётное, то оно делится на 2. Следовательно, если число делится на 6, то оно делится на 2».

Правило введения конъюнкции

Из двух утверждений A и B можно вывести их конъюнкцию A и B.

\[ \frac{A, \ B}{A \land B} \]

Правило удаления конъюнкции

Из конъюнкции A и B можно вывести как A, так и B по отдельности.

\[ \frac{A \land B}{A}, \quad \frac{A \land B}{B} \]

Правило введения дизъюнкции

Из A можно вывести дизъюнкцию A или B (для любого B).

\[ \frac{A}{A \lor B} \]

Правило удаления дизъюнкции (доказательство разбором случаев)

Если истинна дизъюнкция A или B, и из A следует C, и из B следует C, то можно заключить C.

\[ \frac{A \lor B, \ A \to C, \ B \to C}{C} \]

Правило двойного отрицания

Из A можно вывести \(\neg\neg A\), и наоборот.

\[ \frac{A}{\neg\neg A}, \quad \frac{\neg\neg A}{A} \]

Правило введения импликации (теорема о дедукции)

Если, приняв A в качестве допущения, удалось вывести B, то можно заключить \(A \to B\) без допущения.

\[ \frac{[A] \vdash B}{A \to B} \]

Здесь \(\vdash\) означает «доказуемо».

Правила вывода в исчислении предикатов

В исчислении предикатов к пропозициональным правилам добавляются правила, связанные с кванторами.

Правило введения квантора общности

Если утверждение P(x) доказано для произвольного x (без дополнительных ограничений), то можно вывести \(\forall x P(x)\).

\[ \frac{P(x)}{\forall x P(x)} \]

Правило удаления квантора общности (конкретизация)

Из \(\forall x P(x)\) можно вывести P(t) для любого терма t, подставимого вместо x.

\[ \frac{\forall x P(x)}{P(t)} \]

Правило введения квантора существования

Из P(t) можно вывести \(\exists x P(x)\).

\[ \frac{P(t)}{\exists x P(x)} \]

Правило удаления квантора существования

Если доказано \(\exists x P(x)\) и из P(c) (где c — новая константа, не входящая в другие допущения) выведено Q, то можно заключить Q.

\[ \frac{\exists x P(x), \ [P(c)] \vdash Q}{Q} \]

Натуральное исчисление и секвенциальное исчисление

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

• Натуральное исчисление (Генцен, 1934) — набор правил введения и удаления для каждой логической связки и квантора. Доказательство строится как дерево вывода, где каждый шаг соответствует применению одного правила. Это наиболее близкая к естественным рассуждениям формальная система.

• Секвенциальное исчисление — оперирует не одиночными формулами, а секвенциями вида \(\Gamma \vdash \Delta\), где \(\Gamma\) и \(\Delta\) — последовательности формул. Правила вывода в нём симметричны (вводить или удалять связки можно как слева, так и справа от \(\vdash\)). Ключевое свойство — теорема об устранении сечения (Gentzen’s Hauptsatz), которая позволяет строить доказательства без «подглядывания вперёд».

Правила вывода в информатике и искусственном интеллекте

В информатике правила вывода применяются в системах логического вывода, экспертных системах, базах знаний и языках программирования с логикой (например, Пролог).

Modus Ponens в продукционных системах

Большинство экспертных систем (например, MYCIN, CLIPS) используют правило Modus Ponens как основной механизм вывода. Правила вида «ЕСЛИ условие ТО действие» интерпретируются как импликации: при активации условия действие считается выполненным.

Резолюция (принцип резолюции)

Основной метод автоматического доказательства теорем, предложенный Дж. Робинсоном в 1965 году. Правило резолюции применяется к дизъюнктам (формулам в виде дизъюнкции литералов):

\[ \frac{A \lor B, \quad \neg A \lor C}{B \lor C} \]

Резолюция является единственным правилом вывода в логике предикатов, достаточным для полноты доказательства (после приведения формул к клаузальной форме). Этот принцип лёг в основу языка Пролог и многих систем автоматического доказательства теорем (например, Vampire, E Prover).

Вывод по аналогии и индуктивные правила

В системах машинного обучения и рассуждений на основе прецедентов (CBR) используются неклассические правила вывода: индуктивные — обобщение частных случаев; абдуктивные — поиск наиболее правдоподобной гипотезы, объясняющей наблюдения; аналоговые — перенос свойств одного объекта на другой на основе сходства.

Продукция Рете

Алгоритм Рете (Retá, Чарльз Форджи, 1979) — эффективный метод сопоставления множества правил (продукций) с изменяющейся базой фактов. Используется в экспертных системах и языках правил (например, Drools, CLIPS). Правила вывода в нём представлены в виде сети узлов, через которую проходят факты, активирующие соответствующие правила.

Критика и ограничения

Классические правила вывода (особенно Modus Ponens и Modus Tollens) считаются незыблемыми в рамках дедуктивной логики. Однако существуют направления, ставящие под сомнение их универсальность:

• Интуиционистская логика (Л. Э. Я. Брауэр, А. Гейтинг) отвергает правило снятия двойного отрицания и исключённого третьего, требуя конструктивного доказательства.
• Немонотонные логики допускают отмену вывода при поступлении новой информации — классические правила вывода монотонны (если из A следует B, то из A и любой дополнительной посылки C также следует B).
• Паранепротиворечивые логики допускают одновременную истинность противоречащих утверждений, что делает некорректными правила, связанные с принципом взрыва (из противоречия следует любое утверждение).
• Логики с вероятностными или нечёткими правилами вывода (например, нечёткая логика Лотфи Заде) используют взвешенные или градуированные версии Modus Ponens, где степень истинности заключения зависит от степени истинности посылки.

Интересные факты

• Правило Modus Ponens в неявном виде использовалось ещё Аристотелем в трактате «Первая аналитика» (IV век до н. э.).
• Принцип резолюции, лежащий в основе многих автоматических доказателей, был открыт независимо несколькими исследователями, но наибольшее признание получила работа Дж. Робинсона.
• В знаменитом «Трактате» Л. Витгенштейна (1921) была впервые предложена концепция таблиц истинности для проверки корректности правил вывода.
• Крупнейшие проекты автоматического доказательства теорем, такие как Mizar, Isabelle, Coq, используют десятки или сотни формальных правил вывода, включая те, что описаны выше, но в систематизированной и строгой форме.
• В СССР и России значительный вклад в теорию правил вывода внесли А. А. Марков (нормальные алгоритмы), С. Ю. Маслов (метод резолюций в исчислении предикатов), а также В. А. Смирнов (формальные системы и теория доказательств).

Источники

1. Генцен Г. Исследования логических выводов / пер. с нем. — М.: Наука, 1975.
2. Клини С. К. Математическая логика. — М.: Мир, 1973.
3. Робинсон Дж. Машино-ориентированная логика, основанная на принципе резолюции // Кибернетический сборник. — 1970. — № 7.
4. Виноградова Е. Б., Кузнецов С. О. Логика и теория алгоритмов. — М.: МГУ, 2012.
5. Марков А. А. Элементы математической логики. — М.: МГУ, 1984.