There are two popular views about how these kinds of paradox might be managed. The first is committed to an ensemble of equally concrete but different versions of the physical world. Travelers into the past arrive in worlds that are distinct from those that they left. They are free to kill their grandfather secure in the knowledge that their grandfather is not really their grandfather, but something like his counterpart. David Deutsch and Michael Lockwood think that restrictions posed by classical systems on the actions of time travelers imply that time travel must must displace travelers into different worlds.14 It is by no means clear that time travelers under such a scheme are really following a closed timelike curve. Closed timelike curves are paths that return to, or very close to, their own spatiotemporal starting points.15
On quite another view, time travel really does return an agent to his very own past. A temporal rerun is possible only if everything he does in the past is already in place in his history. This means everything. Consistency might be maintained through the most ordinary of physical processes: the gun misfires, or the bullet dribbles out inconclusively, or at the very last moment your grandfather ducks to tie his shoelaces. Your efforts can make the past what it was but they cannot make the past different from what it was.
There is a third, which is that you would arrive in the past only to find that you had no agency at all, no free will. In this formulation you would never attempt to kill your grandfather, and no faulty guns or lucky grandparents are needed. If the present is a hypersurface sweeping through spacetime, leaving the past in its wake, and the past is a set structure... you’re an automaton if you travel to the past. Presumably in this kind of natural order, the future doesn’t exist except as a word and concept. There is the fixed past, and the hypersurface of the present.
Or the future and past are both fixed, and the hypersurface of the present is some strange artifact we perceive. Or... who knows?
Or perhaps it's only the illusion of agency that is gone.
And that makes it a different present for each and everyone/everything.
I’ve never thought about it in quite that way before, but yes I suppose so. Each hypothetical observer is going to experience different slices of “present” in something like Block Universe conjecture.
The main ingredient we need here is to realize that numbers can represent sentences in formal systems. This should be obvious to computer scientists of today, but it was ground-breaking at the time.
Another thing we'll need is diagonalization. Some folks get hung up on this one; ultimately, you'll have to convince yourself that it's a valid technique.
Hofstadter's explanations, both the long gentle one in GEB and the quick fuzzy one in "I Am A Strange Loop", are much more detailed and correct on this, so I'd advise going back and making sure you understand each step.
Also, something that doesn't get enough airtime is Tarski's Undefinability, which says that a formal system afflicted by incompleteness is not capable of talking about truth in certain basic and important ways which would enable a formal system to fully represent itself.
Cynics might take this to mean that maths is meaningless. On the contrary, I'd like to suggest that maths is the canonical emergent pattern; any formal system with sufficient complexity to represent itself will automatically exhibit some algebraic structure, and maths emerges naturally from there.
The biggest implication for computer scientists is that, combined with results of Church and Tarski, we should expect that meta-languages are more powerful than object-languages, whether this is by preprocessing and macros like in C/C++ and CL, or by avoiding using meta-features except when necessary like in Python and Ruby.
At least, that’s my understanding of it.
For any sufficiently powerful system (Turing completeness is definitely powerful enough) there are statements which are true but cannot be proven by that system. Secondarily, no system can demonstrate its own consistency.
However, if you limit your software enough, you can prove that every possible input is handled correctly. That involves removing Turing completeness. E.g. once you accept a language as a configurator, you can no longer prove that. CSS3 is Turing complete. JSON is not.
One requirement is limiting the size of inputs.