Wnat about Gödel incompleteness? Comptuers aren't formal systems. Turing machines have no notion of truth. Their programs may. So a program can have M > N axioms in which case one of the N+1 axioms recognizes the truth that G ≡ ¬ Prov_S(⌜ G ⌝) because it was constructed to be true. Alternatively, construct a system that generates "truth" statements, subject to further verification. After all, some humans think that "Apollo never put men on the moon" is a true statement.

As for intentionality, programs have intentionality.