Rosser Sentence

A variant of a Gödel sentence constructed using Rosser's trick that weakens the hypotheses needed for incompleteness: it yields an undecidable sentence for any consistent, recursively enumerable theory without requiring ω-consistency, by using a modified provability predicate comparing proof lengths.