Uniform Density in Lindenbaum Algebras
V. Yu. Shavrukov, Albert Visser · Notre Dame Journal of Formal Logic · 2014
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.