Skip to main content
Yes, I mean prove-ably,phone!
Source Link
Ron Maimon
  • 921
  • 13
  • 23

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is similar to ROSSER (The statement DEE halts is probablyprovably NOT the negation of "DUM halts", that's the whole point)

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is similar to ROSSER (The statement DEE halts is probably NOT the negation of "DUM halts")

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is similar to ROSSER (The statement DEE halts is provably NOT the negation of "DUM halts", that's the whole point)

Not at all! Ah community wiki.
Source Link
Ron Maimon
  • 921
  • 13
  • 23

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is essentially equivalentsimilar to ROSSER. The (The statement DEE halts is probably NOT the provable negation of "DUM halts", and the programs are saying that S proves "DEE halts" before "DUM halts")

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is essentially equivalent to ROSSER. The statement DEE halts is the provable negation of "DUM halts", and the programs are saying that S proves "DEE halts" before "DUM halts"

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is similar to ROSSER (The statement DEE halts is probably NOT the negation of "DUM halts")

added sections to make the answer more readable
Source Link
Kaveh
  • 5.5k
  • 2
  • 37
  • 52
 

TYPE###TYPE I---: self referential pi-0-1 statements (statements about the non-halting of a certain computer program)

 

TYPE###TYPE II ---: these prove that there exist total functions which are not provably total. The statements in this case are pi-0-2, statements about the totality of some computable function.

 

TYPE###TYPE III ---: nonconstructive theorem about a large class of statements, which do not provide an explicit unprovable statement, and so cannot be used to step up the heirarchy of systems.

 

TYPE I--- self referential pi-0-1 statements (statements about the non-halting of a certain computer program)

TYPE II --- these prove that there exist total functions which are not provably total. The statements in this case are pi-0-2, statements about the totality of some computable function.

TYPE III --- nonconstructive theorem about a large class of statements, which do not provide an explicit unprovable statement, and so cannot be used to step up the heirarchy of systems.

 

###TYPE I: self referential pi-0-1 statements (statements about the non-halting of a certain computer program)

 

###TYPE II: these prove that there exist total functions which are not provably total. The statements in this case are pi-0-2, statements about the totality of some computable function.

 

###TYPE III: nonconstructive theorem about a large class of statements, which do not provide an explicit unprovable statement, and so cannot be used to step up the heirarchy of systems.

 
Post Made Community Wiki
Source Link
Ron Maimon
  • 921
  • 13
  • 23
Loading