notes/170306/index.html

<!DOCTYPE html>
<!-- Akai (pandoc HTML5 template)
     designer:     soimort
     last updated: 2016-05-06
     last adapted: 2016-11-01 -->
<html>
  <head>
    <meta charset="utf-8">
    <meta name="generator" content="pandoc">
    <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
    <meta name="author" content="Mort Yao">
    <meta name="dcterms.date" content="2017-03-06">
    <title>An Intuitive Exposition of Proof by Contradiction vs. Proof of Negation</title>
    <link rel="canonical" href="https://www.soimort.org/notes/170306">
    <style type="text/css">code { white-space: pre; }</style>
    <link rel="stylesheet" href="//cdn.soimort.org/normalize/5.0.0/normalize.min.css">
    <link rel="stylesheet" href="//cdn.soimort.org/fonts/latest/URW-Palladio-L.css">
    <link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/font-awesome/4.7.0/css/font-awesome.min.css">
    <link rel="stylesheet" href="/__/css/style.css">
    <link rel="stylesheet" href="/__/css/pygments.css">
    <script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS_CHTML-full" type="text/javascript"></script>
    <!--[if lt IE 9]>
      <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
    <![endif]-->
    <script src="//cdn.soimort.org/jk/latest/jk.min.js"></script>
    <script src="/__/js/main.js"></script>
    <link rel="icon" href="/favicon.png">
    <link rel="apple-touch-icon" href="/favicon.png">
    <link rel="alternate" type="application/atom+xml" href="/feed.atom">
  </head>
  <body>
    <article>
      <header>
        <h1 class="title"><a href="https://www.soimort.org/notes/170306">An Intuitive Exposition of<br />
“Proof by Contradiction vs. Proof of Negation”</a></h1>
        <address class="author">Mort Yao</address>
        <h3 class="date">2017-03-06</h3>
      </header>
      <div id="content">
<p style="text-align:center !important;text-indent:0 !important">(Inspired by <a href="https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/"><em>A “proof by contradiction” is not a proof that ends with a contradiction</em></a> by Robert Harper.)</p>
<p>There seem to be some common misconceptions about “proof by contradiction”. Recently I came across Robert’s <a href="https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/">blog post</a> on this issue, and couldn’t help reviewing it in my own way. I prefer a more formal treatment, nevertheless, without sacrificing its intuitive comprehensibility.</p>
<p>What is a “proof by contradiction”, exactly? When a classical mathematician (probably you) talks about proving by contradiction, they can mean either one of these two (syntactically) different things:</p>
<ol type="1">
<li>Prove <span class="math inline">\(P\)</span>: Assume <span class="math inline">\(\lnot P\)</span>, we derive a contradiction (<span class="math inline">\(\bot\)</span>). Therefore, we have <span class="math inline">\(P\)</span>.</li>
<li>Prove <span class="math inline">\(\lnot P\)</span>: Assume <span class="math inline">\(P\)</span>, we derive a contradiction (<span class="math inline">\(\bot\)</span>). Therefore, we have <span class="math inline">\(\lnot P\)</span>.</li>
</ol>
<p>Both syntactic forms have some kind of <em>reductio ad absurdum</em> (reduction to / derivation of contradiction) argument. However, the first form provides an <em>indirect proof</em> for <span class="math inline">\(P\)</span>; this is what we call a genuine “proof by contradiction”. The second form provides a <em>direct proof</em> for <span class="math inline">\(\lnot P\)</span> which is just the negation of <span class="math inline">\(P\)</span>; this is preferably called a “proof of negation”, as it’s not a proof of <span class="math inline">\(P\)</span> itself, but rather a proof of the negation of <span class="math inline">\(P\)</span>.</p>
<p>But how are they any different? You may ask. In a classical setting, there is no semantic difference. Notice that in the first form (“proof by contradiction”), we could rewrite <span class="math inline">\(P\)</span> as <span class="math inline">\(\lnot Q\)</span>, then we get</p>
<ol start="3" type="1">
<li>Prove <span class="math inline">\(\lnot Q\)</span>: Assume <span class="math inline">\(Q\)</span>, we derive a contradiction (<span class="math inline">\(\bot\)</span>). Therefore, we have <span class="math inline">\(\lnot Q\)</span>.</li>
</ol>
<p>which is just the second form, i.e., a “proof of negation”. Likewise, if we rewrite <span class="math inline">\(P\)</span> as <span class="math inline">\(\lnot Q\)</span> in the second form, we get</p>
<ol start="4" type="1">
<li>Prove <span class="math inline">\(Q\)</span>: Assume <span class="math inline">\(\lnot Q\)</span>, we derive a contradiction (<span class="math inline">\(\bot\)</span>). Therefore, we have <span class="math inline">\(Q\)</span>.</li>
</ol>
<p>which is just the first form, i.e., a “proof by contradiction”. That’s the very reason people often misconceive them – classically, a proof by contradiction and a proof of negation can be simply converted to the form of one another, without losing their semantic validity.</p>
<p>From a constructivist perspective, things are quite different. In the above rewritten forms, we introduced a new term <span class="math inline">\(\lnot Q := P\)</span>. For the rewrite in the 3rd form to be valid, the new assumption <span class="math inline">\(Q\)</span> must be as strong as the original assumption <span class="math inline">\(\lnot P\)</span>, which is just <span class="math inline">\(\lnot \lnot Q\)</span>. Formally, there must be <span class="math inline">\(\lnot \lnot Q \implies Q\)</span>. For the rewrite in the 4th form to be valid, the new statement <span class="math inline">\(Q\)</span> must be not any stronger than the original statement <span class="math inline">\(\lnot P\)</span>, so formally there must also be <span class="math inline">\(Q \implies \lnot \lnot Q\)</span>. In intuitionistic logic, although we can derive a “double negation introduction” (thus complete the rewrite in the 4th form), there is no way to derive a “double negation elimination” as required to get the 3rd form. So technically, while we can soundly rewrite from a “proof of negation” to a “proof by contradiction”, the other direction is impossible. Indeed, we must make a clear distinction between a “proof by contradiction” and a “proof of negation” here: Semantically, they are not even dual and should not be fused with each other.</p>
<p>Why is this distinction important? Because in intuitionistic logic, the second form (proof of negation) is a valid proof; the first form (proof by contradiction) is not. Take a look at the negation introduction rule: <span class="math display">\[\lnot_\mathsf{I} : \frac{\Gamma, P \vdash \bot}{\Gamma \vdash \lnot P}\]</span> which justifies the validity of “proof of negation”. However, there is no such rule saying that <span class="math display">\[\mathsf{PBC} : \frac{\Gamma, \lnot P \vdash \bot}{\Gamma \vdash P}\]</span> In classical logic, where a rule like <span class="math inline">\(\mathsf{PBC}\)</span> is allowed, one can easily derive the double negation elimination which we begged for before: Given <span class="math inline">\(\Gamma \vdash \lnot \lnot P\)</span>, the only rule that ever introduces a negation is <span class="math inline">\(\lnot_\mathsf{I}\)</span>, so we must also have <span class="math inline">\(\Gamma, \lnot P \vdash \bot\)</span>. Then by <span class="math inline">\(\mathsf{PBC}\)</span>, we get a derivation of <span class="math inline">\(\Gamma \vdash P\)</span>, as desired. <span class="math display">\[\mathsf{DNE} : \frac{\Gamma \vdash \lnot \lnot P}{\Gamma \vdash P}\]</span> If we adopt <span class="math inline">\(\mathsf{PBC}\)</span>, then we will also have adopted <span class="math inline">\(\mathsf{DNE}\)</span>; if we have <span class="math inline">\(\mathsf{DNE}\)</span>, then it would be perfectly valid to rewrite a “proof by contradiction” into the form of a “proof of negation”, or the other way around, as is already shown before. Since constructivists do not want to accept rules like <span class="math inline">\(\mathsf{PBC}\)</span> or <span class="math inline">\(\mathsf{DNE}\)</span> at all, they claim that a “proof by contradiction” and a “proof of negation” are essentially different, in that the latter is a valid proof but the former is doubtful, while their distinction is purely syntactical for classical mathematicians as the semantic equivalence would be trivial with <span class="math inline">\(\mathsf{PBC}\)</span> or <span class="math inline">\(\mathsf{DNE}\)</span>.</p>
<p>The rationale behind constructivists’ choice of ruling out indirect proofs by rejecting derivation rules like <span class="math inline">\(\mathsf{PBC}\)</span> and <span class="math inline">\(\mathsf{DNE}\)</span> comes into view when talking about first-order theories, where existential quantifiers are used. Say, if we wish to prove that there exists some <span class="math inline">\(x\)</span> with a property <span class="math inline">\(P\)</span>, we must specify an example <span class="math inline">\(t\)</span> which makes this property holds: <span class="math display">\[\exists_{\mathsf{I}_t} : \frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x : S.P}\]</span></p>
<p style="text-align:center !important;text-indent:0 !important">(<span class="math inline">\(t\)</span> is a term of sort <span class="math inline">\(S\)</span>)</p>
<p>This is something called a <em>constructive proof</em>, in the sense that in order to derive an existentialization, one must construct such a term explicitly, directly.</p>
<p>What if we allow <span class="math inline">\(\mathsf{PBC}\)</span> in our proofs then? We will be given enough power to utilize an alternate approach: Assume to the contrary that for all <span class="math inline">\(x\)</span> in <span class="math inline">\(S\)</span>, <span class="math inline">\(\lnot P\)</span> holds. Then we derive a contradiction. Thus, by <span class="math inline">\(\mathsf{PBC}\)</span>, there must exist some <span class="math inline">\(x\)</span> such that <span class="math inline">\(P\)</span> holds (since <span class="math inline">\(\lnot (\exists x : S.P) \equiv \forall x : S.\lnot P\)</span>). Formally, <span class="math display">\[\frac{\Gamma, \forall x : S.\lnot P \vdash \bot}{\Gamma \vdash \exists x : S.P}\]</span> Note that a term <span class="math inline">\(t\)</span> is nowhere to be evident in this form of proof. The downside of this classical approach of <em>existence proof</em> is that it is non-constructive, so even if you can derive a proof that some mathematical object exists, you can’t claim that you necessarily know what it is, since you have not concretely constructed such an object yet. Its existence is just “principally provable”, but not necessarily constructible or witnessable.</p>
<p>I would say it’s too much of a philosophical choice between classical logic and intuitionistic logic – at least for old school mathematicians who don’t practically mechanize their proofs at all. But one with some logic maturity should be able to draw a semantic distinction between a “proof by contradiction” that <span class="math inline">\(\vdash P\)</span> and a “proof of negation” that <span class="math inline">\(\vdash \lnot P\)</span>, bewaring of how their treatments can diverge in non-classical logic settings. It is still questionable to me whether every theorem provable in classical logic can be proved constructively, whatsoever, a constructive proof almost always makes more sense: <strong>If you claim that you have an apple, just show me the apple, instead of arguing to me sophistically that it can’t be the case that you do not have an apple.</strong></p>
<section id="references" class="level2">
<h2>References</h2>
<p>[1] Andrzej Filinski, “Course Notes for Semantics and Types, Lecture 1: Logic”.</p>
<p>[2] Robert Harper, “A ‘proof by contradiction’ is not a proof that ends with a contradiction”. <a href="https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/" class="uri">https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/</a></p>
<p>[3] Andrej Bauer, “Proof of negation and proof by contradiction”. <a href="http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/" class="uri">http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/</a></p>
<p>[4] Timothy Gowers, “When is proof by contradiction necessary?”. <a href="https://gowers.wordpress.com/2010/03/28/when-is-proof-by-contradiction-necessary/" class="uri">https://gowers.wordpress.com/2010/03/28/when-is-proof-by-contradiction-necessary/</a></p>
<p>[5] Terence Tao, “The ‘no self-defeating object’ argument”. <a href="https://terrytao.wordpress.com/2009/11/05/the-no-self-defeating-object-argument/" class="uri">https://terrytao.wordpress.com/2009/11/05/the-no-self-defeating-object-argument/</a></p>
</section>
      </div>
      <!-- (www.soimort.org) last updated: 2016-05-07 -->
      <aside id="soimort-toolbar">
        <a href="/"><i class="fa fa-home" aria-hidden="true"></i></a>
      </aside>
    </article>
  </body>
</html>