Главная
Новости
Строительство
Ремонт
Дизайн и интерьер

















Яндекс.Метрика





Натуральный вывод

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

Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским. Наряду с исчислением секвенций относятся генценовскому типу, поскольку отталкиваются от безаксиоматического подхода (в противоположность гильбертовским исчислениям, использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом N K {displaystyle mathbf {NK} } (для классического варианта исчисления предикатов) и N J {displaystyle mathbf {NJ} } (для интуиционистского исчисления предикатов).

Правила вывода в исчислении N J {displaystyle mathbf {NJ} } :

  • введение конъюнкции: A B A ∧ B {displaystyle {cfrac {Aquad B}{Awedge B}}} («если верно A {displaystyle A} и B {displaystyle B} , то можно заключить A ∧ B {displaystyle Awedge B} »);
  • исключение конъюнкции: A ∧ B A {displaystyle {cfrac {Awedge B}{A}}} и A ∧ B B {displaystyle {cfrac {Awedge B}{B}}} ;
  • введение дизъюнкции: A A ∨ B {displaystyle {cfrac {A}{Avee B}}} и B A ∨ B {displaystyle {cfrac {B}{Avee B}}} ;
  • исключение дизъюнкции: A B ⋮ ⋮ A ∨ B C C C {displaystyle {egin{aligned}Aquad Bvdots ;quad vdots ;{cfrac {Avee Bquad Cquad C}{C}}end{aligned}}} («если верно A ∨ B {displaystyle Avee 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 {egin{aligned}Favdots ;{cfrac {exists {x}Fxquad C}{C}}end{aligned}}} ;
  • введение импликации: B A ⇒ B {displaystyle {cfrac {B}{ARightarrow B}}} ;
  • исключение импликации (modus ponens): A A ⇒ B B {displaystyle {cfrac {Aquad ARightarrow B}{B}}} ;
  • введение отрицания: A ⋮ ⊥ ¬ A {displaystyle {egin{aligned}Avdots ;{cfrac {quad ot }{ eg A}}end{aligned}}} ;
  • исключение отрицания: A ¬ A ⊥ {displaystyle {cfrac {Aquad eg A}{ot }}} ;
  • выведение из ложного высказывания: ⊥ A {displaystyle {cfrac {ot }{A}}} .

Классическая система N K {displaystyle mathbf {NK} } получается присоединением к этим правилам вывода аксиомы A ∨ ¬ A {displaystyle Avee eg A} или добавлением правила двойного отрицания ¬ ¬ A A {displaystyle {cfrac { eg eg A}{A}}} .