MyWikiBiz, Author Your Legacy — Wednesday October 29, 2025
Jump to navigationJump to search
28 bytes added
, 04:02, 12 July 2009
| Line 432: |
Line 432: |
| | Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic. This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How]. In another formulation it says that terms are to types as proofs are to propositions. See [LaS, 42–46] and [SeH] for a good discussion and further references. To anticipate the bearing of these issues on our immediate topic, Table 3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question. | | Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic. This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How]. In another formulation it says that terms are to types as proofs are to propositions. See [LaS, 42–46] and [SeH] for a good discussion and further references. To anticipate the bearing of these issues on our immediate topic, Table 3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question. |
| | | | |
| − | {| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%" | + | <br> |
| − | |+ '''Table 3. Analogy Between Real and Boolean Types''' | + | |
| − | |- style="background:ghostwhite" | + | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%" |
| − | ! <math>\mbox{Real Domain}\ \mathbb{R}</math>
| + | |+ <math>\text{Table 3.}~~\text{Analogy Between Real and Boolean Types}</math> |
| − | ! <math>\longleftrightarrow</math>
| + | |- style="background:#f0f0ff" |
| − | ! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>
| + | | <math>\text{Real Domain}~ \mathbb{R}</math> |
| | + | | <math>\longleftrightarrow</math> |
| | + | | <math>\text{Boolean Domain}~ \mathbb{B}</math> |
| | |- | | |- |
| | | <math>\mathbb{R}^n</math> | | | <math>\mathbb{R}^n</math> |
| Line 478: |
Line 480: |
| | <p><math>\mbox{Transformation}\!</math></p> | | <p><math>\mbox{Transformation}\!</math></p> |
| | | <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math> | | | <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math> |
| − | |}<br> | + | |} |
| | + | |
| | + | <br> |
| | | | |
| | The Table exhibits a sample of likely parallels between the real and boolean domains. The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table. These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that pursue their courses through the states of an arbitrary space <math>X.\!</math> Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task. | | The Table exhibits a sample of likely parallels between the real and boolean domains. The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table. These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that pursue their courses through the states of an arbitrary space <math>X.\!</math> Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task. |