Теорема Гливенко — утверждение, отражающее связь между классами ${\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)}$ .

В. И. Гливенко (1897–1940) — советский математик, логик.

Литература

• Тимофеева И. Л. / Ответств. ред. Н. В. Валуева. — 2-е изд., перераб. — М. : КДУ, 2007. — 304 с. — 1000 экз. — ББК 22.12я73 . — УДК . — ISBN 978-5-98227-307-9 .