Sabine Broda, Luís Damas, Marcelo Finger, Paulo Silva e Silva

TCS'??

Abstract

Despite its simple formulation, the decidability of the logic BB'iW
has remained an open problem. We present here a decision procedure for
a fragment of it, called the arity-1 formulas.
The decidability proof is based on a representation of formulas called
formula-trees, which is coupled with a proof method that computes long
normal lambda-terms that inhabit a formula.
A rewriting-system is associated with such lambda-terms, and we show
that a formula admits a BB'IW-lambda-term if and only if the
associated rewriting-system terminates. The fact that termination is
decidable is proved using a result on the finiteness of non-ascending
sequences of n-tuples in N^n, which is equivalent to Kripke Lemma.