5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Although this slightly deviates from your question, Hoare logic might be of interest to you. $\endgroup$ – Stefan Mesken Dec 16 '15 at 9:16
  • $\begingroup$ @Stefan Thanks, I have indeed read about that. It assumes much less than ZFC and seems to be able to formally verify programs. Unfortunately most algorithms are proven in ZFC and not Hoare logic, which makes me wonder if it is possible that they are actually incorrect. $\endgroup$ – Wakaka Dec 16 '15 at 9:47
  • $\begingroup$ It takes a while to prove $2+2=4$ using ZFC, but the proof makes me very confident that it is a fact $\endgroup$ – Hagen von Eitzen Dec 16 '15 at 13:05
  • $\begingroup$ I do not understand at all your new final sentence "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)?" Can you clarify? For example, by Godel's Incompleteness Theorem there will always be a program which can't be verified to never halt, in a given theory, so doesn't that kill this? $\endgroup$ – Noah Schweber Dec 16 '15 at 22:58
  • $\begingroup$ Also, why do you think Hoare logic is sufficient? Can you clarify what properties you are verifying, and for what types of programs? $\endgroup$ – Noah Schweber Dec 16 '15 at 22:59
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ So does this mean that we can never really know for sure that a program will exhibit a simple behavior (e.g. output 1) based on a proof in ZFC? This is since we do not know for sure that it is consistent or arithmetically sound. On the other hand, isn't it possible to formally verify programs? Does this mean that formal verification cannot possibly be done in ZFC? $\endgroup$ – Wakaka Dec 16 '15 at 9:43
  • 2
    $\begingroup$ @Wakaka: if we have a proof in ZFC, that is very good evidence about what will happen. There are many meanings of "certain". In a particular sense, we can never be "certain" of anything, so if that is the sense you mean then, well, we can't be "certain" of anything! But normally we would say that if we have a proof of something in ZFC then we are certain that the something is correct. $\endgroup$ – Carl Mummert Dec 16 '15 at 12:59
  • $\begingroup$ @CarlMummert Has there ever been instances where ZFC proves something about an algorithm and it turns out to be untrue when the algorithm is actually run? (Assuming the mechanical procedure of following the rules of the programming language) $\endgroup$ – Wakaka Dec 16 '15 at 22:06
  • 1
    $\begingroup$ @Wakaka No, there has not. In order for "it turns out to be untrue when the algorithm is actually run" to make sense, the "it" here has to be a universal (or $\Pi^0_1$) sentence: of the form, "such-and-such simple behavior never happens." If ZFC disproves a true sentence of this form, then ZFC is inconsistent, as I pointed out above. Currently, ZFC is not known to be inconsistent. $\endgroup$ – Noah Schweber Dec 16 '15 at 22:57
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks! What I'm asking is if we try to prove the algorithm in the first-order theory of ZFC. Suppose ZFC does prove it (that it outputs correctly according to each input). Then assuming the implementation is faithful, can we be certain that the algorithm will work based only on the axioms of the programming language (and not the full axioms of ZFC)? $\endgroup$ – Wakaka Dec 16 '15 at 11:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.