Натуральный вывод (естественный вывод ) — тип логических исчислений , использующий для доказательства утверждений правила вывода , близкие к обычным содержательным методам рассуждений.
Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским . Наряду с исчислением секвенций относятся генценовскому типу , поскольку отталкиваются от безаксиоматического подхода (в противоположность гильбертовским исчислениям [англ.] , использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом
N
K
{\displaystyle \mathbf {NK} }
(для классического варианта исчисления предикатов ) и
N
J
{\displaystyle \mathbf {NJ} }
(для интуиционистского исчисления предикатов).
Правила вывода в исчислении
N
J
{\displaystyle \mathbf {NJ} }
:
введение конъюнкции :
A
B
A
∧ ∧ -->
B
{\displaystyle {\cfrac {A\quad B}{A\wedge B}}}
(«если верно
A
{\displaystyle A}
и
B
{\displaystyle B}
, то можно заключить
A
∧ ∧ -->
B
{\displaystyle A\wedge B}
»);
исключение конъюнкции:
A
∧ ∧ -->
B
A
{\displaystyle {\cfrac {A\wedge B}{A}}}
и
A
∧ ∧ -->
B
B
{\displaystyle {\cfrac {A\wedge B}{B}}}
;
введение дизъюнкции :
A
A
∨ ∨ -->
B
{\displaystyle {\cfrac {A}{A\vee B}}}
и
B
A
∨ ∨ -->
B
{\displaystyle {\cfrac {B}{A\vee B}}}
;
исключение дизъюнкции:
A
B
⋮ ⋮ -->
⋮ ⋮ -->
A
∨ ∨ -->
B
C
C
C
{\displaystyle {\begin{aligned}A\quad B\\\vdots \;\quad \vdots \;\\{\cfrac {A\vee B\quad C\quad C}{C}}\end{aligned}}}
(«если верно
A
∨ ∨ -->
B
{\displaystyle A\vee B}
, из
A
{\displaystyle A}
выводится
C
{\displaystyle C}
и из
B
{\displaystyle B}
выводится
C
{\displaystyle C}
, то можно заключить
C
{\displaystyle C}
»);
введение квантора всеобщности :
F
a
∀ ∀ -->
x
F
x
{\displaystyle {\cfrac {Fa}{\forall {x}Fx}}}
;
исключение квантора всеобщности:
∀ ∀ -->
x
F
x
F
a
{\displaystyle {\cfrac {\forall {x}Fx}{Fa}}}
;
введение квантора существования :
F
a
∃ ∃ -->
x
F
x
{\displaystyle {\cfrac {Fa}{\exists {x}Fx}}}
;
исключение квантора существования:
F
a
⋮ ⋮ -->
∃ ∃ -->
x
F
x
C
C
{\displaystyle {\begin{aligned}Fa\\\vdots \;\\{\cfrac {\exists {x}Fx\quad C}{C}}\end{aligned}}}
;
введение импликации :
A
⋮ ⋮ -->
B
A
⇒ ⇒ -->
B
{\displaystyle {\begin{aligned}A\\\vdots \;\\{\cfrac {\quad B}{A\Rightarrow B}}\end{aligned}}}
;
исключение импликации (modus ponens ):
A
A
⇒ ⇒ -->
B
B
{\displaystyle {\cfrac {A\quad A\Rightarrow B}{B}}}
;
введение отрицания :
A
⋮ ⋮ -->
⊥ ⊥ -->
¬ ¬ -->
A
{\displaystyle {\begin{aligned}A\\\vdots \;\\{\cfrac {\quad \bot }{\neg A}}\end{aligned}}}
;
исключение отрицания:
A
¬ ¬ -->
A
⊥ ⊥ -->
{\displaystyle {\cfrac {A\quad \neg A}{\bot }}}
;
выведение из ложного высказывания :
⊥ ⊥ -->
A
{\displaystyle {\cfrac {\bot }{A}}}
.
Классическая система
N
K
{\displaystyle \mathbf {NK} }
получается присоединением к этим правилам вывода аксиомы
A
∨ ∨ -->
¬ ¬ -->
A
{\displaystyle A\vee \neg A}
или добавлением правила двойного отрицания
¬ ¬ -->
¬ ¬ -->
A
A
{\displaystyle {\cfrac {\neg \neg A}{A}}}
.
Литература
Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М. : Наука, 1967. — С. 9—76 .
Гетманова А. Д. Логика. — Книжный дом «Университет», 1998. — 480 с.
Зиновьев А. А. Логика высказываний и теория вывода. — Питер, 2015. — 937 с.
Правиц Д. [швед.] . Натуральный вывод. Теоретико-доказательственное исследование / перевод П. Быстрова. — Лори, 1997.
Группы логик
Компоненты
Ссылки на внешние ресурсы
Словари и энциклопедии