12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 20:10, 27 March 2009
, 20:10, 27 March 2009→Positive Intuitionistic Propositional Calculus: markup
===Positive Intuitionistic Propositional Calculus===
===Positive Intuitionistic Propositional Calculus===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
|
|
<p>A ''positive intuitionistic propositional calculus'' is a conjunction calculus with an additional binary operation <math>\Leftarrow</math> ( = if). Thus, if <math>A\!</math> and <math>B\!</math> are formulas, so are <math>\operatorname{T},</math> <math>A \land B,</math> and <math>A \Leftarrow B.</math> (Yes, most people write <math>B \Rightarrow A</math> instead.) We also specify the following new arrow and rule of inference.</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{R4a.} & (A \Leftarrow B) \land B \xrightarrow{~\varepsilon_{A, B}~} A,
\\[8pt]
\text{R4b.} & \dfrac{C \land B \xrightarrow{~h~} A}{C \xrightarrow{~h^*~} A \Leftarrow B}.
| C ----> A <= B
\end{array}</math></p>
|-
|
|
</pre>
<p>(Lambek & Scott, 48–49).</p>
|}
===Intuitionistic Propositional Calculus===
===Intuitionistic Propositional Calculus===