# * Bar Induction is Compatible with Constructive Type Theory *

## by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable

2018

**Powerful yet effective induction principles play an important role in computing, being a paramount**

component of programming languages, automated reasoning and program verification systems. The Bar

Induction principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of

transfinite induction. In this work we investigate the compatibility of several variants of Bar Induction with

Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We

first show that CTT is compatible with a Bar Induction principle for sequences of numbers. Then, we establish

the compatibility of CTT with a more general Bar Induction principle for sequences of name-free closed terms.

The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit

constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding Bar

Induction, such as the non-truncated version of Bar Induction on monotone bars being intuitionistically false.

These enhancements are carried out formally using the Nuprl proof assistant which implements CTT, and the

formalization of CTT within the Coq proof assistant presented in previous works.

component of programming languages, automated reasoning and program verification systems. The Bar

Induction principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of

transfinite induction. In this work we investigate the compatibility of several variants of Bar Induction with

Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We

first show that CTT is compatible with a Bar Induction principle for sequences of numbers. Then, we establish

the compatibility of CTT with a more general Bar Induction principle for sequences of name-free closed terms.

The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit

constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding Bar

Induction, such as the non-truncated version of Bar Induction on monotone bars being intuitionistically false.

These enhancements are carried out formally using the Nuprl proof assistant which implements CTT, and the

formalization of CTT within the Coq proof assistant presented in previous works.