Бар-индукция

Бар-инду́кция, индуктивный способ рассуждения, используемый в интуиционистской математике и состоящий в следующем. Пусть на конечных кортежах натуральных чисел заданы некоторые свойства ${\displaystyle R}$ и ${\displaystyle S}$ такие, что:

1) свойство ${\displaystyle R}$ разрешимо, т. е. для всякого кортежа ${\displaystyle \langle n_{1},\ldots ,n_{m}\rangle }$ эффективно выясняется, выполнено ${\displaystyle R}$ на этом кортеже или нет;

2) для всякой свободно становящейся последовательности ${\displaystyle \alpha }$ найдётся кортеж вида ${\displaystyle \langle \alpha (0),\ldots ,\alpha (n-1)\rangle }$, для которого выполнено ${\displaystyle R}$; при этом, если выполняется 2), то говорят, что ${\displaystyle R}$ «запирает» пустой кортеж ${\displaystyle \langle \ \rangle }$ (отсюда и название «бар-индукция» (от англ. bar – запирать, засов);

3) для всякого кортежа ${\displaystyle \pi }$ натуральных чисел, если ${\displaystyle R(\pi )}$, то ${\displaystyle S(\pi )}$ – т. н. базис бар-индукции;

4) если ${\displaystyle \langle n_{1},\ldots ,n_{m}\rangle }$ – кортеж такой, что для всякого натурального ${\displaystyle k}$ имеет место ${\displaystyle S{\bigl (}\langle n_{1},\ldots ,n_{m},k\rangle {\bigr )}}$, то необходимо ${\displaystyle S{\bigl (}\langle n_{1},\ldots ,n_{m}\rangle {\bigr )}}$; это свойство называют шагом бар-индукции.

Если выполняются перечисленные условия 1)–4), то принцип бар-индукции позволяет заключить, что имеет место ${\displaystyle S{\bigl (}\langle \ \rangle {\bigr )}}$.

Л. Э. Я. Брауэр предложил бар-индукцию как интуиционистски приемлемый способ рассуждения, указывающий на незавершённость, некоторую эффективную несчётность совокупности всех свободно становящихся последовательностей. В частности, было показано (С. К. Клини и независимо А. А. Марковым), что из принципа бар-индукции (фактически даже из некоторого следствия теоремы о веере бар-индукции) следует, что не все свободно становящиеся последовательности рекурсивны.

С 60-х гг. 20 в. в основаниях математики нашли употребление формы бар-индукции, рассматривающие не кортежи натуральных чисел, а кортежи более сложных объектов, например кортежи свободно становящихся последовательностей.

На языке формального интуиционистского математического анализа бар-индукция может быть записана в виде:

${\displaystyle \forall x\,(R(x)\lor \lnot R(x))\And \forall \alpha \,\exists x\,R({\overline {\alpha }}(x))\And \ \forall x\,(R(x)\supset S(x))\And \ \forall x\,(\forall y\,S(x{\mathbin {*}}{\hat {y}})\supset S(x))\supset S(0).}$