Line 62: |
Line 62: |
| All of the axioms in this set have the form of equations. This means that all of the inference licensed by them are reversible. The proof annotation scheme employed below makes use of a double bar <math>\overline{\underline{~~~~~~}}</math> to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case. | | All of the axioms in this set have the form of equations. This means that all of the inference licensed by them are reversible. The proof annotation scheme employed below makes use of a double bar <math>\overline{\underline{~~~~~~}}</math> to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case. |
| | | |
− | Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the ''Entitative'' and the ''Existential'' interpretations, here referred to as "EN" and "EX", respectively. The early CSP, as in his essay on "Qualitative Logic", and also GSB, emphasized the EN interpretation, while the later CSP developed mostly the EX interpretation. | + | Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the ''Entitative'' and the ''Existential'' interpretations, here referred to as <math>\operatorname{En}</math> and <math>\operatorname{Ex},</math> respectively. The early CSP, as in his essay on "Qualitative Logic", and also GSB, emphasized the <math>\operatorname{En}</math> interpretation, while the later CSP developed mostly the <math>\operatorname{Ex}</math> interpretation. |
| | | |
| ===Frequently used theorems=== | | ===Frequently used theorems=== |
Line 907: |
Line 907: |
| |} | | |} |
| | | |
− | For the sake of simplicity in discussing this example, I will revert to the existential interpretation (''Ex'') of logical graphs and their corresponding parse strings. | + | For the sake of simplicity in discussing this example, I will revert to the existential interpretation (<math>\operatorname{Ex}</math>) of logical graphs and their corresponding parse strings. |
| | | |
− | Under ''Ex'' the expression <math>(p\ (q))(p\ (r))\!</math> interprets as the vernacular expression <math>p\ \operatorname{implies}\ q\ \operatorname{and}\ p\ \operatorname{implies}\ r,</math> in symbols, <math>\{ p \Rightarrow q \} \land \{ p \Rightarrow r \},</math> so this is the reading that we'll want to keep in mind for the present. | + | Under <math>\operatorname{Ex}</math> the expression <math>(p\ (q))(p\ (r))\!</math> interprets as the vernacular expression <math>p\ \operatorname{implies}\ q\ \operatorname{and}\ p\ \operatorname{implies}\ r,</math> in symbols, <math>\{ p \Rightarrow q \} \land \{ p \Rightarrow r \},</math> so this is the reading that we'll want to keep in mind for the present. |
| | | |
| Where brevity is required, and it occasionally is, we may invoke the propositional expression <math>(p\ (q))(p\ (r))\!</math> under the name of <math>f\!</math> by making use of the following definition: <math>f = (p\ (q))(p\ (r)).\!</math> | | Where brevity is required, and it occasionally is, we may invoke the propositional expression <math>(p\ (q))(p\ (r))\!</math> under the name of <math>f\!</math> by making use of the following definition: <math>f = (p\ (q))(p\ (r)).\!</math> |
Line 1,573: |
Line 1,573: |
| In other words, "p is equivalent to p and q and r". | | In other words, "p is equivalent to p and q and r". |
| | | |
− | Let's pause to refresh ourselves with a few morsels of lemmas bread. One lemma that I can see just far enough ahead to see our imminent need of is the principle that I canonize as the ''Emptiness Rule''. It says that a bare lobe expression like "(… , …)", with any number of places for arguments but nothing but blanks as filler, is logically tantamount to the proto-typical expression of its type, namely, the constant expression "( )" that ''Ex'' interprets as denoting the logical value ''false''. To depict the rule in graphical form, we have the continuing sequence of equations: | + | Let's pause to refresh ourselves with a few morsels of lemmas bread. One lemma that I can see just far enough ahead to see our imminent need of is the principle that I canonize as the ''Emptiness Rule''. It says that a bare lobe expression like "(… , …)", with any number of places for arguments but nothing but blanks as filler, is logically tantamount to the proto-typical expression of its type, namely, the constant expression "( )" that <math>\operatorname{Ex}</math> interprets as denoting the logical value ''false''. To depict the rule in graphical form, we have the continuing sequence of equations: |
| | | |
| {| align="center" cellpadding="10" style="text-align:center; width:90%" | | {| align="center" cellpadding="10" style="text-align:center; width:90%" |
Line 2,145: |
Line 2,145: |
| : ''e''<sub>5</sub> = "(( (p (q))(p (r)) , (p (q r)) ))" | | : ''e''<sub>5</sub> = "(( (p (q))(p (r)) , (p (q r)) ))" |
| | | |
− | Under ''Ex'' we have the following interpretations: | + | Under <math>\operatorname{Ex}</math> we have the following interpretations: |
| | | |
| : ''e''<sub>0</sub> expresses the logical constant "false" | | : ''e''<sub>0</sub> expresses the logical constant "false" |
Line 2,171: |
Line 2,171: |
| Proof 2 lit on by ''burning the candle at both ends'', changing ''e''<sub>2</sub> into a normal form that reduced to ''e''<sub>4</sub>, and changing ''e''<sub>3</sub> into a normal form that also reduced to ''e''<sub>4</sub>, in this way tethering ''e''<sub>2</sub> and ''e''<sub>3</sub> to a common stake. In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure. | | Proof 2 lit on by ''burning the candle at both ends'', changing ''e''<sub>2</sub> into a normal form that reduced to ''e''<sub>4</sub>, and changing ''e''<sub>3</sub> into a normal form that also reduced to ''e''<sub>4</sub>, in this way tethering ''e''<sub>2</sub> and ''e''<sub>3</sub> to a common stake. In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure. |
| | | |
− | Proof 3 took the path of reflection, expressing the met-equation between ''e''<sub>2</sub> and ''e''<sub>3</sub> in the naturalized equation ''e''<sub>5</sub>, then taking ''e''<sub>5</sub> as ''s''<sub>1</sub> and exchanging it by dint of value preserving steps for ''e''<sub>1</sub> as ''s''<sub>''n''</sub>. Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that ''Ex'' recognizes as the value ''true''. | + | Proof 3 took the path of reflection, expressing the met-equation between ''e''<sub>2</sub> and ''e''<sub>3</sub> in the naturalized equation ''e''<sub>5</sub>, then taking ''e''<sub>5</sub> as ''s''<sub>1</sub> and exchanging it by dint of value preserving steps for ''e''<sub>1</sub> as ''s''<sub>''n''</sub>. Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that <math>\operatorname{Ex}</math> recognizes as the value ''true''. |
| | | |
| Review: | | Review: |