Меню Главная Случайная статья Настройки Теорема Гливенко Материал из https://ru.wikipedia.org Теорема Гливенко — утверждение, отражающее связь между классами ${\displaystyle \mathrm {N_{i}} }$-выводимых и ${\displaystyle \mathrm {N_{k}} }$-выводимых формул. Примечание. ${\displaystyle \mathrm {N_{k}} }$ — классическая система естественного вывода, а ${\displaystyle \mathrm {N_{i}} }$ — интуиционистская система естественного вывода. Известно, что если формула ${\displaystyle \mathrm {N_{i}} }$-выводима, то она ${\displaystyle \mathrm {N_{k}} }$-выводима. Обратное неверно. Однако справедливо следующее утверждение, известное как теорема Гливенко. Для любой формулы языка логики высказываний (ЯЛВ), если эта формула ${\displaystyle \mathrm {N_{k}} }$-выводима, то ${\displaystyle \mathrm {N_{i}} }$-выводимо её двойное отрицание, т. е. ${\displaystyle \left({\mathcal {F}}\right)\left(\vdash _{\mathrm {N_{k}} }{\mathcal {F}}\quad \longrightarrow \quad \vdash _{\mathrm {N_{i}} }\neg \neg {\mathcal {F}}\right)}$. Литература Тимофеева И. Л. Математическая логика. Курс лекций: Учеб. пособие для студентов вузов / Ответств. ред. Н. В. Валуева. — 2-е изд., перераб. — М. : КДУ, 2007. — 304 с. — 1000 экз. — ББК 22.12я73. — УДК 510.6(075.8)(G). — ISBN 978-5-98227-307-9.