12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Monday November 25, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Futures Of Logical Graphs (view source)
Revision as of 01:40, 22 August 2009
, 01:40, 22 August 2009→Analyzing contingent truths: convert graphics
The cactus language syntax also improves the ''reflective capacities'' of the logical calculus, in particular, it facilitates our ability to use the calculus to reflect on the process of proof, that is, the process of establishing equivalences between expressions.
The cactus language syntax also improves the ''reflective capacities'' of the logical calculus, in particular, it facilitates our ability to use the calculus to reflect on the process of proof, that is, the process of establishing equivalences between expressions.
==Analyzing contingent truths==
==Analysis of contingent propositions==
For all of the reasons mentioned above, and for the sake of a more compact illustration of the in and outs of a typical ''propositional equation reasoning system'' (PERS), let's now take up a much simpler example of a contingent proposition:
For all of the reasons mentioned above, and for the sake of a more compact illustration of the ins and outs of a typical propositional equation reasoning system, let's now take up a much simpler example of a contingent proposition:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
| [[Image:Logical Graph (P (Q)) (P (R)).jpg|500px]] || (26)
| |
|}
|}
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.
For the sake of simplicity in discussing this example, let's stick with the existential interpretation (<math>\operatorname{Ex}</math>) of logical graphs and their corresponding parse strings. Under <math>\operatorname{Ex}</math> the formal expression <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math> translates into the vernacular expression <math>{}^{\backprime\backprime} p ~\operatorname{implies}~ q ~\operatorname{and}~ p ~\operatorname{implies}~ r {}^{\prime\prime},</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, we may refer to the propositional expression <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math> under the name <math>f\!</math> by making use of the following definition:
{| align="center" cellpadding="8"
| <math>f ~=~ \texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math>
|}
Since the expression "(p (q))(p (r))" involves just three variables, it may be worth the trouble to draw a venn diagram of the situation. There are in fact a couple of different ways to execute the picture.
Since the expression <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math> involves just three variables, it may be worth the trouble to draw a venn diagram of the situation. There are in fact two different ways to execute the picture.
Figure 1 indicates the points of the universe of discourse ''X'' for which the proposition ''f'' : ''X'' → '''B''' has the value 1 (= true). In this "paint by numbers" style of picture, one simply paints over the cells of a generic template for the universe ''X'', going according to some previously adopted convention, for instance: Let the cells that get the value 0 under ''f'' remain untinted, and let the cells that get the value 1 under ''f'' be painted or shaded. In doing this, it may be good to remind ourselves that the value of the picture as a whole is not in the "paints", in other words, the 0, 1 in '''B''', but in the pattern of regions that they indicate. NB. In this Ascii version, I use background shadings of [ ] for 0 and [ ` ` ` ] for 1.
Figure 27 indicates the points of the universe of discourse <math>X\!</math> for which the proposition <math>f : X \to \mathbb{B}</math> has the value 1, here interpreted as the logical value <math>\operatorname{true}.</math> In this ''paint by numbers'' style of picture, one simply paints over the cells of a generic template for the universe <math>X,\!</math> going according to some previously adopted convention, for instance: Let the cells that get the value 0 under <math>f\!</math> remain untinted and let the cells that get the value 1 under <math>f\!</math> be painted or shaded. In doing this, it may be good to remind ourselves that the value of the picture as a whole is not in the ''paints'', in other words, the <math>0, 1\!</math> in <math>\mathbb{B},</math> but in the pattern of regions that they indicate.
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center"
|
| [[Image:Venn Diagram (P (Q)) (P (R)).jpg|500px]] || (27)
|-
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))}</math>
| ` ` ` o ` ` ` ` ` ` ` ` o ` ` ` o ` ` ` ` ` ` ` ` o ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` `\` ` `/` ` ` ` ` ` ` ` `/` ` ` ` |
</pre>
|}
|}
There are a number of standard ways in mathematics and statistics for talking about "the subset ''W'' of the domain ''X'' that gets painted with the value ''z'' by the indicator function ''f'' : ''X'' → '''B'''". The subset ''W'' ⊆ ''X'' is called the "antecedent", the "fiber", the "inverse image", the "level set", or the "pre-image" in ''X'' of ''z'' under ''f'', and is defined as ''W'' = ''f''<sup>–1</sup>(''z''). Here, ''f''<sup>–1</sup> is called the "converse relation" or the "inverse relation" — it is not in general an inverse function — corresponding to the function ''f''. Whenever possible in simple examples, I will use lower case letters for functions ''f'' : ''X'' → '''B''', and I will try to employ capital letters for subsets of ''X'', if possible, in such a way that ''F'' will be the fiber of 1 under ''f'', in other words, ''F'' = ''f''<sup>–1</sup>(1).
There are a number of standard ways in mathematics and statistics for talking about the subset <math>W\!</math> of the functional domain <math>X\!</math> that gets painted with the value <math>z \in \mathbb{B}</math> by the indicator function <math>f : X \to \mathbb{B}.</math> The region <math>W \subseteq X</math> is called by a variety of names in different settings, for example, the ''antecedent'', the ''fiber'', the ''inverse image'', the ''level set'', or the ''pre-image'' in <math>X\!</math> of <math>z\!</math> under <math>f.\!</math> It is notated and defined as <math>W = f^{-1}(z).\!</math> Here, <math>f^{-1}\!</math> is called the ''converse relation'' or the ''inverse relation'' — it is not in general an inverse function — corresponding to the function <math>f.\!</math> Whenever possible in simple examples, we use lower case letters for functions <math>f : X \to \mathbb{B},</math> and it is sometimes useful to employ capital letters for subsets of <math>X,\!</math> if possible, in such a way that <math>F\!</math> is the fiber of 1 under <math>f,\!</math> in other words, <math>F = f^{-1}(1).\!</math>
The easiest way to see the sense of the venn diagram is to notice that the expression <math>\texttt{(} p \texttt{(} q \texttt{))},</math> read as <math>p \Rightarrow q,</math> can also be read as <math>{}^{\backprime\backprime} \operatorname{not}~ p ~\operatorname{without}~ q {}^{\prime\prime}.</math> Its assertion effectively excludes any tincture of truth from the region of <math>P\!</math> that lies outside the region <math>Q.\!</math> In a similar manner, the expression <math>\texttt{(} p \texttt{(} r \texttt{))},</math> read as <math>p \Rightarrow r,</math> can also be read as <math>{}^{\backprime\backprime} \operatorname{not}~ p ~\operatorname{without}~ r {}^{\prime\prime}.</math> Asserting it effectively excludes any tincture of truth from the region of <math>P\!</math> that lies outside the region <math>R.\!</math>
Figure 2 shows the other standard way of drawing a venn diagram for such a proposition. In this "punctured soap film" style of picture — others may elect to give it the more dignified title of a "logical quotient topology" or some such thing — one goes on from the previous picture to collapse the fiber of 0 under ''X'' down to the point of vanishing utterly from the realm of active contemplation, thereby arriving at a degenre of picture like so:
Figure 28 shows the other standard way of drawing a venn diagram for such a proposition. In this ''punctured soap film'' style of picture — others may elect to give it the more dignified title of a ''logical quotient topology'' — one begins with Figure 27 and then proceeds to collapse the fiber of 0 under <math>X\!</math> down to the point of vanishing utterly from the realm of active contemplation, arriving at the following picture:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center"
|
| [[Image:Venn Diagram (P (Q R)).jpg|500px]] || (28)
|-
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q ~ r \texttt{))}</math>
| | | | | |
| o o o o |
</pre>
|}
|}
This diagram indicates that the region where p is true is wholly contained in the region where both q and r are true. Since only the regions that are painted true in the previous figure show up at all in this one, it is no longer necessary to distinguish the fiber of 1 under f by means of any stipple.
This diagram indicates that the region where <math>p\!</math> is true is wholly contained in the region where both <math>q\!</math> and <math>r\!</math> are true. Since only the regions that are painted true in the previous figure show up at all in this one, it is no longer necessary to distinguish the fiber of 1 under <math>f\!</math> by means of any shading.
In sum, it is immediately obvious from the venn diagram that in drawing a representation of the propositional expression:
In sum, it is immediately obvious from the venn diagram that in drawing a representation of the following propositional expression:
{| align="center" cellpadding="8"
| <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))},</math>
|}
in other words,
in other words,
{| align="center" cellpadding="8"
| <math>(p \Rightarrow q) \land (p \Rightarrow r),</math>
|}
we are also looking at a picture of:
we are also looking at a picture of:
{| align="center" cellpadding="8"
| <math>\texttt{(} p \texttt{(} q r \texttt{))},</math>
|}
in other words,
in other words,
{| align="center" cellpadding="8"
| <math>p \Rightarrow (q \land r).</math>
|}
Let us now examine the following propositional equation:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)).jpg|500px]] || (29)
| [p=>q] & [p=>r] = [p=>[q&r]] |
| |
|}
|}
While we go through each of these ways let us keep one eye out for the character and the conduct of each type of proceeding as a semiotic process, that is, as an orbit, in this case discrete, through a locus of signs, in this case propositional expressions, and as it happens in this case, a sequence of transformations that perseveres in the denotative objective of each expression, that is, in the abstract proposition that it expresses, while it preserves the informed constraint on the universe of discourse that gives us one viable candidate for the informational content of each expression in the interpretive chain of sign metamorphoses.
While we go through each of these ways let us keep one eye out for the character and the conduct of each type of proceeding as a semiotic process, that is, as an orbit, in this case discrete, through a locus of signs, in this case propositional expressions, and as it happens in this case, a sequence of transformations that perseveres in the denotative objective of each expression, that is, in the abstract proposition that it expresses, while it preserves the informed constraint on the universe of discourse that gives us one viable candidate for the informational content of each expression in the interpretive chain of sign metamorphoses.
A ''sign relation'' '''L''' is a subset of a cartesian product '''O''' × '''S''' × '''I''', where '''O''', '''S''', '''I''' are sets known as the ''object domain'', the ''sign domain'', and the ''interpretant sign domain'', respectively. One writes '''L''' ⊆ '''O''' × '''S''' × '''I''', where the symbol "⊆" denotes the subset relation ''contained as a subset of''. Accordingly, a sign relation '''L''' consists of ordered 3-tuples of the form <''o'', ''s'', ''i''>, where ''o'', ''s'', ''i'' are elements of the domains '''O''', '''S''', '''I''', respectively.
A ''sign relation'' <math>L\!</math> is a subset of a cartesian product <math>O \times S \times I,</math> where <math>O, S, I\!</math> are sets known as the ''object'', ''sign'', and ''interpretant sign'' domains, respectively. These facts are symbolized by writing <math>L \subseteq O \times S \times I.</math> Accordingly, a sign relation <math>L\!</math> consists of ordered triples of the form <math>(o, s, i),\!</math> where <math>o, s, i\!</math> belong to the domains <math>O, S, I,\!</math> respectively. An ordered triple of the form <math>(o, s, i) \in L</math> is referred to as a ''sign triple'' or an ''elementary sign relation''.
The ''semiotic domain'' or the ''syntactic domain'' of a sign relation '''L''' ⊆ '''O''' × '''S''' × '''I''' is just the set-theoretic union '''S''' ∪ '''I''' of its sign domain '''S''' and its interpretant domain '''I'''.
The ''syntactic domain'' of a sign relation <math>L \subseteq O \times S \times I</math> is defined as the set-theoretic union <math>S \cup I</math> of its sign domain <math>S\!</math> and its interpretant domain <math>I.\!</math> It is not uncommon, especially in formal examples, for the sign domain and the interpretant domain to be equal as sets, in short, to have <math>S = I.\!</math>
Sign relations may contain any number of sign triples, finite or infinite. Finite sign relations do arise in applications and can be very instructive as expository examples, but most of the sign relations of significance in logic have infinite sign and interpretant domains, and usually infinite object domains, in the long run, at least, though one frequently works up to infinite domains by a series of finite approximations and gradual stages.
With that preamble behind us, let us turn to consider the case of semiosis, or sign transformation process, that is generated by our first proof of the propositional equation <math>E_1.\!</math>
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)) Proof 1.jpg|500px]]
| (30)
{| align="center" style="text-align:center; width:90%"
|
| |
|}
|}
For some reason I always think of this as the way that our DNA would prove it.
For some reason I always think of this as the way that our DNA would prove it.
We are in the process of examining various proofs of the propositional equation "(p (q))(p (r)) = (p (q r))", and viewing them in the light of their character as semiotic processes, in essence, as sign-theoretic transformations.
We are in the process of examining various proofs of the propositional equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))},</math> and viewing these proofs in the light of their character as semiotic processes, in essence, as sign-theoretic transformations.
The second way of establishing the truth of this equation is one that I see, rather loosely, as ''model-theoretic'', for no better reason than the sense of its ending with a pattern of expression, a variant of the ''disjunctive normal form'' (DNF), that is commonly recognized to be the form that one extracts from a truth table by pulling out the rows of the table that evaluate to true and constructing the disjunctive expression that sums up the senses of the corresponding interpretations.
In order to apply this model-theoretic method to an equation between a couple of contingent expressions, one must transform each expression into its associated DNF and then compare those to see if they are equal. In the current setting, these DNF's may indeed end up as identical expressions, but it is possible, also, for them to turn out slightly off-kilter from each other, and so the ultimate comparison may not be absolutely immediate. The explanation of this is that, for the sake of computational efficiency, it is useful to tailor the DNF that gets developed as the output of a DNF algorithm to the particular form of the propositional expression that is given as input.
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
|
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
|-
| Equation E_1 |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-0.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-1.jpg|500px]]
| q r |
|-
| q o o r o |
| [[Image:Equational Inference Bar -- Cast P.jpg|500px]]
| | | | |
|-
| p o o p p o |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-2.jpg|500px]]
| \ / | |
|-
| @ = @ |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
| |
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-3.jpg|500px]]
| |
|-
| (p (q)) (p (r)) = (p (q r)) |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| |
|-
| [p=>q] & [p=>r] = [p=>[q&r]] |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-4.jpg|500px]]
| |
|-
| [[Image:Equational Inference Bar -- Cast Q.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-5.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-6.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-7.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast R.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-8.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-9.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
|}
| (31)
|}
|}
The second way of establishing the truth of this equation is one that I see, rather loosely, as ''model-theoretic'', for no better reason than the sense of its ending with a pattern of expression, a variant of the ''disjunctive normal form'' (DNF), that is commonly recognized to be the form that one extracts from a truth table by pulling out the rows of the table that evaluate to true and constructing the disjunctive expression that sums up the senses of the corresponding interpretations.
The final graph in the sequence of equivalents is a disjunctive normal form (DNF) for the proposition on the left hand side of the equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}.</math>
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
| [[Image:Logical Graph (P (Q)) (P (R)) DNF.jpg|500px]]
| (32)
| |
|}
|}
Remembering that a blank node is the graphical equivalent of a logical value <math>\operatorname{true},</math> the resulting DNF may be read as follows:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| |
| |
|}
|}
It remains to show that the right hand side of the equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}</math> is logically equivalent to the DNF just obtained. The needed chain of equations is as follows:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
|
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
|-
| Equation E_1 |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-0.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-1.jpg|500px]]
| q r |
|-
| q o o r o |
| [[Image:Equational Inference Bar -- Cast P.jpg|500px]]
| | | | |
|-
| p o o p p o |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-2.jpg|500px]]
| \ / | |
|-
| @ = @ |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
| |
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-3.jpg|500px]]
| |
|-
| (p (q)) (p (r)) = (p (q r)) |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| |
|-
| [p=>q] & [p=>r] = [p=>[q&r]] |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-4.jpg|500px]]
| |
|-
| [[Image:Equational Inference Bar -- Cast Q.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-5.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-6.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-7.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast R.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-8.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-2-9.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
|}
|}
| (33)
|}
|}
This is not only a logically equivalent DNF, but exactly the same DNF expression that we obtained before, so we have established the given equation "(p (q))(p (r)) = (p (q r))".
This is not only a logically equivalent DNF but exactly the same DNF expression that we obtained before, so we have established the given equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}.</math> Incidentally, one may wish to note that this DNF expression quickly folds into the following form:
Incidentally, one may wish to note that this DNF expression quickly folds into the following form:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
| [[Image:Logical Graph (P Q R , (P)).jpg|500px]] || (34)
| |
|}
|}
This can be read to say "either p q r, or not p", which gives us yet another expression equivalent to the sentences "(p (q))(p (r))" and "(p (q r))".
This can be read to say <math>{}^{\backprime\backprime} \operatorname{either}~ p q r ~\operatorname{or}~ \operatorname{not}~ p {}^{\prime\prime},</math> which gives us yet another equivalent for the expression <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math> and the expression <math>\texttt{(} p \texttt{(} q r \texttt{))}.</math> Still another way of writing the same thing would be as follows:
{| align="center" cellpadding="8"
| [[Image:Logical Graph ((P , P Q R)).jpg|500px]] || (35)
{| align="center" style="text-align:center; width:90%"
|
| |
|}
|}
In other words, "p is equivalent to p and q and r".
In other words, <math>{}^{\backprime\backprime} p ~\operatorname{is~equivalent~to}~ p ~\operatorname{and}~ q ~\operatorname{and}~ r {}^{\prime\prime}.</math>
One lemma that suggests itself at this point is a principle that may be canonized as the ''Emptiness Rule''. It says that a bare lobe expression like <math>\texttt{( \_, \_, \ldots )},</math> 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 <math>\texttt{(~)}</math> that <math>\operatorname{Ex}</math> interprets as denoting the logical value <math>\operatorname{false}.</math> To depict the rule in graphical form, we have the continuing sequence of equations:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
| @ = @ = @ = ... |
| @ = @ = @ = ... |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (36)
|}
|}
Yet another rule that we'll need is the following:
Yet another rule that we'll need is the following:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
| @ = @ = @ = ... |
| @ = @ = @ = ... |
| |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (37)
|}
|}
This one is easy enough to derive from rules that are already known, but I call it the ''Indistinctness Rule'' just on behalf of ready reference and easy employment.
This one is easy enough to derive from rules that are already known, but just for the sake of ready reference it is useful to canonize it as the ''Indistinctness Rule''. Finally, let me introduce a rule-of-thumb that is a bit more suited to routine computation, and that serves to replace the indistinctness rule in many cases where we actually have to call on it. This is actually just a special case of the evaluation rule listed above:
Finally, let me introduce a rule-of-thumb that is a bit more suited to routine computation, and that will serve to replace the indistinctness rule in many of the cases where we actually have to call on it. This is actually just a special case of the evaluation rule listed above:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (38)
|}
|}
To continue with the beating of this still kicking horse that is known as the propositional equation "(p (q))(p (r)) = (p (q r))", let's now take up the third way that I mentioned for examining propositional equations, but I believe that you will be relieved to know that it is literally a third way only at the very outset, almost immediately breaking up according to whether one proceeds by way of the more routine model-theoretic path or else by way of the more strategic proof-theoretic path. I think that I'll take the low road today.
To continue with the beating of this still-kicking horse in the form of the equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))},</math> let's now take up the third way that I mentioned for examining propositional equations, even if it is literally a third way only at the very outset, almost immediately breaking up according to whether one proceeds by way of the more routine model-theoretic path or else by way of the more strategic proof-theoretic path.
Let's convert the equation between propositions:
Let's convert the equation between propositions:
{| align="center" cellpadding="8"
|
<math>\begin{matrix}
\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}
& = &
\texttt{(} p \texttt{(} q r \texttt{))}
\end{matrix}</math>
|}
into the corresponding equational proposition:
into the corresponding equational proposition:
{| align="center" cellpadding="8"
|
<math>\begin{matrix}
\texttt{((}
&
\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \text{))}
& \texttt{,} &
\texttt{(} p \texttt{(} q r \texttt{))}
&
\texttt{))}
\end{matrix}</math>
|}
If you're like me, you'd rather see it in pictures:
If you're like me, you'd rather see it in pictures:
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
| [[Image:Logical Graph (( (P (Q)) (P (R)) , (P (Q R)) )).jpg|500px]]
| (39)
| [[p=>q] & [p=>r]] <=> [p=>[q&r]] |
| |
|}
|}
We may now interrogate the alleged equation for the third time, working by way of the ''case analysis-synthesis theorem'' (CAST).
We may now interrogate the alleged equation for the third time, working by way of the ''case analysis-synthesis theorem'' (CAST).
{| align="center" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
|
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-00.jpg|500px]]
|-
| |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-01.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast P.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-02.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-03.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-04.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Emptiness.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-05.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-06.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast Q.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-07.jpg|500px]]
| \ / \ / |
|-
| \ / \ / |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| \ / \ / |
|-
| o o |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-08.jpg|500px]]
| | | |
|-
| | | |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-09.jpg|500px]]
| \ / |
|-
| \ / |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-10.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Spike.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-11.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| q r q r |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-12.jpg|500px]]
|-
| | | | / / / |
| [[Image:Equational Inference Bar -- Cast R.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-13.jpg|500px]]
|-
| \ / \ / |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| \ / \ / |
|-
| \ / \ / |
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-14.jpg|500px]]
| o o |
|-
| [[Image:Equational Inference Bar -- Emptiness.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-15.jpg|500px]]
|-
| \ / |
| [[Image:Equational Inference Bar -- Spike.jpg|500px]]
| \ / |
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-16.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 3-17.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
|}
| (40)
| q r q r |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| | | |
| \ / |
| \ / |
| q r q r |
| o o o |
| p o---------------o---o p |
| \ / |
| q r q r |
| | | | |
| \ / |
| \ / |
| o o |
| \ / \ / |
| \ / |
| \ / |
| | | | | | | |
| \ / \ / |
| p o-------o---o p |
| \ / |
| o o o |
| | | |
| \ / |
| \ / |
| r r |
| | | |
| \ / |
| \ / |
| r r |
| | | |
| \ / |
| \ / |
| o o |
| | |
| p o-------o---o p |
| \ / |
| r o---------------o---o r |
| \ / |
| \ / |
| \ / |
| \ / \ / |
| \ / |
| \ / |
| \ / |
| | | |
| q o-------o---o q |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
|}
|}
