The Decidability of a Fragment of BB'IW-Logic

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



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.