1
$\begingroup$

Lot of mathematicians have made several efforts to answer the question : are mathematics consistent ? Although we haven't yet had a proof of consistency, and surely we will never (Gödel second theorem), does this question has an impact on computer science ? I mean, does the work of those mathematicians, like Gödel's theorems or formal deduction systems, shows new answers or new problems in computer science ? What would happen in computer science if, for example, we found a paradox in set theory ?

$\endgroup$
  • 1
    $\begingroup$ It may be worth noting that computer science largely evolved out of work in formal logic, often related to these questions. For example, Turing's work but also Church's and Kleene's. $\endgroup$ – Derek Elkins Nov 24 '17 at 4:12
  • 1
    $\begingroup$ In CS say almost every problem reduces to "does this program terminate or not", which is a $\Pi_0$ sentence in arithmetic. If your theory of arithmetic is inconsistent, your theorems go wrong, and after that you can only run a program until it terminates, you can't prove (non)-termination in any other way. $\endgroup$ – reuns Nov 24 '17 at 7:11
  • $\begingroup$ @reuns Can't we prove (non)-termination if arithmetic were inconsistent because of Π0 sentences, or because inconsistency of arithmetic would lead to inconsistency of stronger theories, like ZFC ? $\endgroup$ – user80502 Nov 24 '17 at 10:38
  • 1
    $\begingroup$ To prove a program terminates or not : you can run it until it terminates, or use an axiomatic theory of arithmetic to find a proof it terminates (or a proof that it doesn't terminate). If your axiomatic theory of arithmetic is inconsistent, and you try anyway using it to prove theorems, things will go wrong (you will be able to prove a given program which does terminate, doesn't terminate) $\endgroup$ – reuns Nov 24 '17 at 11:19
4
$\begingroup$

Absolutely nothing will happen. Computers will still work, experts in machine learning will continue perfecting their tools, and even theoretical computer scientists will go on happily proving their theorems. Most mathematicians will also not feel much difference.

While we are trained to think that we are carrying out our proofs in ZFC, in practice proofs in mathematics and computer science are almost always carried out in English. Even if a contradiction is discovered in set theory, it is extremely likely that the axioms can be amended in such a way that the contradiction disappears and no proofs are affected apart from those in very specialized fields of a foundational nature.

More controversially, one can argue that most mathematicians argue in a nebulous system which actually does not rely on ZFC at all. Indeed, the average mathematician and nearly all computer scientists have little recourse to ZFC during their research life. Making this claim less nebulous, one can (and people do) argue that virtually all proofs in non-foundational fields can be carried out in weak subsystems of ZFC that are in less danger of being shown to be inconsistent. A nice reading in this general direction is McLarty's What does it take to prove Fermat's last theorem.

$\endgroup$
  • 1
    $\begingroup$ +1 Reverse mathematics is a field that directly addresses finding what assumptions are needed (from one perspective) for representative theorems/areas of mathematics. And, of course, constructivists (even those with no philosophical qualms with classical logic) often work in much weaker logics (though still quite powerful in their own way). (Internal languages of) pretoposes provide another perspective on sliding scales of foundational power. $\endgroup$ – Derek Elkins Nov 24 '17 at 13:38
  • 1
    $\begingroup$ I will say though that "absolutely nothing" is a touch strong. A contradiction found in ZFC is likely to at least cause concern for type theorists which is intimately related to much of programming language theory. PLT is at least close to a "field of a foundational nature". Design of type systems is already colored by the contradictions found in naive set theory. $\endgroup$ – Derek Elkins Nov 24 '17 at 13:45
2
$\begingroup$

This would have a huge impact on computer science. All of CS is either a branch of mathematics, or built on the foundations of mathematics.

Every algorithm correctness proof or complexity bound is proven using mathematics. An inconsistency would shake the field to its core.

Moreover, through the Curry-Howard correspondence, proofs are isomorphic to well-typed programs, so a ton of type theory would go out the window.

That said, there is hope. There are multiple foundations of mathematics: ZF set theory, ZFC set theory, Martin-Lof Type Theory, Homotopy Type Theory, etc. Much of Computer Science has been done in all of these theories (particularly in PL theory), so if one is proven inconsistent, it may not mean that all is lost.

$\endgroup$
  • 1
    $\begingroup$ While it would certainly be a big deal, I'm pretty sure this would have little impact on the majority of math, let alone CS. It's empirically clear that a lot of computational aspects of math (again, let alone CS) "work". This alone would already be a basis on which to found a non-trivial chunk of math and CS, particularly the practical aspects. It's not like the contradictions found in naive set theory led us to discard all, or really any, preceding math. Even the things that were demonstrably inconsistent, such as "infinitesimals", were later rehabilitated. $\endgroup$ – Derek Elkins Nov 24 '17 at 7:19
  • $\begingroup$ Any realistic contradiction found is likely to be found in some esoteric aspect that affects few mathematicians. Ironically, PLT is likely to be one of the more impacted areas of CS. $\endgroup$ – Derek Elkins Nov 24 '17 at 7:19
  • $\begingroup$ @DerekElkins Aren't maths aspects so tied that even an esoteric contradiction would lead to the destruction of everything ? $\endgroup$ – user80502 Nov 24 '17 at 10:43
  • 1
    $\begingroup$ @dylan61 I think you're referring to the principle of explosion. Yes, in most logical systems if you have a contradiction, then you can prove anything. (Systems where this doesn't happen are called paraconsistent logics.) However, if a contradiction was found in, say, ZFC, mathematicians would simply switch to a different system omitting the aspects that caused the contradiction just like they did in the move from naive set theory to ZFC. As jmite pointed out, there are already several other possibilities that can recover much of math in practice, and often are the systems used in CS. $\endgroup$ – Derek Elkins Nov 24 '17 at 11:14
  • 1
    $\begingroup$ @dylan61 They would technically need to reprove the theorems, but as many of the theorems aren't even close to formal in the first place, as long as the new system is roughly similar to the old one, at least for the parts used for a particular theorem, they likely wouldn't do anything. It would just be assumed that the theorems would transfer over to the new system. There will be some results in "day-to-day" math that would skirt near the source of the contradiction which would need to be more closely reconsidered. $\endgroup$ – Derek Elkins Nov 24 '17 at 13:29
1
$\begingroup$

Let's assume that maths is inconsistent, and there is a proof that 1 = 0. Using that proof, you can prove that the runtime of any algorithm is zero.

That proof, however, doesn't change the runtime of the algorithm. So we would be in a slightly problematic situation: That we cannot use or trust proofs that are so complex that they can take advantage of this inconsistency. I think it is only very slightly problematic.

$\endgroup$
  • $\begingroup$ It doesn't change the runtime of the algorithm on known inputs. The problem is, there's know way to experimentally know the runtime on every input. So we use logic and proofs to find general formulas. But if the logic is shaky, how can we trust the formula? $\endgroup$ – jmite Feb 13 '18 at 17:30

Your Answer

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