MyWikiBiz, Author Your Legacy — Wednesday May 08, 2024
Jump to navigationJump to search
261 bytes added
, 23:54, 27 March 2009
Line 2,435: |
Line 2,435: |
| ===Intuitionistic Propositional Calculus=== | | ===Intuitionistic Propositional Calculus=== |
| | | |
− | <pre>
| + | {| align="center" cellpadding="8" width="90%" <!--QUOTE--> |
− | | An 'intuitionistic propositional calculus' is more than a | |
− | | positive one; it requires also falsehood and disjunction,
| |
− | | that is, a formula 'F' (= false) and an operation 'v' (= or)
| |
− | | on formulas, together with the following additional arrows:
| |
| | | | | |
− | | []_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, | + | |- |
| | | | | |
− | | k1_A,B
| + | <p><math>\begin{array}{ll} |
− | | R6a. A --------> A v B,
| + | \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> |
| + | |- |
| | | | | |
− | | k2_A,B
| + | <p>(Lambek & Scott, 49–50). |
− | | R6b. B --------> A v B,
| + | |} |
− | |
| |
− | | !z!^C_A,B
| |
− | | R6c. (C <= A) & (C <= B) -----------> C <= (A v B).
| |
− | </pre>
| |
| | | |
| ===Classical Propositional Calculus=== | | ===Classical Propositional Calculus=== |