Programming and ZFC

1.7k Views Asked by At

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)?

2

There are 2 best solutions below

4
On 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. :)

1
On

Let's look at this from a far more mathematical point of view.

An algorithm is like a theory $T$ in some first-order logic. And you can ask if the theory proves $\varphi$. And this can be checked syntactically or in other ways. And that's fine.

An implementation is like a model of $T$. So now instead of asking if $T$ proves $\varphi$ you are asking if $\varphi$ is true in the model $M$. This turns out to be equivalent to asking if the theory of $M$ proves $\varphi$, and that's important. Because it means we can jump between the two questions about truth and provability.

If your implementation (including compiler and processor and whatnot) is faithful and does not deviate from the algorithm (and this means that you have to ignore, completely, all physical constraints or push them into the algorithm somehow), then the fact that you proved that the algorithm works means that your implementation works.

If your implementation is not faithful then you are asking if the algorithm which was faithfully implemented is equivalent to the algorithm that you wanted to implement. That's a whole other question, and it depends also on your ability to extract the "true algorithm" from your implementation.