Laboratory of Mathematical Logic at PDMI

Cреда, 29 мая, ПОМИ РАН, ауд. 106. Начало в 15:00.

Докладчик: С.Н. Артёмов (The Graduate Center of the City University of New York).

Тема: О доказательствах непротиворечивости.

Abstract

Теоремы Гёделя о неполноте основаны на арифметизации содержательных математических рассуждений в виде арифметических формул. При этом как Гёдель, так и Гильберт допускали, что такая арифметизация не покрывает всех «финитарных» методов, и отмечали, что теорема о неполноте не влечёт невозможность финитарных доказательств непротиворечивости.

Однако, получила распространение противоположная точка зрения, восходящая к фон Нейману, и состоящая в том, что гёделевская арифметизация покрывает все методы, выразимые в арифметике Пеано РА (а следовательно, и все финитарные методы), и что, тем самым, теорема Гёделя влечёт невозможность доказательства непротиворечивости РА методами, выразимыми в РА.

Мы приводим простой пример содержательного доказательства методами, выразимыми в РА, которое не представляется в виде единой формулы. Мы также даём математическое доказательство непротиворечивости РА методами, формализуемыми в РА; оно основано на известной технике частичных предикатов истинности.

В обоих случаях мы используем формализацию утверждения о непротиворечивости не в виде единой формулы, а в виде схемы формул. Это показывает, что включение в рассмотрение подобных схем необходимо для изучения доказательств непротиворечивости.

Приложение