show/hide this revision's text 2 added 259 characters in body

This is a question which I spent some time thinking about myself when first encountering Goedel's incompleteness theorems. I should add the disclaimer that I am no expert in logic and set theory, but I think I can answer this question sufficiently well to understand statements such as Goedel's incompleteness theorems (at least, sufficiently well to satisfy myself).

One one end of the scale, there are statements such as CH and AOC which are independent of ZF set theory, so it is not at all clear if they are really true and we could argue about such things forever. Even for statements which are true in the sense that it is possible to prove that they hold in all models of ZF, it is still possible that in an alternative theory they could fail. Even things like the intermediate value theorem, which I think we can agree is true, can fail with intuitionistic logic.

On the other end of the scale, there are statements which we should agree are true independently of any model of set theory or foundation of maths. For example, I know that 3+4=7. There are simple rules for addition of integers which we just have to follow to determine that such an identity holds. You might come up with some freaky model of integer addition following different rules where 3+4=6, but that is really a different statement involving a different operation from what is commonly understood by addition. Similarly, I know that there are positive integral solutions to $x^2+y^2=z^2$. To verify that such equations have a solution we just need to iterate through all possible triples $(x,y,z)\in\mathbb{N}^3$ and test whether $x^2+y^2=z^2$, stopping when a solution is reached. In this case we are guaranteed to arrive at some solution, such as (3,4,5), proving that there is indeed a solution to the equation.

More generally, consider any statement which can be interpreted in terms of a deterministic, computable, algorithm. If we simply follow through that algorithm and find that, after some finite number of steps, the algorithm terminates in some state then the truth of that statement should hold regardless of the logic system we are founding our mathematical universe on.

So, there are statements of the following form: "A specified program (P) for some Turing machine and given initial state (S0) will eventually terminate in some specified final state (S1)". If such a statement is true, then we can prove it by simply running the program - step by step until it reaches the final state. Such statements, I would say, must be true in all reasonable foundations of logic & maths. Identities involving addition and multiplication of integers fall into this category, as there are standard rules of addition & multiplication which we can program. So does the existence of solutions to diophantine equations like $x^2+y^2=z^2$. Existence in any one reasonable logic system implies existence in any other.

At the next level, there are statements which are falsifiable by a computable algorithm, which are of the following form: "A specified program (P) for some Turing machine with initial state (S0) will never terminate". For example, "There are no positive integer solutions to $x^3+y^3=z^3$" fall into this category. You can write a program to iterate through all triples (x,y,z) checking whether $x^3+y^3=z^3$. Fermat's last theorem tells us that this will never terminate. We can never prove this by running such a program, as it would take forever. However, the negation of statement such as this is just of the previous form, whose truth I just argued, holds independently of the "reasonable" logic system used (this is basically $\omega$-consistency, used by Goedel). That is, if I can write an algorithm which I can prove is never going to terminate, then I wouldn't believe some alternative logic which claimed that it did. In the same way, if you came up with some alternative logical theory claiming that there there are positive integer solutions to $x^3+y^3=z^3$ (without providing any explicit solutions, of course), then I wouldn't hesitate in saying that the theory is wrong. Statements like $$ \int_{-\infty}^\infty e^{-x^2}\,dx=\sqrt{\pi} $$ are also of this form. Assuming we agree on what integration, $e^{-x^2}$, $\pi$ and $\sqrt{\ }$ mean, then we can write a program which will evaluate both sides of this identity to ever increasing levels of accuracy, and terminates if the two sides disagree to this accuracy. The identity is then equivalent to the statement that this program never terminates.

Going through the proof of Goedels incompleteness theorem generates a statement of the above form. i.e., "Program P with initial state S0 never terminates" with two properties. (1) If the program P terminates it returns a proof that the program never terminates in the logic system. (2) If there exists a proof that P terminates in the logic system, then P never terminates.

So, if P terminated then it would generate a proof that the logic system is inconsistent and, similarly, if the program never terminates then it is not possible to prove this within the given logic system.

In fact, P can be constructed as a program which searches through all possible proof strings in the logic system until it finds a proof of "P never terminates", at which point it terminates. The assumptions required for the logic system are that is "effectively generated", basically meaning that it is possible to write a program checking all possible proofs of a statement.
show/hide this revision's text 1 [made Community Wiki]

This is a question which I spent some time thinking about myself when first encountering Goedel's incompleteness theorems. I should add the disclaimer that I am no expert in logic and set theory, but I think I can answer this question sufficiently well to understand statements such as Goedel's incompleteness theorems (at least, sufficiently well to satisfy myself).

One one end of the scale, there are statements such as CH and AOC which are independent of ZF set theory, so it is not at all clear if they are really true and we could argue about such things forever. Even for statements which are true in the sense that it is possible to prove that they hold in all models of ZF, it is still possible that in an alternative theory they could fail. Even things like the intermediate value theorem, which I think we can agree is true, can fail with intuitionistic logic.

On the other end of the scale, there are statements which we should agree are true independently of any model of set theory or foundation of maths. For example, I know that 3+4=7. There are simple rules for addition of integers which we just have to follow to determine that such an identity holds. You might come up with some freaky model of integer addition following different rules where 3+4=6, but that is really a different statement involving a different operation from what is commonly understood by addition. Similarly, I know that there are positive integral solutions to $x^2+y^2=z^2$. To verify that such equations have a solution we just need to iterate through all possible triples $(x,y,z)\in\mathbb{N}^3$ and test whether $x^2+y^2=z^2$, stopping when a solution is reached. In this case we are guaranteed to arrive at some solution, such as (3,4,5), proving that there is indeed a solution to the equation.

More generally, consider any statement which can be interpreted in terms of a deterministic, computable, algorithm. If we simply follow through that algorithm and find that, after some finite number of steps, the algorithm terminates in some state then the truth of that statement should hold regardless of the logic system we are founding our mathematical universe on.

So, there are statements of the following form: "A specified program (P) for some Turing machine and given initial state (S0) will eventually terminate in some specified final state (S1)". If such a statement is true, then we can prove it by simply running the program - step by step until it reaches the final state. Such statements, I would say, must be true in all reasonable foundations of logic & maths. Identities involving addition and multiplication of integers fall into this category, as there are standard rules of addition & multiplication which we can program. So does the existence of solutions to diophantine equations like $x^2+y^2=z^2$. Existence in any one reasonable logic system implies existence in any other.

At the next level, there are statements which are falsifiable by a computable algorithm, which are of the following form: "A specified program (P) for some Turing machine with initial state (S0) will never terminate". For example, "There are no positive integer solutions to $x^3+y^3=z^3$" fall into this category. You can write a program to iterate through all triples (x,y,z) checking whether $x^3+y^3=z^3$. Fermat's last theorem tells us that this will never terminate. We can never prove this by running such a program, as it would take forever. However, the negation of statement such as this is just of the previous form, whose truth I just argued, holds independently of the "reasonable" logic system used (this is basically $\omega$-consistency, used by Goedel). That is, if I can write an algorithm which I can prove is never going to terminate, then I wouldn't believe some alternative logic which claimed that it did. Statements like $$ \int_{-\infty}^\infty e^{-x^2}\,dx=\sqrt{\pi} $$ are also of this form. Assuming we agree on what integration, $e^{-x^2}$, $\pi$ and $\sqrt{\ }$ mean, then we can write a program which will evaluate both sides of this identity to ever increasing levels of accuracy, and terminates if the two sides disagree to this accuracy. The identity is then equivalent to the statement that this program never terminates.

Going through the proof of Goedels incompleteness theorem generates a statement of the above form. i.e., "Program P with initial state S0 never terminates" with two properties. (1) If the program P terminates it returns a proof that the program never terminates in the logic system. (2) If there exists a proof that P terminates in the logic system, then P never terminates.

So, if P terminated then it would generate a proof that the logic system is inconsistent and, similarly, if the program never terminates then it is not possible to prove this within the given logic system.

In fact, P can be constructed as a program which searches through all possible proof strings in the logic system until it finds a proof of "P never terminates", at which point it terminates. The assumptions required for the logic system are that is "effectively generated", basically meaning that it is possible to write a program checking all possible proofs of a statement.