but to show that a specific Gödel proposition – neither provable nor disprovable using the axioms and rules of the formal system under consideration – is clearly seen, using our insights into the meanings of the operations in question, to be a true proposition!