Бар-індукція — у математичній логіці та теорії множин: спеціальний принцип індукції, застосовний до добре впорядкованих множин, зокрема до ординалів, який дозволяє доводити властивості для всіх елементів, спираючись на припущення, що властивість виконується для всіх попередніх елементів. Назва походить від символу, що позначає порожню множину або кінець доказу (∅), який у англомовній традиції називається «bar».
Бар-індукція — у конструктивній математиці та інтуїціоністській логіці: принцип доказу, заснований на ідеї, що будь-яка обчислювана функція, визначена на дереві (наприклад, на множині кінцевих послідовностей), має бар, тобто скінченну множину, що перетинає всі нескінченні шляхи в цьому дереві. Цей принцип є важливим інструментом в інтуїціоністському аналізі.