The following explanation was given to a math colleague concerning nonstandard models:
if Con(PA) fails in a non-standard model, it means it contains a
“proof of non-standard length” of a contradiction from PA. With a
little work, one can externalise that to some non-well-founded “proof
tree”, which has at each node a possibly-non-standard formula (which
in turn externalises to some not-necessarily-well-founded syntax
tree), where each step will genuinely follow from earlier steps by
some standard rule of proof, but the whole tree will be
non-well-founded, and hence not an actual proof.
Said colleague had the following question regarding this explanation:
I find this non-well-founded approach an enlightening way of viewing incompleteness. I checked in a book by Peter Smith on Goedel’s theorems, but it does not seem to discuss this particular aspect (possibly he views it as equivalent to discussion around -completeness). Do you know of any book that would place non-well-foundedness center-stage?