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

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

Впервые такие исчисления созданы в 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>.

Литература

• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга