 The assumption of ω-consistency in the First Incompleteness Theorem was eliminated by Rosser in 1936, and replaced by the weaker notion of consistency. Rosser’s generalization involves applying the fixed point theorem to the formula R(x): ‘for all z: either z is not the Gödel number of a proof of the formula with Gödel number x or there is a proof shorter than z of the negation of (the formula with Gödel number) x’ (see Rosser 1936).