Yes, that's how I remember it being explained. But what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange, but if non-standard numbers aren't infinite, how can the proof be infinite?
> what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange
Yes.
> if non-standard numbers aren't infinite, how can the proof be infinite?
I am not an expert on this, but as I understand it, it has to do with how Godel numbering would have to work if non-standard numbers can be Godel numbers. Basically, only a standard natural number can be the Godel number of a finite proof; any proof that has a non-standard number as its Godel number must be infinite (i.e., it must have an infinite number of steps). But unfortunately I cannot explain why that is true. Maybe another poster here can, or can correct me if my understanding is wrong.
My usual interpretation of this is not that we have strange proofs, but rather to interpret this as a failure of Godel encodings to completely capture the notion of proof.
That is the statement Con(T) isn't really a statement about the consistency of T, but rather a statement that is "close enough" to suffice for many, but not all purposes.
