[Home]History of Halting Problem/Talk

HomePage | Recent Changes | Preferences

Revision 24 . . October 1, 2001 6:35 am by Anatoly Vorobey [more about Goedel's proof; some of this stuff may eventually be incorporated into the page on Goedel's thms?]
Revision 23 . . October 1, 2001 5:34 am by AxelBoldt
  

Difference (from prior major revision) (no other diffs)

Changed: 77c77,79
::"extend a very weak theory of arithmetic": does that not mean that the provable arithmetical statements of the weak theory (which are presumably true) are also provable in Q? In other words: Q has to be a little bit sound? --AxelBoldt
::"extend a very weak theory of arithmetic": does that not mean that the provable arithmetical statements of the weak theory (which are presumably true) are also provable in Q? In other words: Q has to be a little bit sound? --AxelBoldt

:::nope, that's why in general case we allow "interpreting", not necessarily extending. This means that we may map the axioms of the weak theory to different sentences, which aren't necessarily true at all, in such a way as to preserve proof-theoretic strength. Essentially what we are after is the power of representation that the weak theory has: e.g. given a recursive function f(x), we want there to be phi(x,y) s.t. the theory proves phi(x,y) whenever f(x)=y and proves not(phi(x,y)) whenever f(x)!=y. Now in the original weak theory this phi(y) will just embody whatever way of building the recursive function up from basic building blocks that we choose (e.g. it may embody a Turing machine or a process of defining the function from basic recursive functions, iterations, etc.), so phi(x,y) will actually be true whenever f(x)=y. But we don't really care about that in Goedel's proof, we just need the theory to be strong enough to prove/disprove phi(x,y) according to whether f(x)=y. So the Goedel's theorem will apply to very convoluted and extremely not-sound theories Q as long as there's a way to faithfully map the "real" sound phi(x,y) proved/disproved by the weak theory into some phi'(x,y) proved disproved by Q, without any regard to its truth in N. --AV

HomePage | Recent Changes | Preferences
Search: