Certainly everybody believes that Godel's theorems are true. But I wonder if its' Achilles heel is the notion of "stepping outside" of the formal system.
Can we formalize what "stepping outside" means? How can we be sure we have done it correctly? When we step "outside" and do reasoning, are we doing it following the formal logic? Which logic? Are there rules as to what kind of inferences are NOT allowed when reasoning "outside of the system"?
In other words when we "reason outside of the formal system" we are using English. Can we trust the logic of English is "correct"?
Can a formal system really do self-reference? It's just strings. WE can give an interpretation to formal sentences but when we interpret a given sentence as referring to "itself" doesn't it really refers to the interpretation, not to "itself" but its interpretation?
When natural language refers to the formal system doesn't it really just refer to what the formal system "means" in the natural language, not to the formal system itself as such?
We can absolutely reason formally from outside a formal system, by embedding it in a larger one, and this is a very standard and normal technique that anyone working seriously in this area does all the time. E.g. you work in ZFC + some large cardinal assumption that allows you to construct a model of ZFC inside that system, and then reason formally about ZFC there.
> WE can give an interpretation to formal sentences but when we interpret a given sentence as referring to "itself" doesn't it really refers to the interpretation, not to "itself" but its interpretation?
Indeed it can't - see e.g. Löb's theorem. A formal system can manipulate a set of rules that might happen to be its own rules, but it can never "know" that those are in fact its own rules. Which makes sense when you think about it.
Yes, very interesting point. It can not know that they are its own rules. BUT we can know that. Therefore we the meta-level can reason about the subject more than it can of itself. For example the subject-system can not mechanically prove that it is looking at its own ruleset.
So the term "unprovable" should probably best be always qualified with: in which system.
There are facts about systems which the system itself can not prove. Statements like that can be expressed in some formalized subset of English and proven following the rules of that formalized English. What is that "formalized English" that we use in our reasoning? Or does it not matter?
> There are facts about systems which the system itself can not prove. Statements like that can be expressed in some formalized subset of English and proven following the rules of that formalized English. What is that "formalized English" that we use in our reasoning? Or does it not matter?
Again, the normal, routine thing is to just use a slightly larger formal system to work with them. But it really doesn't matter.
Can we formalize what "stepping outside" means? How can we be sure we have done it correctly? When we step "outside" and do reasoning, are we doing it following the formal logic? Which logic? Are there rules as to what kind of inferences are NOT allowed when reasoning "outside of the system"?
In other words when we "reason outside of the formal system" we are using English. Can we trust the logic of English is "correct"?
Can a formal system really do self-reference? It's just strings. WE can give an interpretation to formal sentences but when we interpret a given sentence as referring to "itself" doesn't it really refers to the interpretation, not to "itself" but its interpretation?
When natural language refers to the formal system doesn't it really just refer to what the formal system "means" in the natural language, not to the formal system itself as such?