Suppose I have a simple program that implements an algorithm (say depth-first search), written in a simple imperative programming language with the standard for loops, recursions, conditional statements and so on. It takes in a well-specified input and has a well-specified output.
Suppose I want to verify that it always produces the correct output for each input. I can treat the program as a mathematical object subject to certain rules of the programming language. I write a formal mathematical proof, assuming the usual axioms of ZFC and first-order logic, to show that this is true.
How would I know that my program definitely works (i.e. for all inputs, output correctly) due to this proof? I do know that in the ZFC axiom system, my program works because it is defined to work (it is deducible formally). However, it seems that the correctness of my program does not require the full machinery of ZFC; its only axioms are the rules of the programming language. Commonly used proof techniques like mathematical induction are founded on axioms in ZFC, but we do not yet know that these hold due only to the rules of the programming language.
Is it possible that my program does not actually work, but it is proven to work in ZFC? If that's the case, why are all algorithms proven in the usual framework of ZFC (assuming all axioms of set theory, and first-order logic)?
EDIT: Can formal verification of programs (with 100% certainty according to specifications of the programming language) be done in ZFC? I am assuming it can be done under weaker axiom systems (e.g. Hoare logic)?
Best Answer
It depends what you mean by "work."
If you just want to show that a program never exhibits some simple behavior - e.g., if you want to show it doesn't halt - then if ZFC proves this fact, it's correct, as long as ZFC is consistent.
If you want to show that a program will at some point exhibit some simple behavior - e.g., if you want to show it will halt - then knowing the correctness of a ZFC-proof requires a bit more than just the assumption that ZFC is consistent - we need to know that it is $\Sigma^0_1$-sound. This is a technical hypothesis much weaker than the assumption "Every arithmetical consequence of ZFC is true" (which we usually assume).
And, of course, Gödel's theorem shows that ZFC won't always be enough, even for the simplest statements - there is a Turing machine $T$ which never halts (assuming ZFC is consistent) but which ZFC can't prove never halts (again, assuming ZFC is consistent).
But these are general problems you'll have with any background theory, not just ZFC. Every result of this type - actually, every result at all - exists in the context of background assumptions. ZFC happens to occupy that sweet spot of (a) being extremely common to assume, (b) reasonably well-understood, and (c) powerful enough to handle almost all "reasonable" problems. (One can try to make stronger arguments for ZFC as opposed to other theories, but that's a problem for another time.) So the answer to why we use ZFC: well, we gotta use something. :)