12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Friday May 03, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 18:46, 27 March 2009
, 18:46, 27 March 2009→Conjunction Calculus: markup
===Conjunction Calculus===
===Conjunction Calculus===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
| A 'conjunction calculus' is a deductive system dealing with truth and
|
|
<p>A ''conjunction calculus'' is a deductive system dealing with truth and conjunction. Thus we assume that there is given a formula <math>\operatorname{T}</math> ( = true) and a binary operation <math>\land</math> ( = and) for forming the conjunction <math>A \land B</math> of two given formulas <math>A\!</math> and <math>B.\!</math> Moreover, we specify the following additional arrows and rules of inference:</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{R2.} & A \xrightarrow{~\bigcirc_A~} \operatorname{T};
\\[8pt]
\text{R3a.} & A \land B \xrightarrow{~\pi_{A, B}~} A,
\\[8pt]
\text{R3b.} & A \land B \xrightarrow{~\pi'_{A, B}~} B,
\\[8pt]
\text{R3c.} & \dfrac{C \xrightarrow{~f~} A \quad C \xrightarrow{~g~} B}{C \xrightarrow{~\langle f, g \rangle~} A \land B}.
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 47–48).</p>
|}
| C --------> A & B
===Positive Intuitionistic Propositional Calculus===
===Positive Intuitionistic Propositional Calculus===
