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

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

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

Правила вывода в исчислении :

  • введение конъюнкции:
    («если верно и , то можно заключить »);
  • исключение конъюнкции:
    и ;
  • введение дизъюнкции:
    и ;
  • исключение дизъюнкции:
    («если верно , из выводится и из выводится , то можно заключить »);
  • введение квантора всеобщности:
    ;
  • исключение квантора всеобщности:
    ;
  • введение кватора существования:
    ;
  • исключение квантора существования:
    ;
  • введение импликации:
    ;
  • исключение импликации (modus ponens):
    ;
  • введение отрицания:
    ;
  • исключение отрицания:
    ;
  • введение ложного высказывания:
    .

Классическая система получается присоединением к этим правилам вывода аксиомы или добавлением правила двойного отрицания .

ЛитератураПравить

  • Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М.: Наука, 1967. — С. 9—76.
  • Гетманова А. Д. Логика. — Книжный дом «Университет», 1998. — 480 с.
  • Зиновьев А. А.  Логика высказываний и теория вывода. — Питер, 2015. — 937 с.
  • Правиц Д.[sv]. Натуральный вывод. Теоретико-доказательственное исследование / перевод П. Быстрова. — Лори, 1997.