First-order logic and computer science

In the previous article, we discussed the halting problem and its relation to Godel's incompleteness theorem. The essence is as follows: suppose I am programmed to do something I don't predict I will (this is allowed by the definition of a computer). Fundamentally, this means that where T is my theory of my mind and G is the thing I will do, T entails that G ⇔ ¬(T⊢G). Our belief in G then stems from our belief in the soundness of T, that (T⊢G) ⟹ G – thus if T were sound, it wouldn't believe in its own soundness.