Теорема Гливенко

Теорема Гливенко — утверждение, отражающее связь между классами $\mathrm {N_{i}}$-выводимых и $\mathrm {N_{k}}$-выводимых формул.

Примечание. $\mathrm {N_{k}}$ — классическая система естественного вывода, а $\mathrm {N_{i}}$ — интуиционистская система естественного вывода.

Известно, что если формула $\mathrm {N_{i}}$-выводима, то она $\mathrm {N_{k}}$-выводима. Обратное неверно.

Однако справедливо следующее утверждение, известное как теорема Гливенко.

Для любой формулы языка логики высказываний (ЯЛВ), если эта формула $\mathrm {N_{k}}$-выводима, то $\mathrm {N_{i}}$-выводимо её двойное отрицание, т. е. $\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. — УДК 510.6(075.8). — ISBN 978-5-98227-307-9.