Анатомия доказательства

☀️ Естественный вывод: как мы доказываем теоремы на самом деле
В классических формальных системах (как у Гильберта) доказательства выглядят как длинные списки формул, где каждая строка следует из предыдущих по одному правилу. Это неудобно и не похоже на то, как рассуждает человек.
Математическое ядро:
В 1934 году Герхард Генцен и независимо Станислав Яськовский создали систему естественного вывода. Здесь доказательства строятся как деревья, а не как линейные списки.
Главная идея — пары правил для каждой логической связки:
1. Правила введения: Как мы можем получить утверждение? (Например, чтобы доказать «А и В», нужно отдельно доказать А и отдельно доказать В).
2. Правила удаления: Как мы можем использовать утверждение? (Если у нас есть «А и В», мы можем смело взять А).
Это невероятно элегантно. Доказательство в естественном выводе выглядит как дерево, где в корне стоит теорема, а в листьях — аксиомы или допущения.
Зачем это нужно?
Естественный вывод — это основа современных систем автоматического доказательства теорем (например, Coq или Lean). Компьютеру гораздо проще проверять и строить доказательства в формате деревьев Генцена, чем в классических аксиоматических системах.