Общезначимость теорем. Непротиворечивость L

Целью исчисления высказываний, как уже говорилось, является описание тавтологий как теорем некоторой теории. Такое описание полезно потому, что в дальнейшем исчисление высказываний включается в более широкие формальные теории, для которых уже нет другого определения теорем, кроме как через понятие формального вывода. Нашей ближайшей целью является доказательство того, что теоремами теории L являются все тавтологии, и только они. Вторая часть этого утверждения доказывается совсем просто.

Теорема общезначимости теории L.

Каждая теорема теории L является тавтологией алгебры высказываний.

Для ее доказательства достаточно проверить, во-первых, что каждая формула вида (А1)-(А3) является тавтологией. Во-вторых, из правила modus ponens для тавтологий (см. п.2.4) следует, что каждое применение МР в выводах теории L приводит к тавтологиям. Поэтому любое доказательство, вывод теорем в теории L, состоит только из тавтологий, так что все теоремы являются тавтологиями.

Из этой теоремы сразу вытекает непротиворечивость теории L, т.е. невозможность доказать в этой теории какую-нибудь формулу Ф вместе с ее отрицанием . Действительно, не может быть, чтобы обе формулы Ф и были тавтологиями, а поэтому они не могут быть одновременно теоремами теории L.

Отсюда же следует и так называемая абсолютная непротиворечивость L – невозможность существования в этой теории хотя бы одной недоказуемой формулы (если Ф не является тавтологией, то она не выводима в L).

Дата добавления: 2015-11-14