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

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

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

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

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

Литература

• Шаблон:Публикация