Comment:
Putman says "Of course Voevodsky was NOT saying that he felt that the body of theorems making up the "classic mathematics" that we normally deal with might be inconsistent, that is quite a different matter."
But wasn't he? His conjecture is "I suggest that the corret interpretation of Goedel's second incompleteness theorem is that it provides a step towards the proof of inconsistency of many formal theories and in particular of the "first order arithmetic"."
What I don't understand is this. If classical arithmetic is inconsistent anywhere, then it is inconsistent everywhere (an inconsistency proves everything). So why haven't we found any inconsistencies yet?
What is cool is that the notion of reliability he talked about seems to be a move toward a "local" notion of consistency.
Humm, does this make sense? Let A and B be closed formulas of some formal system. Define the "logical distance" between A and B to be the shortest proof of B assuming A (inculding the data of the number of applications of the rules of inference, etc.) Say that B is "locally consistent" with A if the logical distance between A and B is strictly less than the logical distance between A and not-B. A theory is locally consistent if for every pair (A, B) the logical distance from A to B is not equal to the logical distance from A to not-B. Etc. Etc.
