Line 1: |
Line 1: |
| {{DISPLAYTITLE:Propositions As Types}} | | {{DISPLAYTITLE:Propositions As Types}} |
| | | |
− | ==Note 1== | + | ==Identity, or the Identifier== |
| + | |
| + | ===Step 1=== |
| | | |
| <pre> | | <pre> |
− | Identity, or the Identifier
| |
− |
| |
− | Step 1.
| |
− |
| |
| Given a syntactic specification (or paraphrastic definition): | | Given a syntactic specification (or paraphrastic definition): |
| | | |
Line 29: |
Line 27: |
| | | |
| and so K(KS) constitutes a syntactic algorithm for I. | | and so K(KS) constitutes a syntactic algorithm for I. |
| + | </pre> |
| | | |
− | Step 2. | + | ===Step 2=== |
| | | |
| + | <pre> |
| Assign types in the specification: | | Assign types in the specification: |
| | | |
Line 39: |
Line 39: |
| whose type, read as a proposition, is a theorem of | | whose type, read as a proposition, is a theorem of |
| intuitionistic propositional calculus. | | intuitionistic propositional calculus. |
| + | </pre> |
| | | |
− | Step 3 (optional). | + | ===Step 3 (Optional)=== |
| | | |
| + | <pre> |
| Check that A => A is a theorem of classical propositional calculus. | | Check that A => A is a theorem of classical propositional calculus. |
| | | |
Line 52: |
Line 54: |
| </pre> | | </pre> |
| | | |
− | ==Note 2== | + | ===Step 4=== |
| | | |
| <pre> | | <pre> |
− | Identity, or the Identifier (cont.)
| |
− |
| |
− | Step 4.
| |
− |
| |
| If we start from the parse tree of the term I in terms of | | If we start from the parse tree of the term I in terms of |
| the primitive combinators K and S, that is, the articulation | | the primitive combinators K and S, that is, the articulation |
Line 79: |
Line 77: |
| and to carry along the type information as we go, ending up with | | and to carry along the type information as we go, ending up with |
| a typed parse tree for I, tantamount to a proof tree for A => A. | | a typed parse tree for I, tantamount to a proof tree for A => A. |
− | </pre>
| |
− |
| |
− | ==Note 3==
| |
− |
| |
− | <pre>
| |
− | Identity, or the Identifier (cont.)
| |
− |
| |
− | Step 4 (cont.)
| |
| | | |
| Term Development: Contextual Definition ~~~> Combinator Construction | | Term Development: Contextual Definition ~~~> Combinator Construction |
Line 140: |
Line 130: |
| </pre> | | </pre> |
| | | |
− | ==Note 4== | + | ===Step 5=== |
| | | |
| <pre> | | <pre> |
Line 150: |
Line 140: |
| | causing me to leave out a few steps. | | | causing me to leave out a few steps. |
| | | |
− | 1. Identity, or the Identifier (cont.)
| + | Existential Graph Format, Application Triples with Structure Sharing. |
− | | |
− | Step 5.
| |
− | | |
− | Existential Graph Format, | |
− | Application Triples with | |
− | Structure Sharing. | |
| | | |
| Same development in Existential Graph notation. | | Same development in Existential Graph notation. |
Line 215: |
Line 199: |
| </pre> | | </pre> |
| | | |
− | ==Note 5== | + | ==Composition, or the Composer== |
| + | |
| + | ===Step 1.=== |
| | | |
| <pre> | | <pre> |
− | Composition, or the Composer
| |
− |
| |
− | Step 1.
| |
− |
| |
| Given a specification of the "composition combinator", | | Given a specification of the "composition combinator", |
| or the "composer" P, that has the following effects: | | or the "composer" P, that has the following effects: |
Line 244: |
Line 226: |
| </pre> | | </pre> |
| | | |
− | ==Note 6== | + | ===Step 2=== |
| | | |
| <pre> | | <pre> |
− | Composition, or the Composer (cont.)
| |
− |
| |
− | Step 2.
| |
− |
| |
| Assign types in the specification: | | Assign types in the specification: |
| | | |
Line 284: |
Line 262: |
| </pre> | | </pre> |
| | | |
− | ==Note 7== | + | ===Step 3 (Optional)=== |
| | | |
| <pre> | | <pre> |
− | Composition, or the Composer (cont.)
| |
− |
| |
− | Step 3 (optional).
| |
− |
| |
| Check that the propositional type of the composer P is a theorem | | Check that the propositional type of the composer P is a theorem |
| of classical propositional calculus, which is logically necessary | | of classical propositional calculus, which is logically necessary |
Line 385: |
Line 359: |
| </pre> | | </pre> |
| | | |
− | ==Note 8== | + | ===Step 4=== |
| | | |
| <pre> | | <pre> |
− | Composition, or the Composer (cont.)
| |
− |
| |
− | Step 4.
| |
− |
| |
| Repeat the development in Step 1, | | Repeat the development in Step 1, |
| but this time articulating the | | but this time articulating the |
Line 527: |
Line 497: |
| | | | | | | |
| o---------------------------------------------------------------------o | | o---------------------------------------------------------------------o |
− | </pre>
| |
− |
| |
− | ==Note 9==
| |
− |
| |
− | <pre>
| |
− | Composition, or the Composer (cont.)
| |
− |
| |
− | Step 4 (concl.)
| |
| | | |
| The foregoing development has taken us from the | | The foregoing development has taken us from the |
Line 559: |
Line 521: |
| </pre> | | </pre> |
| | | |
− | ==Note 10== | + | ===Step 5=== |
| | | |
| <pre> | | <pre> |
− | Composition, or the Composer (concl.)
| |
− |
| |
− | Step 5.
| |
− |
| |
| Rewrite the final proof tree in existential graph format: | | Rewrite the final proof tree in existential graph format: |
| | | |
Line 617: |
Line 575: |
| </pre> | | </pre> |
| | | |
− | ==Note 11== | + | ==Self-Documentation : Developmental Data Structures== |
| | | |
| <pre> | | <pre> |
− | Self-Documentation
| |
− |
| |
| Observation. Notice the "self-documenting" property | | Observation. Notice the "self-documenting" property |
| of proof developments in the existential graph format, | | of proof developments in the existential graph format, |
Line 672: |
Line 628: |
| | | | | | | |
| o-----------------------------------------------------------o | | o-----------------------------------------------------------o |
− | </pre>
| |
− |
| |
− | ==Note 12==
| |
− |
| |
− | <pre>
| |
− | Self-Documentation, Developmental Data Structures (cont.)
| |
| | | |
| Redo the entire development of the Composer in existential graph format: | | Redo the entire development of the Composer in existential graph format: |
Line 776: |
Line 726: |
| </pre> | | </pre> |
| | | |
− | ==Note 13== | + | ==Triadic Analogy : Analogy Between Two Triadic Relations== |
| | | |
| <pre> | | <pre> |
− | Triadic Analogy: Analogy Between a Couple of Three-Place Relations
| |
− |
| |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| | | | | | | |
Line 792: |
Line 740: |
| </pre> | | </pre> |
| | | |
− | ==Note 14== | + | ==Transposition, or the Transposer== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer
| |
− |
| |
| x(y(zT)) = y(xz) | | x(y(zT)) = y(xz) |
| | | |
Line 803: |
Line 749: |
| specification of how the operator is required to act | | specification of how the operator is required to act |
| on other symbols. | | on other symbols. |
| + | </pre> |
| | | |
− | Step 1. | + | ===Step 1=== |
| | | |
| Find a "pure interpretant" for T, that is, an equivalent term | | Find a "pure interpretant" for T, that is, an equivalent term |
Line 814: |
Line 761: |
| as a sequence of manipulations on formal identifiers, or on | | as a sequence of manipulations on formal identifiers, or on |
| symbols taken as objects in themselves. | | symbols taken as objects in themselves. |
− | </pre>
| |
− |
| |
− | ==Note 15==
| |
− |
| |
− | <pre>
| |
− | Transposition, or the Transposer (cont.)
| |
| | | |
| x(y(zT)) = y(xz) | | x(y(zT)) = y(xz) |
− |
| |
− | Step 1 (concl.)
| |
| | | |
| Observe that y(xz) matches (xy)(xz) on the right, | | Observe that y(xz) matches (xy)(xz) on the right, |
Line 883: |
Line 822: |
| </pre> | | </pre> |
| | | |
− | ==Note 16== | + | ===Step 2=== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 2.
| |
− |
| |
| Using the contextual definition of the transposer T, | | Using the contextual definition of the transposer T, |
| | | |
Line 931: |
Line 866: |
| </pre> | | </pre> |
| | | |
− | ==Note 17== | + | ===Step 3 (Optional)=== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 3 (optional).
| |
− |
| |
| At this juncture we might want to verify that the proposition corresponding | | At this juncture we might want to verify that the proposition corresponding |
| to the type of T is actually a theorem of classical propositional calculus. | | to the type of T is actually a theorem of classical propositional calculus. |
Line 998: |
Line 929: |
| </pre> | | </pre> |
| | | |
− | ==Note 18== | + | ===Step 4=== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 4.
| |
− |
| |
| The construction of the term T of the appropriate type in terms of the | | The construction of the term T of the appropriate type in terms of the |
| primitive typed combinators of the forms K and S is analogous to the | | primitive typed combinators of the forms K and S is analogous to the |
Line 1,020: |
Line 947: |
| denote whatever it is, the supposed object, that | | denote whatever it is, the supposed object, that |
| "(F((SK)S))", the occurrent sign, denotes. | | "(F((SK)S))", the occurrent sign, denotes. |
− | </pre>
| |
− |
| |
− | ==Note 19==
| |
− |
| |
− | <pre>
| |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 4 (cont.)
| |
| | | |
| Consider the following data: | | Consider the following data: |
Line 1,089: |
Line 1,008: |
| | | | | | | |
| o-----------------------------------------------------------o | | o-----------------------------------------------------------o |
− | </pre>
| |
− |
| |
− | ==Note 20==
| |
− |
| |
− | <pre>
| |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 4 (cont.)
| |
| | | |
| If this strategy is successful it suggests that the proof tree can | | If this strategy is successful it suggests that the proof tree can |
Line 1,110: |
Line 1,021: |
| to reconstruct the true embryology or living physiology | | to reconstruct the true embryology or living physiology |
| of discovery involved. | | of discovery involved. |
− | </pre>
| |
− |
| |
− | ==Note 21==
| |
− |
| |
− | <pre>
| |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 4 (concl.)
| |
| | | |
| Repeat the development in Step 1, | | Repeat the development in Step 1, |
Line 1,502: |
Line 1,405: |
| </pre> | | </pre> |
| | | |
− | ==Note 22== | + | ===Step 5=== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 5.
| |
− |
| |
| Rewrite the final proof tree in existential graph format, | | Rewrite the final proof tree in existential graph format, |
| implementing structure sharing among application triples | | implementing structure sharing among application triples |
Line 1,652: |
Line 1,551: |
| </pre> | | </pre> |
| | | |
− | ==Note 23== | + | ===Step 5 (Extended)=== |
| | | |
| <pre> | | <pre> |
− | Transposition, or the Transposer (cont.)
| |
− |
| |
− | Step 5 (extended).
| |
− |
| |
| Redo the development of the proof tree in existential graph format. | | Redo the development of the proof tree in existential graph format. |
| | | |