(Note: this has been rewritten to reflect the comments below). The answer to #1 is basically yes, because the proof that the Lindenbaum algebra above T is atomless is completely constructive. Start with T, and assume that T + ~Con(T) is consistent. Then there is a sentence S such that T + ~Con(T) neither proves nor disproves S (using the first incompleteness theorem via Rosser's trick). So T + ~Con(T)$\land$S is stronger than T + ~Con(T), but is still consistent. This means that T + ~(Con(T)$\lor$~S) is consistent, so T + Con(T)$\lor$~S is stonger than T. If T $\vdash$ (Con(T)$\lor$S) $\to$ Con(T) then T $\vdash$ S $\to$ Con(T). But this means T $\vdash$ ~Con(T) $\to$ ~S which is impossible. This shows that T + (Con(T)$\lor$S) < T+ Con(T) . So we can let T<sup>H</sup> be T + (Con(T)$\lor$S).