Uniform density in Lindenbaum Algebras

Abstract

In this paper we prove that the preordering ≲ of provable implication over any recursively enumerable theory T containing a modicum of arithmetic is uniformly dense. This means that we can find a recursive extensional density function F for ≲. A recursive function F is a density function if it computes, for A and B with A ≤≁ B, an element C such that A ≤≁ C ≤≁ B. The function is extensional if it preserves T -provable equivalence. Secondly, we prove a general result that implies that, for extensions of elementary arithmetic, the ordering ≲ restricted to σn-sentences is uniformly dense. In the last section we provide historical notes and background material.