[1] https://www.amazon.ca/Undecidable-Propositions-Principia-Mat...
From my understanding, C&L diverges from Godel's original proof technique in order to make it easier to follow, but it's much more rigorous and explicit than what you'd find in Godel, Escher, Bach or something. It's still a textbook.
[1]: https://www.amazon.com/Computability-Logic-George-S-Boolos/d...
Regarding [1], "circularity" in an uncountably infinite context seems different than "self-referential", though the latter is usually geometrically analogized as the former. I tentatively consider Yablo's Paradox to demonstrate that an ineradicable cycle of alternating truth-assignments is equivalent to an infinite (>= aleph-one) regression of alternating truth-assignments, and thus that circularity does not map coherently to self-reference in all logic systems.
[0] http://www.mit.edu/~yablo/pwsr.pdf
[1] http://ferenc.andrasek.hu/papersybprx/jcbeal_is_yablo_non_ci...
Imagine an infinite sequence of sentences S1, S2, S3, ...,
(S1) for all k >1, Sk is untrue
(S2) for all k >2, Sk is untrue
(S3) for all k >3, Sk is untrue
...
This Yablo's paradox seem self referential to me. The statements are making claims about a series of statements of which they themselves are part of. I see the statements only making claims about subsequent statements... but still.
How about, rather that banning "self references", you have a more carefull phrasing requiring all structures to be fully and independently defined before you start asking questions (or making claims) about them? (No side effects from the question please). Does this avoid all Goedelish paradoxes?
In 1952 the logician Martin Löb invented something called "provability logic" as a way to formulate Gödel's theorem more abstractly, so that we could see how the proof worked without having to work with explicit numerical encodings of formulas. (Think of this as the difference between working with strings versus abstract syntax trees.)
His version of the proof is now called Löb's theorem, and its structure is almost identical to what logicians call Curry's paradox, and which (via the Curry-Howard correspondence) programmers know as the Y combinator. The Y combinator is used to implement recursion in the lambda calculus, specifically including the ability to go into infinite loops.
I blogged about this last year:
http://semantic-domain.blogspot.co.uk/2016/05/lobs-theorem-i...
A | B | A -> B
0 | 0 | 1
0 | 1 | 1
1 | 0 | 0
1 | 1 | 1
I fail to see why all except for 1 -> 0 = 0 aren't undefined. I understand reasoning behind why this was done, but mixing unrelated predicates seems like a generally bad idea, even if it allows mechanical proofs.
Aren't there already "complete" systems like relevance logic? Now with computers we can perhaps make proofs we need "relevant" instead of being based on fundamentally incomplete though "simpler" logic?
Also, if I understand you correctly you're trying to 'fix' incompleteness by making A -> B undecidable, which seems like it would achieve the opposite.
1 -> 0 = 0