12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday May 04, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:58, 27 March 2009
, 12:58, 27 March 2009→Deductive System: spacing
|
|
<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>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}
::<p><math>\begin{array}{c}
\underline{~ f : A \to B ~~~~~ g : B \to C ~}
\underline{~ f : A \to B ~~~~~ g : B \to C ~}
gf : A \to C
gf : A \to C
\end{array}</math></p>
\end{array}</math></p>
|-
|
<p>as a ''rule of inference''.</p>
<p>as a ''rule of inference''.</p>
