12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 12:50, 18 August 2009
, 12:50, 18 August 2009→Analysis of contingent propositions: redo proof display as table of figures
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:
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" cellpadding="10"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)).jpg|500px]] || (26)
| [[Image:Logical Graph (P (Q)) (P (R)).jpg|500px]] || (26)
|}
|}
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:
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="10"
{| align="center" cellpadding="8"
| <math>f ~=~ \texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math>
| <math>f ~=~ \texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))}</math>
|}
|}
In sum, it is immediately obvious from the venn diagram that in drawing a representation of the following 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="10"
{| align="center" cellpadding="8"
| <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))},</math>
| <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))},</math>
|}
|}
in other words,
in other words,
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
| <math>(p \Rightarrow q) \land (p \Rightarrow r),</math>
| <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="10"
{| align="center" cellpadding="8"
| <math>\texttt{(} p \texttt{(} q r \texttt{))},</math>
| <math>\texttt{(} p \texttt{(} q r \texttt{))},</math>
|}
|}
in other words,
in other words,
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
| <math>p \Rightarrow (q \land r).</math>
| <math>p \Rightarrow (q \land r).</math>
|}
|}
Let us now examine the following propositional equation:
Let us now examine the following propositional equation:
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)).jpg|500px]] || (29)
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)).jpg|500px]] || (29)
|}
|}
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>
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="10"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)) Proof 1.jpg|500px]]
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)) Proof 1.jpg|500px]]
| (30)
| (30)
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.
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" cellpadding="10"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)) Proof 2a Alt.jpg|500px]]
|
{| 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)) 2-1-0.jpg|500px]]
|-
| [[Image:Proof (P (Q)) (P (R)) = (P (Q R)) 2-1-1.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast P.jpg|500px]]
|-
| [[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]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[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)
| (31)
|}
|}
What we have harvested is the succulent equivalent of a disjunctive normal form (DNF) for the proposition with which we started. Remembering that a blank node is the graphical equivalent of a logical value <math>\operatorname{true},</math> we can read this brand of DNF in the following manner:
What we have harvested is the succulent equivalent of a disjunctive normal form (DNF) for the proposition with which we started. Remembering that a blank node is the graphical equivalent of a logical value <math>\operatorname{true},</math> we can read this brand of DNF in the following manner:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
We are still in the middle of contemplating a particular example of a propositional equation, namely, <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))},</math> and we are still considering the second of three formal methods that are illustrated in the process of thrice-over establishing it.
We are still in the middle of contemplating a particular example of a propositional equation, namely, <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))},</math> and we are still considering the second of three formal methods that are illustrated in the process of thrice-over establishing it.
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
We probably ought to go ahead and carry out the second half of this model-theoretic strategy, just so we'll have the security of this concrete experience to call on in future discussions. The remainder of the needed chain of equations is as follows:
We probably ought to go ahead and carry out the second half of this model-theoretic strategy, just so we'll have the security of this concrete experience to call on in future discussions. The remainder of the needed chain of equations is as follows:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
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:
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:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
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:
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="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
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:
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" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
Yet another rule that we'll need is the following:
Yet another rule that we'll need is the following:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
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:
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:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
Let's convert the equation between propositions:
Let's convert the equation between propositions:
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
into the corresponding equational proposition:
into the corresponding equational proposition:
{| align="center" cellpadding="10"
{| align="center" cellpadding="8"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
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" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>
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" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
|
<pre>
<pre>