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 23:54, 27 March 2009
, 23:54, 27 March 2009→Intuitionistic Propositional Calculus: markup
===Intuitionistic Propositional Calculus===
===Intuitionistic Propositional Calculus===
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
| An 'intuitionistic propositional calculus' is more than a
|
|
<p>An ''intuitionistic propositional calculus'' is more than a positive one; it requires also falsehood and disjunction, that is, a formula <math>\bot</math> ( = false) and an operation <math>\lor</math> ( = or) on formulas, together with the following additional arrows:</p>
| R5. F ------> A,
|-
|
|
<p><math>\begin{array}{ll}
\text{R5.} & \bot ~\xrightarrow{~\Box_A~}~ A;
\\[8pt]
\text{R6a.} & A ~\xrightarrow{~\kappa_{A, B}~}~ A \lor B,
\\[8pt]
\text{R6b.} & B ~\xrightarrow{~\kappa'_{A, B}~}~ A \lor B,
\\[8pt]
\text{R6c.} & (C \Leftarrow A) \land (C \Leftarrow B) ~\xrightarrow{~\zeta^C_{A, B}~}~ C \Leftarrow (A \lor B).
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 49–50).
|}
===Classical Propositional Calculus===
===Classical Propositional Calculus===
