12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 15:48, 27 March 2009
, 15:48, 27 March 2009→Deductive System 2: markup
===Deductive System 2===
===Deductive System 2===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''deductive system'' is a graph with a specified arrow</p>
| R1a. A -----> A,
|-
|
|
| and a binary operation on arrows ('composition')
<p><math>\text{R1a.} \quad A \xrightarrow{~1_A~} A,</math></p>
|-
|
|
| f g
<p>and a binary operation on arrows (''composition'')
|-
| R1b. ----------------------
|
| gf
<p><math>\text{R1b.} \quad \dfrac{A \xrightarrow{~f~} B \quad B \xrightarrow{~g~} C}
{A \xrightarrow{~gf~} C}.</math></p>
</pre>
|-
|
<p>(Lambek & Scott, 47).</p>
|}
===Conjunction Calculus===
===Conjunction Calculus===