Теорема Гливенко — утверждение, отражающее связь между классами формул, выводимых в классическом и интуиционистском исчислении высказываний.
Формулировка Всякая формула, выводимая в интуиционистском исчислении высказываний, выводима и в классическом. Обратное неверно, однако для любой формулы языка логики высказываний (ЯЛВ), если в классическом исчислении высказываний, то в интиуиционистском исчислении высказываний.
Доказательство Индукция по длине вывода (в ). Для каждой из аксиом классического исчисления высказываний, входящих также в интуиционистское утверждение, очевидно, верно. Двойное отрицание аксиом вида получается путём приведения к абсурду их отрицания, влекущего как , так и . Переход индукции доказывается путём переноса правила modus ponens из классического вывода с добавлением двойного отрицания: если в интуиционистстком выводе и , то . Доказательство вновь использует приведение к абсурду: из , и выводимо . Это, в свою очередь доказывается путём приведения к абсурду набора , , и выводом из него .
Примечания
Литература
Категория:Логика Категория:Математическая логика