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 λ-terms that inhabit a formula.

A rewriting-system is associated with such λ-terms, and we show that a formula admits a BB′IW-λ-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 Nn, which is equivalent to Kripke’s Lemma.