michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/19.08/Negation/index.html

610 lines
52 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html lang="en"><head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Negation: Negation, with intuitionistic and classical logic | Programming Language Foundations in Agda
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
<meta name="generator" content="Jekyll v3.9.0" />
<meta property="og:title" content="Negation: Negation, with intuitionistic and classical logic" />
<meta property="og:locale" content="en_US" />
<meta name="description" content="Programming Language Foundations in Agda" />
<meta property="og:description" content="Programming Language Foundations in Agda" />
<link rel="canonical" href="https://plfa.github.io/19.08/Negation/" />
<meta property="og:url" content="https://plfa.github.io/19.08/Negation/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/19.08/Negation/","headline":"Negation: Negation, with intuitionistic and classical logic","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/19.08/">Programming Language Foundations in Agda
</a>
<nav class="site-nav">
<span class="menu-icon">
<svg viewBox="0 0 18 15" width="18px" height="15px">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</span>
<div class="trigger">
<a class="page-link" href="/19.08/">The Book</a>
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
<a class="page-link" href="/19.08/Citing/">Citing</a>
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
</div>
</nav>
</div>
</header>
<main class="page-content" aria-label="Content">
<div class="wrapper">
<article class="post">
<header class="post-header">
<h1 class="post-title">Negation: Negation, with intuitionistic and classical logic</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Connectives/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part1/Negation.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/Quantifiers/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="180" class="Keyword">module</a> <a id="187" href="/19.08/Negation/" class="Module">plfa.part1.Negation</a> <a id="207" class="Keyword">where</a>
</pre>
<p>This chapter introduces negation, and discusses intuitionistic
and classical logic.</p>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="319" class="Keyword">open</a> <a id="324" class="Keyword">import</a> <a id="331" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="369" class="Keyword">using</a> <a id="375" class="Symbol">(</a><a id="376" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="379" class="Symbol">;</a> <a id="381" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="385" class="Symbol">)</a>
<a id="387" class="Keyword">open</a> <a id="392" class="Keyword">import</a> <a id="399" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="408" class="Keyword">using</a> <a id="414" class="Symbol">(</a><a id="415" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="416" class="Symbol">;</a> <a id="418" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="422" class="Symbol">;</a> <a id="424" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="427" class="Symbol">)</a>
<a id="429" class="Keyword">open</a> <a id="434" class="Keyword">import</a> <a id="441" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="452" class="Keyword">using</a> <a id="458" class="Symbol">(</a><a id="459" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a><a id="460" class="Symbol">;</a> <a id="462" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="468" class="Symbol">)</a>
<a id="470" class="Keyword">open</a> <a id="475" class="Keyword">import</a> <a id="482" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.html" class="Module">Data.Sum</a> <a id="491" class="Keyword">using</a> <a id="497" class="Symbol">(</a><a id="498" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">_⊎_</a><a id="501" class="Symbol">;</a> <a id="503" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a><a id="507" class="Symbol">;</a> <a id="509" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a><a id="513" class="Symbol">)</a>
<a id="515" class="Keyword">open</a> <a id="520" class="Keyword">import</a> <a id="527" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="540" class="Keyword">using</a> <a id="546" class="Symbol">(</a><a id="547" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="550" class="Symbol">)</a>
<a id="552" class="Keyword">open</a> <a id="557" class="Keyword">import</a> <a id="564" href="/19.08/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="587" class="Keyword">using</a> <a id="593" class="Symbol">(</a><a id="594" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">_≃_</a><a id="597" class="Symbol">;</a> <a id="599" href="plfa.part1.Isomorphism.html#2684" class="Postulate">extensionality</a><a id="613" class="Symbol">)</a>
</pre>
<h2 id="negation">Negation</h2>
<p>Given a proposition <code class="language-plaintext highlighter-rouge">A</code>, the negation <code class="language-plaintext highlighter-rouge">¬ A</code> holds if <code class="language-plaintext highlighter-rouge">A</code> cannot hold.
We formalise this idea by declaring negation to be the same
as implication of false:</p>
<pre class="Agda"><a id="¬_"></a><a id="793" href="/19.08/Negation/#793" class="Function Operator">¬_</a> <a id="796" class="Symbol">:</a> <a id="798" class="PrimitiveType">Set</a> <a id="802" class="Symbol">→</a> <a id="804" class="PrimitiveType">Set</a>
<a id="808" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="810" href="plfa.part1.Negation.html#810" class="Bound">A</a> <a id="812" class="Symbol">=</a> <a id="814" href="plfa.part1.Negation.html#810" class="Bound">A</a> <a id="816" class="Symbol">→</a> <a id="818" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
</pre>
<p>This is a form of <em>proof by contradiction</em>: if assuming <code class="language-plaintext highlighter-rouge">A</code> leads
to the conclusion <code class="language-plaintext highlighter-rouge">⊥</code> (a contradiction), then we must have <code class="language-plaintext highlighter-rouge">¬ A</code>.</p>
<p>Evidence that <code class="language-plaintext highlighter-rouge">¬ A</code> holds is of the form</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ{ x → N }
</code></pre></div></div>
<p>where <code class="language-plaintext highlighter-rouge">N</code> is a term of type <code class="language-plaintext highlighter-rouge">⊥</code> containing as a free variable <code class="language-plaintext highlighter-rouge">x</code> of type <code class="language-plaintext highlighter-rouge">A</code>.
In other words, evidence that <code class="language-plaintext highlighter-rouge">¬ A</code> holds is a function that converts evidence
that <code class="language-plaintext highlighter-rouge">A</code> holds into evidence that <code class="language-plaintext highlighter-rouge">⊥</code> holds.</p>
<p>Given evidence that both <code class="language-plaintext highlighter-rouge">¬ A</code> and <code class="language-plaintext highlighter-rouge">A</code> hold, we can conclude that <code class="language-plaintext highlighter-rouge">⊥</code> holds.
In other words, if both <code class="language-plaintext highlighter-rouge">¬ A</code> and <code class="language-plaintext highlighter-rouge">A</code> hold, then we have a contradiction:</p>
<pre class="Agda"><a id="¬-elim"></a><a id="1374" href="/19.08/Negation/#1374" class="Function">¬-elim</a> <a id="1381" class="Symbol">:</a> <a id="1383" class="Symbol">∀</a> <a id="1385" class="Symbol">{</a><a id="1386" href="plfa.part1.Negation.html#1386" class="Bound">A</a> <a id="1388" class="Symbol">:</a> <a id="1390" class="PrimitiveType">Set</a><a id="1393" class="Symbol">}</a>
<a id="1397" class="Symbol">→</a> <a id="1399" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="1401" href="plfa.part1.Negation.html#1386" class="Bound">A</a>
<a id="1405" class="Symbol">→</a> <a id="1407" href="/19.08/Negation/#1386" class="Bound">A</a>
<a id="1413" class="Comment">---</a>
<a id="1419" class="Symbol">→</a> <a id="1421" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
<a id="1423" href="/19.08/Negation/#1374" class="Function">¬-elim</a> <a id="1430" href="plfa.part1.Negation.html#1430" class="Bound">¬x</a> <a id="1433" href="plfa.part1.Negation.html#1433" class="Bound">x</a> <a id="1435" class="Symbol">=</a> <a id="1437" href="plfa.part1.Negation.html#1430" class="Bound">¬x</a> <a id="1440" href="plfa.part1.Negation.html#1433" class="Bound">x</a>
</pre>
<p>Here we write <code class="language-plaintext highlighter-rouge">¬x</code> for evidence of <code class="language-plaintext highlighter-rouge">¬ A</code> and <code class="language-plaintext highlighter-rouge">x</code> for evidence of <code class="language-plaintext highlighter-rouge">A</code>. This
means that <code class="language-plaintext highlighter-rouge">¬x</code> must be a function of type <code class="language-plaintext highlighter-rouge">A → ⊥</code>, and hence the application
<code class="language-plaintext highlighter-rouge">¬x x</code> must be of type <code class="language-plaintext highlighter-rouge">⊥</code>. Note that this rule is just a special case of <code class="language-plaintext highlighter-rouge">→-elim</code>.</p>
<p>We set the precedence of negation so that it binds more tightly
than disjunction and conjunction, but less tightly than anything else:</p>
<pre class="Agda"><a id="1825" class="Keyword">infix</a> <a id="1831" class="Number">3</a> <a id="1833" href="/19.08/Negation/#793" class="Function Operator">¬_</a>
</pre>
<p>Thus, <code class="language-plaintext highlighter-rouge">¬ A × ¬ B</code> parses as <code class="language-plaintext highlighter-rouge">(¬ A) × (¬ B)</code> and <code class="language-plaintext highlighter-rouge">¬ m ≡ n</code> as <code class="language-plaintext highlighter-rouge">¬ (m ≡ n)</code>.</p>
<p>In <em>classical</em> logic, we have that <code class="language-plaintext highlighter-rouge">A</code> is equivalent to <code class="language-plaintext highlighter-rouge">¬ ¬ A</code>.
As we discuss below, in Agda we use <em>intuitionistic</em> logic, where
we have only half of this equivalence, namely that <code class="language-plaintext highlighter-rouge">A</code> implies <code class="language-plaintext highlighter-rouge">¬ ¬ A</code>:</p>
<pre class="Agda"><a id="¬¬-intro"></a><a id="2122" href="/19.08/Negation/#2122" class="Function">¬¬-intro</a> <a id="2131" class="Symbol">:</a> <a id="2133" class="Symbol">∀</a> <a id="2135" class="Symbol">{</a><a id="2136" href="plfa.part1.Negation.html#2136" class="Bound">A</a> <a id="2138" class="Symbol">:</a> <a id="2140" class="PrimitiveType">Set</a><a id="2143" class="Symbol">}</a>
<a id="2147" class="Symbol">→</a> <a id="2149" href="/19.08/Negation/#2136" class="Bound">A</a>
<a id="2155" class="Comment">-----</a>
<a id="2163" class="Symbol">→</a> <a id="2165" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="2167" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="2169" href="plfa.part1.Negation.html#2136" class="Bound">A</a>
<a id="2171" href="/19.08/Negation/#2122" class="Function">¬¬-intro</a> <a id="2180" href="plfa.part1.Negation.html#2180" class="Bound">x</a> <a id="2183" class="Symbol">=</a> <a id="2186" class="Symbol">λ{</a><a id="2188" href="plfa.part1.Negation.html#2188" class="Bound">¬x</a> <a id="2191" class="Symbol">→</a> <a id="2193" href="plfa.part1.Negation.html#2188" class="Bound">¬x</a> <a id="2196" href="plfa.part1.Negation.html#2180" class="Bound">x</a><a id="2197" class="Symbol">}</a>
</pre>
<p>Let <code class="language-plaintext highlighter-rouge">x</code> be evidence of <code class="language-plaintext highlighter-rouge">A</code>. We show that assuming
<code class="language-plaintext highlighter-rouge">¬ A</code> leads to a contradiction, and hence <code class="language-plaintext highlighter-rouge">¬ ¬ A</code> must hold.
Let <code class="language-plaintext highlighter-rouge">¬x</code> be evidence of <code class="language-plaintext highlighter-rouge">¬ A</code>. Then from <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">¬ A</code>
we have a contradiction, evidenced by <code class="language-plaintext highlighter-rouge">¬x x</code>. Hence, we have
shown <code class="language-plaintext highlighter-rouge">¬ ¬ A</code>.</p>
<p>An equivalent way to write the above is as follows:</p>
<pre class="Agda"><a id="¬¬-intro′"></a><a id="2504" href="/19.08/Negation/#2504" class="Function">¬¬-intro′</a> <a id="2514" class="Symbol">:</a> <a id="2516" class="Symbol">∀</a> <a id="2518" class="Symbol">{</a><a id="2519" href="plfa.part1.Negation.html#2519" class="Bound">A</a> <a id="2521" class="Symbol">:</a> <a id="2523" class="PrimitiveType">Set</a><a id="2526" class="Symbol">}</a>
<a id="2530" class="Symbol">→</a> <a id="2532" href="/19.08/Negation/#2519" class="Bound">A</a>
<a id="2538" class="Comment">-----</a>
<a id="2546" class="Symbol">→</a> <a id="2548" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="2550" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="2552" href="plfa.part1.Negation.html#2519" class="Bound">A</a>
<a id="2554" href="/19.08/Negation/#2504" class="Function">¬¬-intro′</a> <a id="2564" href="plfa.part1.Negation.html#2564" class="Bound">x</a> <a id="2566" href="plfa.part1.Negation.html#2566" class="Bound">¬x</a> <a id="2569" class="Symbol">=</a> <a id="2571" href="plfa.part1.Negation.html#2566" class="Bound">¬x</a> <a id="2574" href="plfa.part1.Negation.html#2564" class="Bound">x</a>
</pre>
<p>Here we have simply converted the argument of the lambda term
to an additional argument of the function. We will usually
use this latter style, as it is more compact.</p>
<p>We cannot show that <code class="language-plaintext highlighter-rouge">¬ ¬ A</code> implies <code class="language-plaintext highlighter-rouge">A</code>, but we can show that
<code class="language-plaintext highlighter-rouge">¬ ¬ ¬ A</code> implies <code class="language-plaintext highlighter-rouge">¬ A</code>:</p>
<pre class="Agda"><a id="¬¬¬-elim"></a><a id="2840" href="/19.08/Negation/#2840" class="Function">¬¬¬-elim</a> <a id="2849" class="Symbol">:</a> <a id="2851" class="Symbol">∀</a> <a id="2853" class="Symbol">{</a><a id="2854" href="plfa.part1.Negation.html#2854" class="Bound">A</a> <a id="2856" class="Symbol">:</a> <a id="2858" class="PrimitiveType">Set</a><a id="2861" class="Symbol">}</a>
<a id="2865" class="Symbol">→</a> <a id="2867" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="2869" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="2871" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="2873" href="plfa.part1.Negation.html#2854" class="Bound">A</a>
<a id="2879" class="Comment">-------</a>
<a id="2889" class="Symbol">→</a> <a id="2891" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="2893" href="plfa.part1.Negation.html#2854" class="Bound">A</a>
<a id="2895" href="/19.08/Negation/#2840" class="Function">¬¬¬-elim</a> <a id="2904" href="plfa.part1.Negation.html#2904" class="Bound">¬¬¬x</a> <a id="2910" class="Symbol">=</a> <a id="2913" class="Symbol">λ</a> <a id="2915" href="plfa.part1.Negation.html#2915" class="Bound">x</a> <a id="2917" class="Symbol">→</a> <a id="2919" href="plfa.part1.Negation.html#2904" class="Bound">¬¬¬x</a> <a id="2924" class="Symbol">(</a><a id="2925" href="plfa.part1.Negation.html#2122" class="Function">¬¬-intro</a> <a id="2934" href="plfa.part1.Negation.html#2915" class="Bound">x</a><a id="2935" class="Symbol">)</a>
</pre>
<p>Let <code class="language-plaintext highlighter-rouge">¬¬¬x</code> be evidence of <code class="language-plaintext highlighter-rouge">¬ ¬ ¬ A</code>. We will show that assuming
<code class="language-plaintext highlighter-rouge">A</code> leads to a contradiction, and hence <code class="language-plaintext highlighter-rouge">¬ A</code> must hold.
Let <code class="language-plaintext highlighter-rouge">x</code> be evidence of <code class="language-plaintext highlighter-rouge">A</code>. Then by the previous result, we
can conclude <code class="language-plaintext highlighter-rouge">¬ ¬ A</code>, evidenced by <code class="language-plaintext highlighter-rouge">¬¬-intro x</code>. Then from
<code class="language-plaintext highlighter-rouge">¬ ¬ ¬ A</code> and <code class="language-plaintext highlighter-rouge">¬ ¬ A</code> we have a contradiction, evidenced by
<code class="language-plaintext highlighter-rouge">¬¬¬x (¬¬-intro x)</code>. Hence we have shown <code class="language-plaintext highlighter-rouge">¬ A</code>.</p>
<p>Another law of logic is <em>contraposition</em>,
stating that if <code class="language-plaintext highlighter-rouge">A</code> implies <code class="language-plaintext highlighter-rouge">B</code>, then <code class="language-plaintext highlighter-rouge">¬ B</code> implies <code class="language-plaintext highlighter-rouge">¬ A</code>:</p>
<pre class="Agda"><a id="contraposition"></a><a id="3397" href="/19.08/Negation/#3397" class="Function">contraposition</a> <a id="3412" class="Symbol">:</a> <a id="3414" class="Symbol">∀</a> <a id="3416" class="Symbol">{</a><a id="3417" href="plfa.part1.Negation.html#3417" class="Bound">A</a> <a id="3419" href="plfa.part1.Negation.html#3419" class="Bound">B</a> <a id="3421" class="Symbol">:</a> <a id="3423" class="PrimitiveType">Set</a><a id="3426" class="Symbol">}</a>
<a id="3430" class="Symbol">→</a> <a id="3432" class="Symbol">(</a><a id="3433" href="/19.08/Negation/#3417" class="Bound">A</a> <a id="3435" class="Symbol">→</a> <a id="3437" href="plfa.part1.Negation.html#3419" class="Bound">B</a><a id="3438" class="Symbol">)</a>
<a id="3444" class="Comment">-----------</a>
<a id="3458" class="Symbol">→</a> <a id="3460" class="Symbol">(</a><a id="3461" href="/19.08/Negation/#793" class="Function Operator">¬</a> <a id="3463" href="plfa.part1.Negation.html#3419" class="Bound">B</a> <a id="3465" class="Symbol">→</a> <a id="3467" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="3469" href="plfa.part1.Negation.html#3417" class="Bound">A</a><a id="3470" class="Symbol">)</a>
<a id="3472" href="/19.08/Negation/#3397" class="Function">contraposition</a> <a id="3487" href="plfa.part1.Negation.html#3487" class="Bound">f</a> <a id="3489" href="plfa.part1.Negation.html#3489" class="Bound">¬y</a> <a id="3492" href="plfa.part1.Negation.html#3492" class="Bound">x</a> <a id="3494" class="Symbol">=</a> <a id="3496" href="plfa.part1.Negation.html#3489" class="Bound">¬y</a> <a id="3499" class="Symbol">(</a><a id="3500" href="plfa.part1.Negation.html#3487" class="Bound">f</a> <a id="3502" href="plfa.part1.Negation.html#3492" class="Bound">x</a><a id="3503" class="Symbol">)</a>
</pre>
<p>Let <code class="language-plaintext highlighter-rouge">f</code> be evidence of <code class="language-plaintext highlighter-rouge">A → B</code> and let <code class="language-plaintext highlighter-rouge">¬y</code> be evidence of <code class="language-plaintext highlighter-rouge">¬ B</code>. We
will show that assuming <code class="language-plaintext highlighter-rouge">A</code> leads to a contradiction, and hence <code class="language-plaintext highlighter-rouge">¬ A</code>
must hold. Let <code class="language-plaintext highlighter-rouge">x</code> be evidence of <code class="language-plaintext highlighter-rouge">A</code>. Then from <code class="language-plaintext highlighter-rouge">A → B</code> and <code class="language-plaintext highlighter-rouge">A</code> we
may conclude <code class="language-plaintext highlighter-rouge">B</code>, evidenced by <code class="language-plaintext highlighter-rouge">f x</code>, and from <code class="language-plaintext highlighter-rouge">B</code> and <code class="language-plaintext highlighter-rouge">¬ B</code> we may
conclude <code class="language-plaintext highlighter-rouge">⊥</code>, evidenced by <code class="language-plaintext highlighter-rouge">¬y (f x)</code>. Hence, we have shown <code class="language-plaintext highlighter-rouge">¬ A</code>.</p>
<p>Using negation, it is straightforward to define inequality:</p>
<pre class="Agda"><a id="_≢_"></a><a id="3919" href="/19.08/Negation/#3919" class="Function Operator">_≢_</a> <a id="3923" class="Symbol">:</a> <a id="3925" class="Symbol">∀</a> <a id="3927" class="Symbol">{</a><a id="3928" href="plfa.part1.Negation.html#3928" class="Bound">A</a> <a id="3930" class="Symbol">:</a> <a id="3932" class="PrimitiveType">Set</a><a id="3935" class="Symbol">}</a> <a id="3937" class="Symbol">→</a> <a id="3939" href="plfa.part1.Negation.html#3928" class="Bound">A</a> <a id="3941" class="Symbol">→</a> <a id="3943" href="plfa.part1.Negation.html#3928" class="Bound">A</a> <a id="3945" class="Symbol">→</a> <a id="3947" class="PrimitiveType">Set</a>
<a id="3951" href="/19.08/Negation/#3951" class="Bound">x</a> <a id="3953" href="plfa.part1.Negation.html#3919" class="Function Operator">≢</a> <a id="3955" href="plfa.part1.Negation.html#3955" class="Bound">y</a> <a id="3958" class="Symbol">=</a> <a id="3961" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="3963" class="Symbol">(</a><a id="3964" href="plfa.part1.Negation.html#3951" class="Bound">x</a> <a id="3966" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3968" href="plfa.part1.Negation.html#3955" class="Bound">y</a><a id="3969" class="Symbol">)</a>
</pre>
<p>It is trivial to show distinct numbers are not equal:</p>
<pre class="Agda"><a id="4033" href="/19.08/Negation/#4033" class="Function">_</a> <a id="4035" class="Symbol">:</a> <a id="4037" class="Number">1</a> <a id="4039" href="plfa.part1.Negation.html#3919" class="Function Operator">≢</a> <a id="4041" class="Number">2</a>
<a id="4043" class="Symbol">_</a> <a id="4045" class="Symbol">=</a> <a id="4047" class="Symbol">λ()</a>
</pre>
<p>This is our first use of an absurd pattern in a lambda expression.
The type <code class="language-plaintext highlighter-rouge">M ≡ N</code> is occupied exactly when <code class="language-plaintext highlighter-rouge">M</code> and <code class="language-plaintext highlighter-rouge">N</code> simplify to
identical terms. Since <code class="language-plaintext highlighter-rouge">1</code> and <code class="language-plaintext highlighter-rouge">2</code> simplify to distinct normal forms,
Agda determines that there is no possible evidence that <code class="language-plaintext highlighter-rouge">1 ≡ 2</code>.
As a second example, it is also easy to validate
Peano’s postulate that zero is not the successor of any number:</p>
<pre class="Agda"><a id="peano"></a><a id="4440" href="/19.08/Negation/#4440" class="Function">peano</a> <a id="4446" class="Symbol">:</a> <a id="4448" class="Symbol">∀</a> <a id="4450" class="Symbol">{</a><a id="4451" href="plfa.part1.Negation.html#4451" class="Bound">m</a> <a id="4453" class="Symbol">:</a> <a id="4455" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="4456" class="Symbol">}</a> <a id="4458" class="Symbol">→</a> <a id="4460" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="4465" href="plfa.part1.Negation.html#3919" class="Function Operator">≢</a> <a id="4467" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="4471" href="plfa.part1.Negation.html#4451" class="Bound">m</a>
<a id="4473" href="/19.08/Negation/#4440" class="Function">peano</a> <a id="4479" class="Symbol">=</a> <a id="4481" class="Symbol">λ()</a>
</pre>
<p>The evidence is essentially the same, as the absurd pattern matches
all possible evidence of type <code class="language-plaintext highlighter-rouge">zero ≡ suc m</code>.</p>
<p>Given the correspondence of implication to exponentiation and
false to the type with no members, we can view negation as
raising to the zero power. This indeed corresponds to what
we know for arithmetic, where</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>0 ^ n ≡ 1, if n ≡ 0
≡ 0, if n ≢ 0
</code></pre></div></div>
<p>Indeed, there is exactly one proof of <code class="language-plaintext highlighter-rouge">⊥ → ⊥</code>. We can write
this proof two different ways:</p>
<pre class="Agda"><a id="id"></a><a id="4967" href="/19.08/Negation/#4967" class="Function">id</a> <a id="4970" class="Symbol">:</a> <a id="4972" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a> <a id="4974" class="Symbol">→</a> <a id="4976" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
<a id="4978" href="/19.08/Negation/#4967" class="Function">id</a> <a id="4981" href="plfa.part1.Negation.html#4981" class="Bound">x</a> <a id="4983" class="Symbol">=</a> <a id="4985" href="plfa.part1.Negation.html#4981" class="Bound">x</a>
<a id="id′"></a><a id="4988" href="/19.08/Negation/#4988" class="Function">id′</a> <a id="4992" class="Symbol">:</a> <a id="4994" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a> <a id="4996" class="Symbol">→</a> <a id="4998" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
<a id="5000" href="/19.08/Negation/#4988" class="Function">id′</a> <a id="5004" class="Symbol">()</a>
</pre>
<p>But, using extensionality, we can prove these equal:</p>
<pre class="Agda"><a id="id≡id′"></a><a id="5068" href="/19.08/Negation/#5068" class="Function">id≡id′</a> <a id="5075" class="Symbol">:</a> <a id="5077" href="plfa.part1.Negation.html#4967" class="Function">id</a> <a id="5080" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5082" href="plfa.part1.Negation.html#4988" class="Function">id′</a>
<a id="5086" href="/19.08/Negation/#5068" class="Function">id≡id′</a> <a id="5093" class="Symbol">=</a> <a id="5095" href="/19.08/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="5110" class="Symbol">(λ())</a>
</pre>
<p>By extensionality, <code class="language-plaintext highlighter-rouge">id ≡ id′</code> holds if for every
<code class="language-plaintext highlighter-rouge">x</code> in their domain we have <code class="language-plaintext highlighter-rouge">id x ≡ id′ x</code>. But there
is no <code class="language-plaintext highlighter-rouge">x</code> in their domain, so the equality holds trivially.</p>
<p>Indeed, we can show any two proofs of a negation are equal:</p>
<pre class="Agda"><a id="assimilation"></a><a id="5348" href="/19.08/Negation/#5348" class="Function">assimilation</a> <a id="5361" class="Symbol">:</a> <a id="5363" class="Symbol">∀</a> <a id="5365" class="Symbol">{</a><a id="5366" href="plfa.part1.Negation.html#5366" class="Bound">A</a> <a id="5368" class="Symbol">:</a> <a id="5370" class="PrimitiveType">Set</a><a id="5373" class="Symbol">}</a> <a id="5375" class="Symbol">(</a><a id="5376" href="plfa.part1.Negation.html#5376" class="Bound">¬x</a> <a id="5379" href="plfa.part1.Negation.html#5379" class="Bound">¬x′</a> <a id="5383" class="Symbol">:</a> <a id="5385" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="5387" href="plfa.part1.Negation.html#5366" class="Bound">A</a><a id="5388" class="Symbol">)</a> <a id="5390" class="Symbol">→</a> <a id="5392" href="plfa.part1.Negation.html#5376" class="Bound">¬x</a> <a id="5395" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5397" href="plfa.part1.Negation.html#5379" class="Bound">¬x′</a>
<a id="5401" href="/19.08/Negation/#5348" class="Function">assimilation</a> <a id="5414" href="plfa.part1.Negation.html#5414" class="Bound">¬x</a> <a id="5417" href="plfa.part1.Negation.html#5417" class="Bound">¬x′</a> <a id="5421" class="Symbol">=</a> <a id="5423" href="/19.08/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="5438" class="Symbol">(λ</a> <a id="5441" href="plfa.part1.Negation.html#5441" class="Bound">x</a> <a id="5443" class="Symbol">→</a> <a id="5445" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="5452" class="Symbol">(</a><a id="5453" href="plfa.part1.Negation.html#5414" class="Bound">¬x</a> <a id="5456" href="plfa.part1.Negation.html#5441" class="Bound">x</a><a id="5457" class="Symbol">))</a>
</pre>
<p>Evidence for <code class="language-plaintext highlighter-rouge">¬ A</code> implies that any evidence of <code class="language-plaintext highlighter-rouge">A</code>
immediately leads to a contradiction. But extensionality
quantifies over all <code class="language-plaintext highlighter-rouge">x</code> such that <code class="language-plaintext highlighter-rouge">A</code> holds, hence any
such <code class="language-plaintext highlighter-rouge">x</code> immediately leads to a contradiction,
again causing the equality to hold trivially.</p>
<h4 id="exercise--irreflexive-recommended">Exercise <code class="language-plaintext highlighter-rouge">&lt;-irreflexive</code> (recommended)</h4>
<p>Using negation, show that
<a href="/19.08/Relations/#strict-inequality">strict inequality</a>
is irreflexive, that is, <code class="language-plaintext highlighter-rouge">n &lt; n</code> holds for no <code class="language-plaintext highlighter-rouge">n</code>.</p>
<pre class="Agda"><a id="5920" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-trichotomy-practice">Exercise <code class="language-plaintext highlighter-rouge">trichotomy</code> (practice)</h4>
<p>Show that strict inequality satisfies
<a href="/19.08/Relations/#trichotomy">trichotomy</a>,
that is, for any naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code> exactly one of the following holds:</p>
<ul>
<li><code class="language-plaintext highlighter-rouge">m &lt; n</code></li>
<li><code class="language-plaintext highlighter-rouge">m ≡ n</code></li>
<li><code class="language-plaintext highlighter-rouge">m &gt; n</code></li>
</ul>
<p>Here “exactly one” means that not only one of the three must hold,
but that when one holds the negation of the other two must also hold.</p>
<pre class="Agda"><a id="6330" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise--dual--recommended">Exercise <code class="language-plaintext highlighter-rouge">⊎-dual-×</code> (recommended)</h4>
<p>Show that conjunction, disjunction, and negation are related by a
version of De Morgan’s Law.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
</code></pre></div></div>
<p>This result is an easy consequence of something we’ve proved previously.</p>
<pre class="Agda"><a id="6602" class="Comment">-- Your code goes here</a>
</pre>
<p>Do we also have the following?</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
</code></pre></div></div>
<p>If so, prove; if not, can you give a relation weaker than
isomorphism that relates the two sides?</p>
<h2 id="intuitive-and-classical-logic">Intuitive and Classical logic</h2>
<p>In Gilbert and Sullivan’s <em>The Gondoliers</em>, Casilda is told that
as an infant she was married to the heir of the King of Batavia, but
that due to a mix-up no one knows which of two individuals, Marco or
Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say
that I am married to one of two gondoliers, but it is impossible to
say which?” To which the response is “Without any doubt of any kind
whatever.”</p>
<p>Logic comes in many varieties, and one distinction is between
<em>classical</em> and <em>intuitionistic</em>. Intuitionists, concerned
by assumptions made by some logicians about the nature of
infinity, insist upon a constructionist notion of truth. In
particular, they insist that a proof of <code class="language-plaintext highlighter-rouge">A ⊎ B</code> must show
<em>which</em> of <code class="language-plaintext highlighter-rouge">A</code> or <code class="language-plaintext highlighter-rouge">B</code> holds, and hence they would reject the
claim that Casilda is married to Marco or Giuseppe until one of the
two was identified as her husband. Perhaps Gilbert and Sullivan
anticipated intuitionism, for their story’s outcome is that the heir
turns out to be a third individual, Luiz, with whom Casilda is,
conveniently, already in love.</p>
<p>Intuitionists also reject the law of the excluded middle, which
asserts <code class="language-plaintext highlighter-rouge">A ⊎ ¬ A</code> for every <code class="language-plaintext highlighter-rouge">A</code>, since the law gives no clue as to
<em>which</em> of <code class="language-plaintext highlighter-rouge">A</code> or <code class="language-plaintext highlighter-rouge">¬ A</code> holds. Heyting formalised a variant of
Hilbert’s classical logic that captures the intuitionistic notion of
provability. In particular, the law of the excluded middle is provable
in Hilbert’s logic, but not in Heyting’s. Further, if the law of the
excluded middle is added as an axiom to Heyting’s logic, then it
becomes equivalent to Hilbert’s. Kolmogorov showed the two logics
were closely related: he gave a double-negation translation, such that
a formula is provable in classical logic if and only if its
translation is provable in intuitionistic logic.</p>
<p>Propositions as Types was first formulated for intuitionistic logic.
It is a perfect fit, because in the intuitionist interpretation the
formula <code class="language-plaintext highlighter-rouge">A ⊎ B</code> is provable exactly when one exhibits either a proof
of <code class="language-plaintext highlighter-rouge">A</code> or a proof of <code class="language-plaintext highlighter-rouge">B</code>, so the type corresponding to disjunction is
a disjoint sum.</p>
<p>(Parts of the above are adopted from “Propositions as Types”, Philip Wadler,
<em>Communications of the ACM</em>, December 2015.)</p>
<h2 id="excluded-middle-is-irrefutable">Excluded middle is irrefutable</h2>
<p>The law of the excluded middle can be formulated as follows:</p>
<pre class="Agda"><a id="9138" class="Keyword">postulate</a>
<a id="em"></a><a id="9150" href="/19.08/Negation/#9150" class="Postulate">em</a> <a id="9153" class="Symbol">:</a> <a id="9155" class="Symbol">∀</a> <a id="9157" class="Symbol">{</a><a id="9158" href="plfa.part1.Negation.html#9158" class="Bound">A</a> <a id="9160" class="Symbol">:</a> <a id="9162" class="PrimitiveType">Set</a><a id="9165" class="Symbol">}</a> <a id="9167" class="Symbol">→</a> <a id="9169" href="plfa.part1.Negation.html#9158" class="Bound">A</a> <a id="9171" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">⊎</a> <a id="9173" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="9175" href="plfa.part1.Negation.html#9158" class="Bound">A</a>
</pre>
<p>As we noted, the law of the excluded middle does not hold in
intuitionistic logic. However, we can show that it is <em>irrefutable</em>,
meaning that the negation of its negation is provable (and hence that
its negation is never provable):</p>
<pre class="Agda"><a id="em-irrefutable"></a><a id="9419" href="/19.08/Negation/#9419" class="Function">em-irrefutable</a> <a id="9434" class="Symbol">:</a> <a id="9436" class="Symbol">∀</a> <a id="9438" class="Symbol">{</a><a id="9439" href="plfa.part1.Negation.html#9439" class="Bound">A</a> <a id="9441" class="Symbol">:</a> <a id="9443" class="PrimitiveType">Set</a><a id="9446" class="Symbol">}</a> <a id="9448" class="Symbol">→</a> <a id="9450" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="9452" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="9454" class="Symbol">(</a><a id="9455" href="plfa.part1.Negation.html#9439" class="Bound">A</a> <a id="9457" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">⊎</a> <a id="9459" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="9461" href="plfa.part1.Negation.html#9439" class="Bound">A</a><a id="9462" class="Symbol">)</a>
<a id="9464" href="/19.08/Negation/#9419" class="Function">em-irrefutable</a> <a id="9479" class="Symbol">=</a> <a id="9481" class="Symbol">λ</a> <a id="9483" href="plfa.part1.Negation.html#9483" class="Bound">k</a> <a id="9485" class="Symbol">→</a> <a id="9487" href="plfa.part1.Negation.html#9483" class="Bound">k</a> <a id="9489" class="Symbol">(</a><a id="9490" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="9495" class="Symbol">(λ</a> <a id="9498" href="plfa.part1.Negation.html#9498" class="Bound">x</a> <a id="9500" class="Symbol">→</a> <a id="9502" href="plfa.part1.Negation.html#9483" class="Bound">k</a> <a id="9504" class="Symbol">(</a><a id="9505" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="9510" href="plfa.part1.Negation.html#9498" class="Bound">x</a><a id="9511" class="Symbol">)))</a>
</pre>
<p>The best way to explain this code is to develop it interactively:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>em-irrefutable k = ?
</code></pre></div></div>
<p>Given evidence <code class="language-plaintext highlighter-rouge">k</code> that <code class="language-plaintext highlighter-rouge">¬ (A ⊎ ¬ A)</code>, that is, a function that given a
value of type <code class="language-plaintext highlighter-rouge">A ⊎ ¬ A</code> returns a value of the empty type, we must fill
in <code class="language-plaintext highlighter-rouge">?</code> with a term that returns a value of the empty type. The only way
we can get a value of the empty type is by applying <code class="language-plaintext highlighter-rouge">k</code> itself, so let’s
expand the hole accordingly:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>em-irrefutable k = k ?
</code></pre></div></div>
<p>We need to fill the new hole with a value of type <code class="language-plaintext highlighter-rouge">A ⊎ ¬ A</code>. We don’t have
a value of type <code class="language-plaintext highlighter-rouge">A</code> to hand, so let’s pick the second disjunct:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>em-irrefutable k = k (inj₂ λ{ x → ? })
</code></pre></div></div>
<p>The second disjunct accepts evidence of <code class="language-plaintext highlighter-rouge">¬ A</code>, that is, a function
that given a value of type <code class="language-plaintext highlighter-rouge">A</code> returns a value of the empty type. We
bind <code class="language-plaintext highlighter-rouge">x</code> to the value of type <code class="language-plaintext highlighter-rouge">A</code>, and now we need to fill in the hole
with a value of the empty type. Once again, the only way we can get a
value of the empty type is by applying <code class="language-plaintext highlighter-rouge">k</code> itself, so let’s expand the
hole accordingly:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>em-irrefutable k = k (inj₂ λ{ x → k ? })
</code></pre></div></div>
<p>This time we do have a value of type <code class="language-plaintext highlighter-rouge">A</code> to hand, namely <code class="language-plaintext highlighter-rouge">x</code>, so we can
pick the first disjunct:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })
</code></pre></div></div>
<p>There are no holes left! This completes the proof.</p>
<p>The following story illustrates the behaviour of the term we have created.
(With apologies to Peter Selinger, who tells a similar story
about a king, a wizard, and the Philosopher’s stone.)</p>
<p>Once upon a time, the devil approached a man and made an offer:
“Either (a) I will give you one billion dollars, or (b) I will grant
you any wish if you pay me one billion dollars.
Of course, I get to choose whether I offer (a) or (b).”</p>
<p>The man was wary. Did he need to sign over his soul?
No, said the devil, all the man need do is accept the offer.</p>
<p>The man pondered. If he was offered (b) it was unlikely that he would
ever be able to buy the wish, but what was the harm in having the
opportunity available?</p>
<p>“I accept,” said the man at last. “Do I get (a) or (b)?”</p>
<p>The devil paused. “I choose (b).”</p>
<p>The man was disappointed but not surprised. That was that, he thought.
But the offer gnawed at him. Imagine what he could do with his wish!
Many years passed, and the man began to accumulate money. To get the
money he sometimes did bad things, and dimly he realised that
this must be what the devil had in mind.
Eventually he had his billion dollars, and the devil appeared again.</p>
<p>“Here is a billion dollars,” said the man, handing over a valise
containing the money. “Grant me my wish!”</p>
<p>The devil took possession of the valise. Then he said, “Oh, did I say
(b) before? I’m so sorry. I meant (a). It is my great pleasure to
give you one billion dollars.”</p>
<p>And the devil handed back to the man the same valise that the man had
just handed to him.</p>
<p>(Parts of the above are adopted from “Call-by-Value is Dual to Call-by-Name”,
Philip Wadler, <em>International Conference on Functional Programming</em>, 2003.)</p>
<h4 id="exercise-classical-stretch">Exercise <code class="language-plaintext highlighter-rouge">Classical</code> (stretch)</h4>
<p>Consider the following principles:</p>
<ul>
<li>Excluded Middle: <code class="language-plaintext highlighter-rouge">A ⊎ ¬ A</code>, for all <code class="language-plaintext highlighter-rouge">A</code></li>
<li>Double Negation Elimination: <code class="language-plaintext highlighter-rouge">¬ ¬ A → A</code>, for all <code class="language-plaintext highlighter-rouge">A</code></li>
<li>Peirce’s Law: <code class="language-plaintext highlighter-rouge">((A → B) → A) → A</code>, for all <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>.</li>
<li>Implication as disjunction: <code class="language-plaintext highlighter-rouge">(A → B) → ¬ A ⊎ B</code>, for all <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>.</li>
<li>De Morgan: <code class="language-plaintext highlighter-rouge">¬ (¬ A × ¬ B) → A ⊎ B</code>, for all <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>.</li>
</ul>
<p>Show that each of these implies all the others.</p>
<pre class="Agda"><a id="12900" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-stable-stretch">Exercise <code class="language-plaintext highlighter-rouge">Stable</code> (stretch)</h4>
<p>Say that a formula is <em>stable</em> if double negation elimination holds for it:</p>
<pre class="Agda"><a id="Stable"></a><a id="13043" href="/19.08/Negation/#13043" class="Function">Stable</a> <a id="13050" class="Symbol">:</a> <a id="13052" class="PrimitiveType">Set</a> <a id="13056" class="Symbol">→</a> <a id="13058" class="PrimitiveType">Set</a>
<a id="13062" href="/19.08/Negation/#13043" class="Function">Stable</a> <a id="13069" href="plfa.part1.Negation.html#13069" class="Bound">A</a> <a id="13071" class="Symbol">=</a> <a id="13073" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="13075" href="plfa.part1.Negation.html#793" class="Function Operator">¬</a> <a id="13077" href="plfa.part1.Negation.html#13069" class="Bound">A</a> <a id="13079" class="Symbol">→</a> <a id="13081" href="plfa.part1.Negation.html#13069" class="Bound">A</a>
</pre>
<p>Show that any negated formula is stable, and that the conjunction
of two stable formulas is stable.</p>
<pre class="Agda"><a id="13192" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="standard-prelude">Standard Prelude</h2>
<p>Definitions similar to those in this chapter can be found in the standard library:</p>
<pre class="Agda"><a id="13328" class="Keyword">import</a> <a id="13335" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="13352" class="Keyword">using</a> <a id="13358" class="Symbol">(</a><a id="13359" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="13361" class="Symbol">)</a>
<a id="13363" class="Keyword">import</a> <a id="13370" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="13396" class="Keyword">using</a> <a id="13402" class="Symbol">(</a><a id="13403" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#880" class="Function">contraposition</a><a id="13417" class="Symbol">)</a>
</pre>
<h2 id="unicode">Unicode</h2>
<p>This chapter uses the following unicode:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>¬ U+00AC NOT SIGN (\neg)
≢ U+2262 NOT IDENTICAL TO (\==n)
</code></pre></div></div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Connectives/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part1/Negation.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/Quantifiers/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/19.08/"></data>
<div class="wrapper">
<h2 class="footer-heading">Programming Language Foundations in Agda
</h2><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Philip Wadler</li>
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Wen Kokke</li>
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Jeremy Siek</li>
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
</div>
</footer>
<!-- Import jQuery -->
<script type="text/javascript" src="/19.08/assets/jquery.js"></script>
<script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="/19.08/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink