Русская Википедия:Натуральный вывод

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

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

Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским. Наряду с исчислением секвенций относятся генценовскому типу, поскольку отталкиваются от безаксиоматического подхода (в противоположность Шаблон:Iw, использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом <math>\mathbf{NK}</math> (для классического варианта исчисления предикатов) и <math>\mathbf{NJ}</math> (для интуиционистского исчисления предикатов).

Правила вывода в исчислении <math>\mathbf{NJ}</math>:

  • введение конъюнкции:
    <math>\cfrac {A \quad B}{A \wedge B}</math> («если верно <math>A</math> и <math>B</math>, то можно заключить <math>A \wedge B</math>»);
  • исключение конъюнкции:
    <math>\cfrac{A \wedge B}{A}</math> и <math>\cfrac{A \wedge B}{B}</math>;
  • введение дизъюнкции:
    <math>\cfrac{A}{A \vee B}</math> и <math>\cfrac{B}{A \vee B}</math>;
  • исключение дизъюнкции:
    <math>\begin{align} A \quad B \\ \vdots \; \quad \vdots \; \\ \cfrac{A \vee B \quad C \quad C}{C} \end{align}</math> («если верно <math>A \vee B</math>, из <math>A</math> выводится <math>C</math> и из <math>B</math> выводится <math>C</math>, то можно заключить <math>C</math>»);
  • введение квантора всеобщности:
    <math>\cfrac{Fa}{\forall{x}Fx}</math>;
  • исключение квантора всеобщности:
    <math>\cfrac{\forall{x}Fx}{Fa}</math>;
  • введение квантора существования:
    <math>\cfrac{Fa}{\exists{x}Fx}</math>;
  • исключение квантора существования:
    <math>\begin{align} Fa \\ \vdots\; \\ \cfrac{\exists{x}Fx \quad C}{C} \end{align}</math>;
  • введение импликации:
    <math>\cfrac{B}{A \Rightarrow B}</math>;
  • исключение импликации (modus ponens):
    <math>\cfrac{A \quad A \Rightarrow B}{B}</math>;
  • введение отрицания:
    <math>\begin{align} A \\ \vdots\; \\ \cfrac{\quad \bot}{\neg A} \end{align}</math>;
  • исключение отрицания:
    <math>\cfrac{A \quad \neg A}{\bot}</math>;
  • выведение из ложного высказывания:
    <math>\cfrac{\bot}{A}</math>.

Классическая система <math>\mathbf{NK}</math> получается присоединением к этим правилам вывода аксиомы <math>A \vee\neg A</math> или добавлением правила двойного отрицания <math>\cfrac{\neg \neg A}{A}</math>.

Литература

Шаблон:Логика Шаблон:ВС