12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 03:26, 11 August 2009
, 03:26, 11 August 2009→Analysis of contingent propositions: center figures
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 in and outs of a typical propositional equation reasoning system (PERS), let's now take up a much simpler example of a contingent proposition:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
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 (''Ex'') of logical graphs and their corresponding parse strings.
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 [```] for 0 and [^^^] for 1.
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 [```] for 0 and [^^^] for 1.
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
Figure 1. Venn Diagram for (p (q))(p (r))
Figure 1. Venn Diagram for (p (q))(p (r))
</pre>
</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
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 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 ''X'' of ''z'' under ''f''. It is notated and 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, we use lower case letters for functions ''f'' : ''X'' → '''B''', and its is sometimes useful to employ capital letters for subsets of ''X'', if possible, in such a way that ''F'' is the fiber of 1 under ''f'', in other words, ''F'' = ''f''<sup>–1</sup>(1).
''W'' ⊆ ''X'' 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 ''X'' of ''z'' under ''f''. It is notated and 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, we use lower case letters for functions ''f'' : ''X'' → '''B''', and its is sometimes useful to employ capital letters for subsets of ''X'', if possible, in such a way that ''F'' is the fiber of 1 under ''f'', in other words, ''F'' = ''f''<sup>–1</sup>(1).
The easiest way to see the sense of the venn diagram is to notice that the expression "(p (q))", read as "''p'' ⇒ ''q''", can also be read as "not ''p'' without ''q''". Its assertion effectively excludes any tincture of truth from the region of ''P'' that lies outside the region ''Q''.
The easiest way to see the sense of the venn diagram is to notice that the expression "(p (q))", read as "''p'' ⇒ ''q''", can also be read as "not ''p'' without ''q''". Its assertion effectively excludes any tincture of truth from the region of ''P'' that lies outside the region ''Q''.
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 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:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
Figure 2. Venn Diagram for (p (q r))
Figure 2. Venn Diagram for (p (q r))
</pre>
</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 ''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.
Let us now examine the following propositional equation:
Let us now examine the following propositional equation:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
There are three distinct ways that I can think of right off as to how we might go about formally proving or systematically checking the proposed equivalence, the evidence of whose truth we already have before us clearly enough, and in a visually intuitive form, from the venn diagrams that we examined above.
There are three distinct ways that I can think of right off as to how we might go about formally proving or systematically checking the proposed equivalence, the evidence of whose truth we already have before us clearly enough, and in a visually intuitive form, from the venn diagrams that we examined above.
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 ''E''<sub>1</sub>.
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 ''E''<sub>1</sub>.
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o=============================< QED >=======================o
o=============================< QED >=======================o
</pre>
</pre>
|}
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.
Here is a reminder of the equation in question:
Here is a reminder of the equation in question:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
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 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.
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" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o=============================< DNF >=======================o
o=============================< DNF >=======================o
</pre>
</pre>
|}
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 ''true'', 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 ''true'', we can read this brand of DNF in the following manner:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
Sorry, the half-time show was cancelled by the censors. But I'm guessing that the reader can probably finish off the second half of the proof with a few scribbles on paper faster than I can asciify it on my own, so at least there's that entertaiment to occupy the interval.
Sorry, the half-time show was cancelled by the censors. But I'm guessing that the reader can probably finish off the second half of the proof with a few scribbles on paper faster than I can asciify it on my own, so at least there's that entertaiment to occupy the interval.
We are still in the middle of contemplating a particular example of a propositional equation, namely, "(p (q))(p (r)) = (p (q r))", and we are still considering the second of three formal methods that I intend to illustrate in the process of thrice-over establishing it.
We are still in the middle of contemplating a particular example of a propositional equation, namely, "(p (q))(p (r)) = (p (q r))", and we are still considering the second of three formal methods that I intend to illustrate in the process of thrice-over establishing it.
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
I know that it must seem tedious, but I probably ought to go ahead and carry out the second half of this analogically model-theoretic strategy, just so that we will have the security of this concrete and shared experience on which to fall back at every later point in whatmay quickly become a rather abstruse discussion. Here then is the rest of the necessary chain of equations:
I know that it must seem tedious, but I probably ought to go ahead and carry out the second half of this analogically model-theoretic strategy, just so that we will have the security of this concrete and shared experience on which to fall back at every later point in whatmay quickly become a rather abstruse discussion. Here then is the rest of the necessary chain of equations:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o=============================< DNF >=======================o
o=============================< DNF >=======================o
</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 "(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 "(p (q))(p (r)) = (p (q r))".
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" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
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 "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))".
Still another way of writing the same thing would be like so:
Still another way of writing the same thing would be like so:
{| align="center" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
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 ''Ex'' 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%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</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%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
This one is easy enough to derive from rules that are already known, but call it the ''Indistinctness Rule'' just on behalf of ready reference and employment.
This one is easy enough to derive from rules that are already known, but call it the ''Indistinctness Rule'' just on behalf of ready reference and employment.
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:
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" cellpadding="10" style="text-align:center; width:90%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
|}
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 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.
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%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</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%"
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
o==================================< QED >==================o
o==================================< QED >==================o
</pre>
</pre>
|}
And that, of course, is the DNF of a theorem.
And that, of course, is the DNF of a theorem.