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

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

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

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

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

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

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

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

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

$$\begin{gathered} \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). \end{gathered}$$