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

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

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

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

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

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

Литература

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

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