12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 02:49, 27 March 2009
, 02:49, 27 March 2009→Deductive System: markup
===Deductive System===
===Deductive System===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''deductive system'' is a graph in which to each object <math>A\!</math> there is associated an arrow <math>1_A : A \to A,</math> the ''identity'' arrow, and to each pair of arrows <math>f : A \to B</math> and <math>g : B \to C</math> there is associated an arrow <math>gf : A \to C,</math> the ''composition'' of <math>f\!</math> with <math>g.\!</math> A logician may think of the objects as ''formulas'' and of the arrows as ''deductions'' or ''proofs'', hence of</p>
::<p><math>\begin{array}{c}
\underline{~ f : A \to B ~~~~~ g : B \to C ~}
\\
</pre>
gf : A \to C
\end{array}</math></p>
<p>as a ''rule of inference''.</p>
<p>(Lambek & Scott, 5).</p>
|}
===Category===
===Category===