Gödel's second incompleteness theorem also implies that a system "F"1 satisfying the technical conditions outlined above cannot prove the consistency of any system "F"2 that proves the consistency of "F"1. This is because such a system "F"1 can prove that if "F"2 proves the consistency of "F"1, then "F"1 is in fact consistent. For the claim that "F"1 is consistent has form "for all numbers "n", "n" has the decidable property of not being a code for a proof of contradiction in "F"1". If "F"1 were in fact inconsistent, then "F"2 would prove for some "n" that "n" is the code of a contradiction in "F"1. But if "F"2 also proved that "F"1 is consistent (that is, that there is no such "n"), then it would itself be inconsistent. This reasoning can be formalized in "F"1 to show that if "F"2 is consistent, then "F"1 is consistent. Since, by second incompleteness theorem, "F"1 does not prove its consistency, it cannot prove the consistency of "F"2 either.