Строгий логический вывод в формальной системе
Доказательство, построенное внутри формального исчисления (например, логики высказываний или арифметики Пеано), где каждый шаг строго регламентирован правилами вывода. Здесь важно не то, «что» утверждается, а то, «как» это выведено из аксиом.
Близкие слова
- формальный выводЧаще используется как синоним процесса, а не самого объекта-доказательства.
- синтаксическое доказательствоПодчеркивает опору на правила синтаксиса, а не на семантику.
В системе Пирса-Фреге теорема о законе исключённого третьего доказывается чисто формальными манипуляциями со знаками, без обращения к интуиции или опыту.
Компьютерный верификатор Coq принимает только формальные доказательства, проверяя каждый шаг на соответствие типам и правилам языка.
Алгоритмически проверяемая последовательность шагов
В информатике и теории сложности формальное доказательство рассматривается как объект, который можно проверить за полиномиальное время. Это свойство лежит в основе многих криптографических протоколов.
Близкие слова
- верифицируемое свидетельствоБолее общий термин, часто используемый в контексте компьютерных наук и криптографии.
Протокол zk-SNARK позволяет доказать владение секретом, предоставляя формальное доказательство, не раскрывая сам секрет.
Математики используют автоматические доказательства теорем, чтобы убедиться в корректности сложных алгоритмов шифрования.
Отличие от неформальных рассуждений
Неформальное доказательство опирается на понимание смысла слов, контекст и интуитивные допущения. Формальное же полностью абстрагируется от семантики: формулы воспринимаются как символы, а правила вывода — как механические операции. Это устраняет риск ошибок из-за двусмысленности естественного языка, но делает доказательства громоздкими и трудными для чтения человеком без специальных инструментов.
Значение в основаниях математики
Идея формализации возникла как ответ на логические парадоксы. Формальные доказательства позволяют точно определить понятие «математическая истина» через доказуемость в заданной аксиоматической системе. Теорема Гёделя о неполноте показала, что для достаточно богатых систем существуют истинные утверждения, не имеющие формального доказательства внутри самой системы.