[TelmoMenezes]

Sure, and abductive reasoning can be formalized in certain modal logics with Kripke semantics.

What Gödel tells us is that, as long as you have a sufficiently powerful formal system, you cannot prove the consistency of the system itself. Modal logics are no exception.

If you are a computationalist (that is to say, you believe that the human mind can be emulated by a Turing machine), then you might want to take a look at Gödel, Escher, Bach, where Hofstadter discusses how the second incompleteness theorem applies to Turing machines.

You might also enjoy "Forever Undecided" by Smullyan. It uses puzzles to guide you to an intuition about what the incompleteness theorems means to human knowledge and its limitations. In the worst case it's a fun read.

Peace!

[eli_gottlieb]

> Sure, and abductive reasoning can be formalized in certain modal logics with Kripke semantics.

No, it can't. Abductive reasoning is probabilistic modelling, and notably, there's a line of research by Cristian Calude showing that you can soundly, non-paradoxically place probabilities on Halting questions.

(Computational tractability is still an obstacle with his current approach, but it has been shown not to generate paradoxes, which is already a major step forward.)

>you might want to take a look at Gödel, Escher, Bach, where Hofstadter discusses how the second incompleteness theorem applies to Turing machines.

This is backwards: halting problems and Kolmogorov complexity for Turing machines give us the two Incompleteness Theorems for proof systems, via Chaitin's Incompleteness Theorem.

Which also neatly gives a way around the Second Incompleteness Theorem: a hierarchical-probabilistic reasoner can create an abstract, compressed model of themselves which consists of small-enough amounts of information that they can reason about its behavior without becoming subject to Chaitin Incompleteness.