If you believe that some model of computation can be expressed in arithmetics (this implies expressibility of the notion of correct proof), Godel’s first theorem is more or less analyzis of “This statement cannot be proved”. If it can be proved, it is false and there is a provable false statement; if it cannot be proved it is an unprovable true statement.
But most of the effort in proving Godel’s theorem has to be spent on proving that you cannot go half way: if you have a big enogh theory to express basic arithmetical facts, you have to have full reflection. It can be stated in various ways, but it requires a technically accurate proof—I am not sure how well it would fit into a cartoon.
Could you state explicitly what do you want to find—just the non-tehnical part, or both?
Does any one know of a good guide to Godel’s theorems along the lines of the cartoon guide to lob’s theorem?
If you believe that some model of computation can be expressed in arithmetics (this implies expressibility of the notion of correct proof), Godel’s first theorem is more or less analyzis of “This statement cannot be proved”. If it can be proved, it is false and there is a provable false statement; if it cannot be proved it is an unprovable true statement.
But most of the effort in proving Godel’s theorem has to be spent on proving that you cannot go half way: if you have a big enogh theory to express basic arithmetical facts, you have to have full reflection. It can be stated in various ways, but it requires a technically accurate proof—I am not sure how well it would fit into a cartoon.
Could you state explicitly what do you want to find—just the non-tehnical part, or both?
Actually that was pretty much enough.