&gt; for any non-trivial property, there is no general decision procedure that, for all programs<p>&gt; all but the most trivial axiomatic systems<p>This is about non-trivial <i>properties</i> on arbitrary programs, and non-trivial <i>axiomatic systems</i> proving arbitrary statements. It is not about non-trivial <i>programs</i> or non-trivial <i>statements</i>.<p>Rice&#x27;s theorem states that, for all non-trivial properties P, there exists a program S where you cannot compute P(S). (The Wikipedia phrasing puts the negative in a different spot, but this is de Morgan&#x27;s law for quantifiers: ∀P ¬∀S P(S) is computable = ∀P ∃S ¬ P(S) is computable.)<p>Gödel&#x27;s first theorem is that, for all non-trivial formalizations P, there exists a statement S where you cannot prove P in S.<p>You are claiming, for all non-trivial properties P, <i>for all non-trivial programs S</i>, you cannot compute P(S); for all non-trivial formalizations P, <i>for all non-trivial statements S</i>, you cannot prove P in S.<p>This is not what Rice&#x27;s or Gödel&#x27;s theorems are, and not what the texts you quoted say.<p>&gt; Then Gödel shows up and says, &quot;On which shelf shall we put the index?&quot;<p>You keep it outside the library. The index tells you where <i>every single book</i> is, other than the index.<p>In particular, Gödel claims that, if the index has any chance of being correct, it <i>must</i> be outside the library. The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct; in fact, Gödel&#x27;s second theorem means that if it <i>could</i> be proven in itself, we&#x27;d be confident it was wrong!