Created
July 30, 2016 17:46
-
-
Save rplacd/8baf8aa8d47a9abf9a4b87771672006d to your computer and use it in GitHub Desktop.
A comparison of natural deduction and the sequent calculus as formalisms of deduction. Formalised in Coq.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" | |
| "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> | |
| <html xmlns="http://www.w3.org/1999/xhtml"> | |
| <head> | |
| <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> | |
| <style type="text/css"> | |
| body { padding: 0px 0px; | |
| margin: 0px 0px; | |
| background-color: white } | |
| #page { display: block; | |
| padding: 0px; | |
| margin: 0px; | |
| padding-bottom: 10px; } | |
| #header { display: block; | |
| position: relative; | |
| padding: 0; | |
| margin: 0; | |
| vertical-align: middle; | |
| border-bottom-style: solid; | |
| border-width: thin } | |
| #header h1 { padding: 0; | |
| margin: 0;} | |
| /* Contents */ | |
| #main{ display: block; | |
| padding: 10px; | |
| font-family: sans-serif; | |
| font-size: 100%; | |
| line-height: 100% } | |
| #main h1 { line-height: 95% } /* allow for multi-line headers */ | |
| #main a.idref:visited {color : #416DFF; text-decoration : none; } | |
| #main a.idref:link {color : #416DFF; text-decoration : none; } | |
| #main a.idref:hover {text-decoration : none; } | |
| #main a.idref:active {text-decoration : none; } | |
| #main a.modref:visited {color : #416DFF; text-decoration : none; } | |
| #main a.modref:link {color : #416DFF; text-decoration : none; } | |
| #main a.modref:hover {text-decoration : none; } | |
| #main a.modref:active {text-decoration : none; } | |
| #main .keyword { color : #cf1d1d } | |
| #main { color: black } | |
| .section { background-color: rgb(60%,60%,100%); | |
| padding-top: 13px; | |
| padding-bottom: 13px; | |
| padding-left: 3px; | |
| margin-top: 5px; | |
| margin-bottom: 5px; | |
| font-size : 175% } | |
| h2.section { background-color: rgb(80%,80%,100%); | |
| padding-left: 3px; | |
| padding-top: 12px; | |
| padding-bottom: 10px; | |
| font-size : 130% } | |
| h3.section { background-color: rgb(90%,90%,100%); | |
| padding-left: 3px; | |
| padding-top: 7px; | |
| padding-bottom: 7px; | |
| font-size : 115% } | |
| h4.section { | |
| /* | |
| background-color: rgb(80%,80%,80%); | |
| max-width: 20em; | |
| padding-left: 5px; | |
| padding-top: 5px; | |
| padding-bottom: 5px; | |
| */ | |
| background-color: white; | |
| padding-left: 0px; | |
| padding-top: 0px; | |
| padding-bottom: 0px; | |
| font-size : 100%; | |
| font-weight : bold; | |
| text-decoration : underline; | |
| } | |
| #main .doc { margin: 0px; | |
| font-family: sans-serif; | |
| font-size: 100%; | |
| line-height: 125%; | |
| max-width: 40em; | |
| color: black; | |
| padding: 10px; | |
| background-color: #90bdff } | |
| .inlinecode { | |
| display: inline; | |
| /* font-size: 125%; */ | |
| color: #666666; | |
| font-family: monospace } | |
| .doc .inlinecode { | |
| display: inline; | |
| font-size: 120%; | |
| color: rgb(30%,30%,70%); | |
| font-family: monospace } | |
| .doc .inlinecode .id { | |
| color: rgb(30%,30%,70%); | |
| } | |
| .inlinecodenm { | |
| display: inline; | |
| color: #444444; | |
| } | |
| .doc .code { | |
| display: inline; | |
| font-size: 120%; | |
| color: rgb(30%,30%,70%); | |
| font-family: monospace } | |
| .comment { | |
| display: inline; | |
| font-family: monospace; | |
| color: rgb(50%,50%,80%); | |
| } | |
| .code { | |
| display: block; | |
| /* padding-left: 15px; */ | |
| font-size: 110%; | |
| font-family: monospace; | |
| } | |
| table.infrule { | |
| border: 0px; | |
| margin-left: 50px; | |
| margin-top: 10px; | |
| margin-bottom: 10px; | |
| } | |
| td.infrule { | |
| font-family: monospace; | |
| text-align: center; | |
| /* color: rgb(35%,35%,70%); */ | |
| padding: 0px; | |
| line-height: 100%; | |
| } | |
| tr.infrulemiddle hr { | |
| margin: 1px 0 1px 0; | |
| } | |
| .infrulenamecol { | |
| color: rgb(60%,60%,60%); | |
| font-size: 80%; | |
| padding-left: 1em; | |
| padding-bottom: 0.1em | |
| } | |
| /* Pied de page */ | |
| #footer { font-size: 65%; | |
| font-family: sans-serif; } | |
| /* Identifiers: <span class="id" title="...">) */ | |
| .id { display: inline; } | |
| .id[title="constructor"] { | |
| color: rgb(60%,0%,0%); | |
| } | |
| .id[title="var"] { | |
| color: rgb(40%,0%,40%); | |
| } | |
| .id[title="variable"] { | |
| color: rgb(40%,0%,40%); | |
| } | |
| .id[title="definition"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="abbreviation"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="lemma"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="instance"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="projection"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="method"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[title="inductive"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[title="record"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[title="class"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[title="keyword"] { | |
| color : #cf1d1d; | |
| /* color: black; */ | |
| } | |
| /* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ | |
| .id[type="constructor"] { | |
| color: rgb(60%,0%,0%); | |
| } | |
| .id[type="var"] { | |
| color: rgb(40%,0%,40%); | |
| } | |
| .id[type="variable"] { | |
| color: rgb(40%,0%,40%); | |
| } | |
| .id[type="definition"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="abbreviation"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="lemma"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="instance"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="projection"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="method"] { | |
| color: rgb(0%,40%,0%); | |
| } | |
| .id[type="inductive"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[type="record"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[type="class"] { | |
| color: rgb(0%,0%,80%); | |
| } | |
| .id[type="keyword"] { | |
| color : #cf1d1d; | |
| /* color: black; */ | |
| } | |
| .inlinecode .id { | |
| color: rgb(0%,0%,0%); | |
| } | |
| /* TOC */ | |
| #toc h2 { | |
| padding: 10px; | |
| background-color: rgb(60%,60%,100%); | |
| } | |
| #toc li { | |
| padding-bottom: 8px; | |
| } | |
| /* Index */ | |
| #index { | |
| margin: 0; | |
| padding: 0; | |
| width: 100%; | |
| } | |
| #index #frontispiece { | |
| margin: 1em auto; | |
| padding: 1em; | |
| width: 60%; | |
| } | |
| .booktitle { font-size : 140% } | |
| .authors { font-size : 90%; | |
| line-height: 115%; } | |
| .moreauthors { font-size : 60% } | |
| #index #entrance { | |
| text-align: center; | |
| } | |
| #index #entrance .spacer { | |
| margin: 0 30px 0 30px; | |
| } | |
| #index #footer { | |
| position: absolute; | |
| bottom: 0; | |
| } | |
| .paragraph { | |
| height: 0.75em; | |
| } | |
| ul.doclist { | |
| margin-top: 0em; | |
| margin-bottom: 0em; | |
| } | |
| </style> | |
| <title></title> | |
| </head> | |
| <body> | |
| <div id="page"> | |
| <div id="header"> | |
| </div> | |
| <div id="main"> | |
| <div class="code"> | |
| <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="var">Coq.Strings.String</span>.<br/> | |
| <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="var">Coq.Lists.List</span>.<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| <a name="lab1"></a><h1 class="section">A taste of Curry-Howard</h1> | |
| <div class="paragraph"> </div> | |
| In particular, how do we show a λ-calculus term is valid proof for a logical proposition? | |
| <div class="paragraph"> </div> | |
| <a name="lab2"></a><h2 class="section">An overview</h2> | |
| <div class="paragraph"> </div> | |
| To be more specific: I assume you've worked before with deduction systems that are given in the assumptions-over-conclusion notation. (If you've seen them stacked on top of each other in proof trees, so much the better.) In particular, if you understand a definition in that form of a relation like the has-type or evaluates-to relation, you should be set. | |
| <div class="paragraph"> </div> | |
| Throughout we make clear the distinction between metalogic - Coq - and logic. | |
| Our logic is the implicational logic: atomic propositions and the connective of implication, <span class="inlinecode">→</span>. Two formalisms of proofs ("proof systems") for this logic are then defined in the metalogic: natural deduction and the sequent calculus. | |
| <div class="paragraph"> </div> | |
| An interesting interlude follows: what distinguishes the two? Conversely, what unites the two - how come we aren't comparing apples to oranges? Equally interesting: all our proofs of logical statements - acts of reasoning with the rules that bind the proof system - are given by metalogical proofs, written in Coq's term language. What is a proof on the level of the logic itself? | |
| <div class="paragraph"> </div> | |
| Introducing the Curry-Howard correspondence answers this question, and restores the propositional logic to full ability: we can now give proofs in the level of the propositional logic, with the λ-calculus. We show that the ability to give logical proofs shouldn't change the metalogical proofs of the same statements. | |
| <div class="paragraph"> </div> | |
| <a name="lab3"></a><h2 class="section">Utility definitions</h2> | |
| <div class="paragraph"> </div> | |
| We use lists to represent bunches of assumptions and conclusions; when working on them, we need to add elements to both the front and the back of lists. So we provide a uniform notation for both operations: | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Notation</span> "a :+ B" := (<span class="id" title="var">cons</span> <span class="id" title="var">a</span> <span class="id" title="var">B</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 57, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/> | |
| <span class="id" title="keyword">Notation</span> "B +: c" := (<span class="id" title="var">app</span> <span class="id" title="var">B</span> (<span class="id" title="var">c</span> :: <span class="id" title="var">nil</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 58, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| Note that in the operators, <span class="inlinecode">:</span> is always on the side of the element, as in <span class="inlinecode">::</span>; and <span class="inlinecode">+</span> is on the side of the list, as in <span class="inlinecode">++</span>. | |
| <div class="paragraph"> </div> | |
| <a name="lab4"></a><h2 class="section">The logic: propositional logic</h2> | |
| <div class="paragraph"> </div> | |
| We deal with implicational logic: atomic propositions, and implications between propositions (<span class="inlinecode">→</span>). These are the terms of our logic. (It's another thing entirely to say how we can manipulate these terms - that comes next.) | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">prop</span> : <span class="id" title="keyword">Set</span> :=<br/> | |
| | <span class="id" title="var">Atom</span> : <span class="id" title="var">string</span> → <span class="id" title="var">prop</span><br/> | |
| | <span class="id" title="var">Impl</span> : <span class="id" title="var">prop</span> → <span class="id" title="var">prop</span> → <span class="id" title="var">prop</span>.<br/> | |
| <span class="id" title="keyword">Notation</span> "A => B" := (<span class="id" title="var">Impl</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 56, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| <a name="lab5"></a><h2 class="section">The formalisms of proof - natural deduction and the sequent calculus</h2> | |
| <div class="paragraph"> </div> | |
| We assume that what we want to do with a logic is, given a statement, try to derive a proof for it. "Informal" introductions to logic and proof usually conclude by offering a procedure that takes assumptions to conclusions: to show the conjunction of two statements, show each statement individually; and so on. It then should come to no surprise that both formalisms here distill the bookkeeping to the bare essentials of this process: a turnstile <span class="inlinecode">|-</span> dividing, on the left, what is known; on the right, what is being concluded. | |
| <div class="paragraph"> </div> | |
| We should make the distinction between the logic and metalogic clear. The logic is the propositional calculus - it is being implemented or hosted. The metalogic is the type theory Coq encodes, a variant on "minimal logic". (But more on type theories being logics below!) So the metalogical proposition <span class="inlinecode"><span class="id" title="var">A</span>,</span> <span class="inlinecode"><span class="id" title="var">B</span></span> <span class="inlinecode">|-</span> <span class="inlinecode"><span class="id" title="var">C</span></span> states that, by the rules of the proof system, <span class="inlinecode"><span class="id" title="var">C</span></span> can be derived from <span class="inlinecode"><span class="id" title="var">A</span></span> and <span class="inlinecode"><span class="id" title="var">B</span></span>. Note that our proofs remain in the metalogic - we'll see how to lower down our proofs down to the level of the logic later. | |
| <div class="paragraph"> </div> | |
| Two systems are presented: natural deduction and the sequent calculus; we call them both proof systems. Both are defined by Gerhard Genzten in his classic <i>Investigations into Logical Deduction</i>. (Other formalisms of deduction are available - Russell and Whitehead's <i>Principia</i> begins by defining deduction rules; so does Gottlob Frege in his <i>Begriffsschrift</i>.) | |
| <div class="paragraph"> </div> | |
| Can you see how they're reasonable as models of deduction? We'll see them proving the correctness of families of deductions below. We'll then compare the two - but there is no clear-cut duality between the two. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Reserved Notation</span> "A ]- B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90).<br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">NatDed</span> : <span class="id" title="var">list</span> <span class="id" title="var">prop</span> → <span class="id" title="var">prop</span> → <span class="id" title="keyword">Prop</span> :=<br/> | |
| | <span class="id" title="var">N_Id</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]- <span class="id" title="var">A</span>)<br/> | |
| | <span class="id" title="var">N_Impl_intro</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>) →<br/> | |
| ( <span class="id" title="var">L</span> ]- <span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">N_Impl_elim</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> ]- <span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span>) → (<span class="id" title="var">L</span> ]- <span class="id" title="var">A</span>) →<br/> | |
| (<span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">N_Interchange</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">A</span> ++ <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> ]- <span class="id" title="var">C</span>) →<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">B</span> ++ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span> ]- <span class="id" title="var">C</span>)<br/> | |
| | <span class="id" title="var">N_Thinning</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>) →<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">N_Contraction</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>) →<br/> | |
| ( <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]- <span class="id" title="var">B</span>)<br/> | |
| <span class="id" title="keyword">where</span> "A ]- B" := (<span class="id" title="var">NatDed</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>).<br/> | |
| <br/> | |
| <span class="id" title="keyword">Reserved Notation</span> "A }- B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90).<br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">Sequent</span> : <span class="id" title="var">list</span> <span class="id" title="var">prop</span> → <span class="id" title="var">list</span> <span class="id" title="var">prop</span> → <span class="id" title="keyword">Prop</span> :=<br/> | |
| | <span class="id" title="var">S_Id</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">S_Impl_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">B</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span> ) →<br/> | |
| (<span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span> )<br/> | |
| | <span class="id" title="var">S_Impl_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> ) →<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> )<br/> | |
| | <span class="id" title="var">S_Interchange_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">A</span> ++ <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> }- <span class="id" title="var">N</span>) →<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">B</span> ++ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span> }- <span class="id" title="var">N</span>)<br/> | |
| | <span class="id" title="var">S_Interchange_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">M</span> ++ <span class="id" title="var">A</span> :: <span class="id" title="var">B</span> :+ <span class="id" title="var">N</span>) →<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">M</span> ++ <span class="id" title="var">B</span> :: <span class="id" title="var">A</span> :+ <span class="id" title="var">N</span>)<br/> | |
| | <span class="id" title="var">S_Thinning_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">S_Thinning_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">S_Contraction_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span>) →<br/> | |
| ( <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">S_Contraction_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">L</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">S_Cut</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span> <span class="id" title="var">O</span>:<span class="id" title="var">list</span> <span class="id" title="var">prop</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }- <span class="id" title="var">M</span>) → (<span class="id" title="var">N</span> }- <span class="id" title="var">A</span> :+ <span class="id" title="var">O</span>) →<br/> | |
| (<span class="id" title="var">L</span> ++ <span class="id" title="var">N</span> }- <span class="id" title="var">M</span> ++ <span class="id" title="var">O</span>)<br/> | |
| <span class="id" title="keyword">where</span> "A }- B" := (<span class="id" title="var">Sequent</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| A fine technical point involved here is the representation of lists of assumptions. As data types, what should we be able to do with them? Consider the options available to us: | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> The set, the canonical representation. Sets don't work well as terms in types, though: term unification is not equivalence for sets. Unification does not take into account permutation - <span class="inlinecode">{<span class="id" title="var">A</span>,</span> <span class="inlinecode"><span class="id" title="var">B</span>,</span> <span class="inlinecode"><span class="id" title="var">C</span>}</span> does not unify with <span class="inlinecode">{<span class="id" title="var">C</span>,</span> <span class="inlinecode"><span class="id" title="var">B</span>,</span> <span class="inlinecode"><span class="id" title="var">A</span>}</span>. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> The multiset: here, equivalence is <i>still</i> not unification. However, multiple instances of an item may appear in a multiset, which unification does take into account: <span class="inlinecode">{<span class="id" title="var">A</span>,</span> <span class="inlinecode"><span class="id" title="var">B</span>}</span> <span class="inlinecode">/=</span> <span class="inlinecode">{<span class="id" title="var">A</span>,</span> <span class="inlinecode"><span class="id" title="var">A</span>,</span> <span class="inlinecode"><span class="id" title="var">B</span>}</span>. Gallier's reference work, cited below, uses this feature in a more featureful logic, Girard's linear logic, where a class of assumptions can be used once (and only once.) We don't necessarily want to deal with duplicates in our logic, but it turns out to make for a conveniently-available datatype. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> The list, where equivalence is unification. But now we need some other way, on a level other than the datatype, of sanctioning the reordering of assumptions. We choose to add rules them on the level of the proof system. Here, "structural" inference rules for <span class="inlinecode"><span class="id" title="var">Permutation</span></span> encode permutation. What about duplication or removal ("cut"), which we should also be free to do? We add separate rules for those, too. (These rules are given by Wadler, cited below.) | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| So we use the last representation. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| <a name="lab6"></a><h2 class="section">What distinguishes natural deduction from the sequent calculus?</h2> | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> A natural deduction turnstile <span class="inlinecode">|-</span> can only have one conclusion; a sequent calculus deducution can have a disjunction of conclusions: the logical or of many propositions. Unfortunately the propositional logic doesn't have a logical <span class="inlinecode">∨</span> to interact with the metalogical <span class="inlinecode">∨</span>, and in fact we can remove it out of our formalisation. But we won't - this difference counterbalances another. And read Wadler's <i>Call-by-Value is dual to Call-by-Name</i>: as both logics grow, this core difference pushes their development in entirely different directions. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> For each connective (and here we only have <span class="inlinecode">→</span>), each proof system provides qualitatively different rules. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> Rules in natural deduction describe transformations that go strictly from the left to the right of a <span class="inlinecode">|-</span>. Rules in the sequent calculus occur in pairs, each sticking to one side of the turnstile: we have a <span class="inlinecode"><span class="id" title="var">S_Impl_L</span></span> rule and a <span class="inlinecode"><span class="id" title="var">S_Impl_R</span></span> rules that respectively work on the left and the right. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> Rules in natural deduction occur in pairs, corresponding to introduction and elimination (or constructor and accessor). In the sequent calculus, we only have construction rules. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> The sequent calculus has a <span class="inlinecode"><span class="id" title="var">S_Cut</span></span> rule; natural deduction does not. Gallier (cited below) notes that this isn't required for propositional logic. In more full-featured logics, though, a Cut rule is required to to show the consistency of the sequent calculus! (This due to Wadler.) | |
| </li> | |
| </ul> | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| We find out that each comparison turns out asymmetrically: either natural deduction has a pair of rules, and the sequent calculus does not, or vice-versa. And then, curiously enough, once all the comparisons are taking into account the asymmetries balance out. Are these systems somehow duals - two sides of a symmetry? I don't have a meaningful conclusion there. | |
| <div class="paragraph"> </div> | |
| Another question to ask: how do these asymmetries end up preserving the "equivalence" of both the systems? We'll delay the answer for a bit. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> These asymmetries end up distinguishing the style of deductions done in each proof system. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> A consequence of the first comparison: a user of natural deduction looks at propositions on the left of the <span class="inlinecode">|-</span> in order to construct propositions on the right of the <span class="inlinecode">|-</span>. A user of the sequent calculus must stick on one side: looking at propositions on the left, creating propositions on the left; and vice-versa. | |
| <div class="paragraph"> </div> | |
| </li> | |
| <li> And of the second. A user of natural deduction can both create and take apart connectives. A user of the sequent calculus can only create them! | |
| </li> | |
| </ul> | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| The apparent missing features of each system balance each other out: a user of a sequent calculus can only create <span class="inlinecode">→</span>s, but he can do so in order to create an assumption or a conclusion. A user of the natural deduction can either create or destroy a <span class="inlinecode">→</span>, but he can only do so to create a conclusion. | |
| <div class="paragraph"> </div> | |
| Back to the question: are the systems equivalent in power? Yes - Gentzen has shown it; this result was used to show that natural deduction could be translated into the sequent calculus (and vice-versa), and so that both systems were either consistent or inconsistent together. (See Wadler for more.) | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">N_cooccurrence_is_implication</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :: <span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>) ]- (<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span>).<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">N_Id</span> (<span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) <span class="id" title="var">B</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Interchange</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>; <span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Impl_intro</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Thinning</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">S_cooccurrence_is_implication</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span> :: <span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>) }- (<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>).<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">S_Id</span> <span class="id" title="var">nil</span> <span class="id" title="var">nil</span> <span class="id" title="var">B</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Thinning_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Impl_R</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Thinning_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">N_modus_ponens</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) ]- <span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">N_Id</span> <span class="id" title="var">nil</span> <span class="id" title="var">A</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">N_Id</span> <span class="id" title="var">nil</span> (<span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">Q</span>.<br/> | |
| <span class="id" title="tactic">eapply</span> <span class="id" title="var">N_Impl_elim</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Interchange</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Thinning</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">Q</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">N_Thinning</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">S_modus_ponens</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>),<br/> | |
| (<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) }- (<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>).<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Impl_L</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Interchange_R</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">M</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Thinning_R</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Id</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">A</span>).<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Interchange_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Thinning_L</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">S_Id</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">B</span>).<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| Note how awkward it is in Coq's tactic language to build a proof term by first giving smaller statements, and then constructing larger ones from them. Simultaneously, note how much easier it is to do the opposite: give a single large statement, and then fill in its arguments: Coq will allow you to give the arguments as late as you like, representing the obligation to do so as subgoals. | |
| <div class="paragraph"> </div> | |
| The relevant proof-theoretic distinction to make here is between forward and backward proof: forwards - syntactically - from smaller bindings into the expression in tail form; backwards from statements into subgoals. We say that Coq assists backwards proof more than it does forward proof. | |
| <div class="paragraph"> </div> | |
| Forwards proof in Coq requires working with local bindings. The tactics <span class="inlinecode"><span class="id" title="tactic">pose</span></span> and <span class="inlinecode"><span class="id" title="var">remember</span></span> then become useful - but they require you to give their values at once. You can't delay giving them by turning them into subgoals; you can't use unification to infer implicit (curly-bracketed) arguments, either. Unless you use the tactic <span class="inlinecode"><span class="id" title="tactic">assert</span></span>: but this requires you immediately give the type of the term instead. | |
| <div class="paragraph"> </div> | |
| <div class="paragraph"> </div> | |
| <a name="lab7"></a><h1 class="section">Adding a language of proof onto a language of propositions, by Curry-Howard</h1> | |
| <div class="paragraph"> </div> | |
| It's hard to introduce just one link the Curry-Howard correspondence makes, and then use that alone to justify the Correspondence. So we'll introduce many of them as once, glossing them as required. We have | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> propositions as types (<span class="inlinecode"><span class="id" title="var">A</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" title="var">B</span></span>, the function, is <span class="inlinecode"><span class="id" title="var">A</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" title="var">B</span></span>, <span class="inlinecode"><span class="id" title="var">A</span></span> implying <span class="inlinecode"><span class="id" title="var">B</span></span>); | |
| </li> | |
| <li> proof terms as terms in a computational calculus - in this case, the λ-calculus. | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| We when talk about "terms", we talk about the elements of the one language that acts both as proof language and computational language. Both "proof language" and "computational language" will be used interchangeably. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> the type-of relation binding proof terms to their propositions in inference rules (equally, terms to their types in typing rules); | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| Hang in there - but what is a proof term? It is how we give, in the logic itself, proof for logical statements in the logic. Up until now we have given them in the <i>metalogic</i>: a Coq proof is a Coq function. So our propositional logic must rely on the metalogic for its proofs - until we introduce a proof language native to the logic itself. | |
| <div class="paragraph"> </div> | |
| <span class="inlinecode"><span class="id" title="var">NT_cooccurrence_is_implication</span></span>, defined below, is a metalogical proof (like the rest of the proofs here) for a metalogical proposition. Here is its proof term: | |
| <div class="paragraph"> </div> | |
| <pre> | |
| Coq => Print NT_cooccurrence_is_implication. | |
| -------------------------------------------- | |
| NT_cooccurrence_is_implication : | |
| forall (A B:prop) (a:id) (b:term), | |
| (Var a:A :: b:B :: nil) ]= (\a->b:A => B) | |
| = | |
| fun (A B : prop) (a : id) (b : term) => | |
| let P := NT_Id ((Var a : A) :+ nil) (b : B) in | |
| (fun P0 : nil +: Var a : A +: b : B ]= b : B => | |
| (fun P1 : (b : B) :+ nil ]= \ a -> b : A => B => | |
| (fun P2 : (Var a : A) :+ (b : B) :+ nil ]= \ a -> b : A => B => P2) | |
| (NT_Thinning ((b : B) :+ nil) (Var a : A) (\ a -> b : A => B) P1)) | |
| (NT_Impl_intro ((b : B) :+ nil) A B a b P0)) | |
| (NT_Interchange nil nil (b : B) (Var a : A) (b : B) P) | |
| : forall (A B : prop) (a : id) (b : term), | |
| (Var a : A) :+ (b : B) :+ nil ]= \ a -> b : A => B | |
| </pre> | |
| <div class="paragraph"> </div> | |
| But read the metalogical proposition more closely: it proposes the correctness of a logical proof. What is the logical proof term? Metalogically assuming <span class="inlinecode"><span class="id" title="var">Var</span></span> <span class="inlinecode"><span class="id" title="var">a</span>:</span> <span class="inlinecode"><span class="id" title="var">A</span></span> and <span class="inlinecode"><span class="id" title="var">b</span>:</span> <span class="inlinecode"><span class="id" title="var">B</span></span>, it is <span class="inlinecode">\<span class="id" title="var">a</span>→<span class="id" title="var">b</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">A</span>⇒<span class="id" title="var">B</span></span>, the logic-level proof term. (More on how a λ-calculus term can be a proof below.) We no longer have to prove things in the metalogic! It's scandalous: up until now, instead of giving (logical) proof, we've instead just had to give (metalogical) proof that a (logical) proof was possible! But now we're giving (metalogical) proof that a certain (logical) proof is correct. | |
| <div class="paragraph"> </div> | |
| Now that we know what a proof term is, we further complete the analogy. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li>type checking is proof checking, and | |
| </li> | |
| <li> term evaluation corresponds - to what? To a process called proof normalisation, defined so as to simplify proof terms. And isn't evaluation itself a well-defined form of simplification? | |
| </li> | |
| </ul> | |
| A sidenote: note that term evaluation is sometimes formalised as term <i>normalisation</i>, a relation mapping terms into a a subset of "normal forms". A text like Peirce et al.'s <i>Software Foundations</i> covers this in the gory detail required for Coq. | |
| <div class="paragraph"> </div> | |
| Also note that proof normalisation turns statements on the set of proofs into a statement on a far smaller set: the set of normalised proofs. (Due to Gallier.) This technique helps Gentzen as he shows the consistency of the sequent calculus, and by equivalence natural deduction. (Due to Wadler.) | |
| <div class="paragraph"> </div> | |
| <a name="lab8"></a><h2 class="section">The term language, and typing the term language - or the proof language, and the proofs of a proposition</h2> | |
| <div class="paragraph"> </div> | |
| Now let's encode the concepts introduced above - proof language, the type-of (or is-proof-of) relation, and so on - in the metalogic that is Coq. | |
| <div class="paragraph"> </div> | |
| The type-of relation becomes, in the metalogic, a proposition. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">typing</span> {<span class="id" title="var">proof</span>:<span class="id" title="keyword">Set</span>} : <span class="id" title="keyword">Set</span> :=<br/> | |
| | <span class="id" title="var">GiveType</span> : <span class="id" title="var">proof</span> → <span class="id" title="var">prop</span> → <span class="id" title="var">typing</span>.<br/> | |
| <span class="id" title="keyword">Notation</span> "a : A" := (<span class="id" title="var">GiveType</span> <span class="id" title="var">a</span> <span class="id" title="var">A</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 57).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| Variable identifiers are a type of their own. (The opaqueness declaration prevents Coq from evaluating <span class="inlinecode"><span class="id" title="var">id</span></span> to <span class="inlinecode"><span class="id" title="var">string</span></span>. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Definition</span> <span class="id" title="var">id</span> : <span class="id" title="keyword">Set</span> := <span class="id" title="var">string</span>.<br/> | |
| <span class="id" title="keyword">Opaque</span> <span class="id" title="var">id</span>.<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| Now the computational language - or the proof language. | |
| <div class="paragraph"> </div> | |
| Note that one proof language suffices for both proof systems, natural deduction and the sequent calculus. This language is - when given with its "usual" type system - the simply-typed λ-calculus. It seems the type language heavily determines the term language. | |
| <div class="paragraph"> </div> | |
| Could it be that the type language is <i>sufficient</i> to determine the term language? This is true when we think of the term language as a proof language, but clearly not as a computational language, or a language to code in the large with. Conversely, it can hint at us how to simplify a language: both Haskell and OCaml inherit the features that simplify them (expression-orientation, parametric polymorphism, type inference) from their ancestor language ML - a Meta-Language built to express metalogical proofs of features of languages. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">term</span> : <span class="id" title="keyword">Set</span> :=<br/> | |
| | <span class="id" title="var">Var</span> : <span class="id" title="var">id</span> → <span class="id" title="var">term</span><br/> | |
| | <span class="id" title="var">Lam</span> : <span class="id" title="var">id</span> → <span class="id" title="var">term</span> → <span class="id" title="var">term</span><br/> | |
| | <span class="id" title="var">App</span> : <span class="id" title="var">term</span> → <span class="id" title="var">term</span> → <span class="id" title="var">term</span>.<br/> | |
| <span class="id" title="keyword">Notation</span> "\ x -> a" := (<span class="id" title="var">Lam</span> <span class="id" title="var">x</span> <span class="id" title="var">a</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 44, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 44).<br/> | |
| <span class="id" title="keyword">Notation</span> "f @ a" := (<span class="id" title="var">App</span> <span class="id" title="var">f</span> <span class="id" title="var">a</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 44, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/> | |
| <br/> | |
| <span class="id" title="keyword">Definition</span> <span class="id" title="var">tterm</span> : <span class="id" title="keyword">Set</span> := <span class="id" title="var">typing</span> (<span class="id" title="var">proof</span>:=<span class="id" title="var">term</span>).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| Finally, we give the same proof systems above. But now note how, as they manipulate propositions, they simultaneously manipulate proof terms attached with a <span class="inlinecode">:</span> to propositions - more on proof term manipulation below... | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Reserved Notation</span> "A ]= B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90).<br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">NatDedTypings</span> : <span class="id" title="var">list</span> <span class="id" title="var">tterm</span> → <span class="id" title="var">tterm</span> → <span class="id" title="keyword">Prop</span> :=<br/> | |
| | <span class="id" title="var">NT_Id</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]= <span class="id" title="var">A</span>)<br/> | |
| | <span class="id" title="var">NT_Impl_intro</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">a</span>:<span class="id" title="var">id</span>) (<span class="id" title="var">b</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]= <span class="id" title="var">b</span> : <span class="id" title="var">B</span> ) →<br/> | |
| ( <span class="id" title="var">L</span> ]= \<span class="id" title="var">a</span>→<span class="id" title="var">b</span> : <span class="id" title="var">A</span>⇒<span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">NT_Impl_elim</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">f</span> <span class="id" title="var">a</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">L</span> ]= <span class="id" title="var">f</span> : <span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span>) → (<span class="id" title="var">L</span> ]= <span class="id" title="var">a</span> : <span class="id" title="var">A</span>) →<br/> | |
| (<span class="id" title="var">L</span> ]= <span class="id" title="var">f@a</span> : <span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">NT_Interchange</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">A</span> ++ <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> ]= <span class="id" title="var">C</span>) →<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">B</span> ++ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span> ]= <span class="id" title="var">C</span>)<br/> | |
| | <span class="id" title="var">NT_Thinning</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> ]= <span class="id" title="var">B</span>) →<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]= <span class="id" title="var">B</span>)<br/> | |
| | <span class="id" title="var">NT_Contraction</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]= <span class="id" title="var">B</span>) →<br/> | |
| ( <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> ]= <span class="id" title="var">B</span>)<br/> | |
| <span class="id" title="keyword">where</span> "A ]= B" := (<span class="id" title="var">NatDedTypings</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>).<br/> | |
| <br/> | |
| <span class="id" title="keyword">Reserved Notation</span> "A }= B" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90).<br/> | |
| <span class="id" title="keyword">Inductive</span> <span class="id" title="var">SequentTypings</span> : <span class="id" title="var">list</span> <span class="id" title="var">tterm</span> → <span class="id" title="var">list</span> <span class="id" title="var">tterm</span> → <span class="id" title="keyword">Prop</span> :=<br/> | |
| | <span class="id" title="var">ST_Id</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Impl_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">a</span> <span class="id" title="var">f</span>: <span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">f@a</span>:<span class="id" title="var">B</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">f</span>:<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Impl_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">a</span> <span class="id" title="var">f</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">a</span>:<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">f@a</span> : <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> ) →<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">f</span> : <span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> )<br/> | |
| | <span class="id" title="var">ST_Interchange_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">A</span> ++ <span class="id" title="var">B</span> :+ <span class="id" title="var">M</span> }= <span class="id" title="var">N</span>) →<br/> | |
| (<span class="id" title="var">L</span> +: <span class="id" title="var">B</span> ++ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span> }= <span class="id" title="var">N</span>)<br/> | |
| | <span class="id" title="var">ST_Interchange_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">M</span> ++ <span class="id" title="var">A</span> :: <span class="id" title="var">B</span> :+ <span class="id" title="var">N</span>) →<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">M</span> ++ <span class="id" title="var">B</span> :: <span class="id" title="var">A</span> :+ <span class="id" title="var">N</span>)<br/> | |
| | <span class="id" title="var">ST_Thinning_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Thinning_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Contraction_L</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>) →<br/> | |
| ( <span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Contraction_R</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">A</span> :+ <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>) →<br/> | |
| (<span class="id" title="var">L</span> }= <span class="id" title="var">A</span> :+ <span class="id" title="var">M</span>)<br/> | |
| | <span class="id" title="var">ST_Cut</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">L</span> <span class="id" title="var">M</span> <span class="id" title="var">N</span> <span class="id" title="var">O</span>:<span class="id" title="var">list</span> <span class="id" title="var">tterm</span>) (<span class="id" title="var">A</span>:<span class="id" title="var">tterm</span>),<br/> | |
| (<span class="id" title="var">A</span> :+ <span class="id" title="var">L</span> }= <span class="id" title="var">M</span>) → (<span class="id" title="var">N</span> }= <span class="id" title="var">A</span> :+ <span class="id" title="var">O</span>) →<br/> | |
| (<span class="id" title="var">L</span> ++ <span class="id" title="var">N</span> }= <span class="id" title="var">M</span> ++ <span class="id" title="var">O</span>)<br/> | |
| <span class="id" title="keyword">where</span> "A }= B" := (<span class="id" title="var">SequentTypings</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span>).<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| A side note: <span class="inlinecode"><span class="id" title="var">ST_Impl_</span></span>L was once defined as | |
| <div class="paragraph"> </div> | |
| <pre> | |
| | ST_Impl_L : forall (L M:list tterm) (A B:prop) (a:id) (b:term), | |
| (L }= Var a:A :+ M) -> | |
| ( b:B :+ L }= M) -> | |
| (\a->b : A=>B :+ L }= M) | |
| </pre> | |
| <div class="paragraph"> </div> | |
| <span class="inlinecode"><span class="id" title="var">ST_Impl_R</span></span> was, too, defined analogously. | |
| <div class="paragraph"> </div> | |
| This is a plausible rule, but it didn't make the proof below of <span class="inlinecode"><span class="id" title="var">ST_modus_ponens</span></span> go through without substantial changes: <span class="inlinecode"><span class="id" title="var">ST_Impl_L</span></span> couldn't be used at the same point it was used when showing <span class="inlinecode"><span class="id" title="var">S_modus_ponens</span></span>. So we conclude: metalogical proofs of a logical proposition shouldn't change in order to give logical proofs of the same proposition! | |
| <div class="paragraph"> </div> | |
| <a name="lab9"></a><h2 class="section">Using the proof systems to give proofs</h2> | |
| <div class="paragraph"> </div> | |
| We promised above to clarify how terms in the λ-calculus can be interpreted as proofs. There is, in fact, a canonical interpretation of this process - the Brouwer-Heyting-Kolgomorov interpretation of a constructive proof of a proposition: for the conjunction of two propositions, give a proof for both of them, and so on... | |
| <div class="paragraph"> </div> | |
| This interpretation is, more precisely, given for intuitionistic logic. It is a superset of our propositional logic, adding extra connectives (logical <span class="inlinecode">∧</span>, and so on) and extra reasoning principles (a representation of falsity, and an axiom encoding the principle of explosion). See Gallier cited below for further details. But we assume the interpretation doesn't go astray for propositional logic (without giving formal proof of this), since all statements that can be proved in the propositional logic can be proved in intuitionistic logic as well. The contrapositive clearly is true as well - if something can't be proved in intuitionistic logic, it can't be shown in propositional logic., either. | |
| <div class="paragraph"> </div> | |
| The exact sequence inference rules we use to deduce these propositions remain the same - not surprising, since the inference rules themselves have remained the same, rule for rule! We've only just changed uses of the type <span class="inlinecode"><span class="id" title="var">prop</span></span> to the type <span class="inlinecode"><span class="id" title="var">tterm</span></span>. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">NT_cooccurrence_is_implication</span> : <br/> | |
| <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">a</span>:<span class="id" title="var">id</span>) (<span class="id" title="var">b</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :: <span class="id" title="var">b</span>:<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>) ]= (\<span class="id" title="var">a</span>→<span class="id" title="var">b</span>:<span class="id" title="var">A</span> ⇒ <span class="id" title="var">B</span>).<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">NT_Id</span> (<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) (<span class="id" title="var">b</span>:<span class="id" title="var">B</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Interchange</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>; <span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Impl_intro</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Thinning</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| As we proceed through the steps of the metalogical proof, we find that we're slowly building up a logic-level program to the left of the <span class="inlinecode">:</span>. By the time we reach the <span class="inlinecode"><span class="id" title="keyword">Qed</span></span>, the program is not only finished, but type-correct given the assumed typings to the left of the turnstile. So we add one more Curry-Howard consequence: | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> proof term derivations are program transformations. | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| As we've said in an earlier preview: here, the program we've derived in our natural-deduction system is given in the type. It is <span class="inlinecode">\<span class="id" title="var">a</span>→<span class="id" title="var">b</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">A</span>⇒<span class="id" title="var">B</span></span>, having metalogically assumed <span class="inlinecode"><span class="id" title="var">Var</span></span> <span class="inlinecode"><span class="id" title="var">a</span>:<span class="id" title="var">A</span></span> and <span class="inlinecode"><span class="id" title="var">b</span>:<span class="id" title="var">B</span></span>. | |
| <div class="paragraph"> </div> | |
| Here are the rest of the proofs, equivalent to the ones given for the proofless proof systems. | |
| </div> | |
| <div class="code"> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">ST_cooccurrence_is_implication</span> :<br/> | |
| <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">a</span>:<span class="id" title="var">id</span>) (<span class="id" title="var">b</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :: <span class="id" title="var">b</span>:<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>) }= (\<span class="id" title="var">a</span>→<span class="id" title="var">b</span>:<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>).<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">ST_Id</span> <span class="id" title="var">nil</span> <span class="id" title="var">nil</span> (<span class="id" title="var">b</span>:<span class="id" title="var">B</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Thinning_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Impl_R</span> <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Thinning_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">A</span>:=<span class="id" title="var">Var</span> <span class="id" title="var">a</span>:<span class="id" title="var">A</span>) <span class="id" title="keyword">in</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">NT_modus_ponens</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">f</span> <span class="id" title="var">a</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">f</span>:<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) ]= <span class="id" title="var">f@a</span>:<span class="id" title="var">B</span>.<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">f</span> <span class="id" title="var">a</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">NT_Id</span> <span class="id" title="var">nil</span> (<span class="id" title="var">a</span>:<span class="id" title="var">A</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="tactic">pose</span> (<span class="id" title="var">NT_Id</span> <span class="id" title="var">nil</span> (<span class="id" title="var">f</span>: <span class="id" title="var">A</span>⇒<span class="id" title="var">B</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">Q</span>.<br/> | |
| <span class="id" title="tactic">eapply</span> <span class="id" title="var">NT_Impl_elim</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Interchange</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Thinning</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">Q</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">NT_Thinning</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">P</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| <span class="id" title="keyword">Lemma</span> <span class="id" title="var">ST_modus_ponens</span> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="var">prop</span>) (<span class="id" title="var">f</span> <span class="id" title="var">a</span>:<span class="id" title="var">term</span>),<br/> | |
| (<span class="id" title="var">f</span>:<span class="id" title="var">A</span>⇒<span class="id" title="var">B</span> :: <span class="id" title="var">a</span>:<span class="id" title="var">A</span> :: <span class="id" title="var">nil</span>) }= <span class="id" title="var">f@a</span>:<span class="id" title="var">B</span> :: <span class="id" title="var">nil</span>.<br/> | |
| <span class="id" title="keyword">Proof</span>.<br/> | |
| <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">f</span> <span class="id" title="var">a</span>.<br/> | |
| <span class="id" title="keyword">Print</span> <span class="id" title="var">ST_Impl_L</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Impl_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">a</span>:=<span class="id" title="var">a</span>).<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Interchange_R</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">M</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Thinning_R</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Id</span>.<br/> | |
| - <br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Interchange_L</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">L</span>:=<span class="id" title="var">nil</span>); <span class="id" title="tactic">simpl</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Thinning_L</span>.<br/> | |
| <span class="id" title="tactic">apply</span> <span class="id" title="var">ST_Id</span>.<br/> | |
| <span class="id" title="keyword">Qed</span>.<br/> | |
| <br/> | |
| </div> | |
| <div class="doc"> | |
| <div class="paragraph"> </div> | |
| That should be the end of the taster - short, but broad and precise. | |
| <div class="paragraph"> </div> | |
| A final parting note - we take the ability to use the metalogic to check logic-level proofs for granted. But - | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> This comes at the cost of spelling out our proofs in painful detail. | |
| </li> | |
| <li> Clearly the vast majority of proofs aren't checked in any metalogic, and can't immediately be converted in a checkable form: they are given at a more abstract level. ("Proposition: if <span class="inlinecode"><span class="id" title="var">a</span>:<span class="id" title="var">A</span></span>, <span class="inlinecode"><span class="id" title="tactic">eval</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">A</span></span>. Proof. By induction on terms of the language; the induction hypothesis is only used in the cases where...") | |
| </li> | |
| <li> And who checks the metalogic's proofs, anyhow? | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| <a name="lab10"></a><h2 class="section">Credits</h2> | |
| <div class="paragraph"> </div> | |
| I knit together a few observations in this work. None of them are mine. | |
| <div class="paragraph"> </div> | |
| Some of the ideas used above are considered standard. (The named ones clearly are.) For these ideas the citations given below are references, rather than introductions, to them. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> The sequent calculus as an alternative to natural deduction. | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| I originally learned of this from Wadler's <i>Call-by-Value is Dual to Call-by-Name</i>: it shows what Gentzen "designed" both proof systems for, and what he was able to do with either of both systems. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> Sometimes you get a language from its typing rules | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| Staring at the typing rules in order to define your computational language is a process I learned from Gallier's <i>Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi</i>. (I've never found a Part II.) It deals with logics up to intuitionistic logic, and gives the corresponding lambda-calculi as increase with complexity. | |
| <div class="paragraph"> </div> | |
| After reaching that point, he changes to focus instead on proof theoretic results - a pity, since the real excitement starts when you try to identify calculi for classical logic (Peirce's law as <span class="inlinecode"><span class="id" title="var">call</span>/<span class="id" title="var">cc</span></span>), or for linear logic, for example. A series of lecture notes by Frank Pfennig et al. outlines this process, but I've lost the reference. | |
| <div class="paragraph"> </div> | |
| <ul class="doclist"> | |
| <li> If your lists of assumptions are lists, rather than sets, you'll have to give permutation rules in the proof system. | |
| </li> | |
| </ul> | |
| <div class="paragraph"> </div> | |
| Due to Wadler's paper above, again. Gallier uses multisets without giving a good technical description of them. | |
| <div class="paragraph"> </div> | |
| </div> | |
| <hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> | |
| </div> | |
| </div> | |
| </body> | |
| </html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment