Bar Induction is Compatible with Constructive Type Theory
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
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.
bibTex ref: RCB-771