12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 21:20, 24 March 2010
, 21:20, 24 March 2010back to arabic numbering of figures & tables, but sequential with sections
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_05.jpg|500px]] || (α)
| [[Image:PERS_Figure_05.jpg|500px]] || (1)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_06.jpg|500px]] || (β)
| [[Image:PERS_Figure_06.jpg|500px]] || (2)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_07.jpg|500px]] || (γ)
| [[Image:PERS_Figure_07.jpg|500px]] || (3)
|}
|}
| [[Image:Double Negation 2.0 Animation.gif]]
| [[Image:Double Negation 2.0 Animation.gif]]
|}
|}
| (δ)
| (4)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_08.jpg|500px]] || (α)
| [[Image:PERS_Figure_08.jpg|500px]] || (1)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_09.jpg|500px]] || (β)
| [[Image:PERS_Figure_09.jpg|500px]] || (2)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_10.jpg|500px]] || (α)
| [[Image:PERS_Figure_10.jpg|500px]] || (1)
|}
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_11.jpg|500px]] || (β)
| [[Image:PERS_Figure_11.jpg|500px]] || (2)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:PERS_Figure_12.jpg|500px]] || (α)
| [[Image:PERS_Figure_12.jpg|500px]] || (1)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:PERS_Figure_13.jpg|500px]] || (β)
| [[Image:PERS_Figure_13.jpg|500px]] || (2)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:PERS_Figure_14.jpg|500px]] || (α)
| [[Image:PERS_Figure_14.jpg|500px]] || (1)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:PERS_Figure_15.jpg|500px]] || (β)
| [[Image:PERS_Figure_15.jpg|500px]] || (2)
|}
|}
a b + a c + b c
a b + a c + b c
\end{matrix}</math>
\end{matrix}</math>
| (α)
| (1)
|}
|}
| [[Image:Equational Inference QED.jpg|500px]]
| [[Image:Equational Inference QED.jpg|500px]]
|}
|}
| (β)
| (2)
|}
|}
| [[Image:Majority Function Example 2.0 Animation.gif]]
| [[Image:Majority Function Example 2.0 Animation.gif]]
|}
|}
| (γ)
| (3)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (α)
| (1)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (β)
| (2)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (α)
| (1)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (β)
| (2)
|-
|-
|
|
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (γ)
| (3)
|-
|-
|
|
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (δ)
| (4)
|}
|}
o=============================< QES >=======================o
o=============================< QES >=======================o
</pre>
</pre>
| (ε)
| (5)
|}
|}
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
|}
|}
| (α)
| (1)
|}
|}
| [[Image:Praeclarum Theorema CAST 2.0 Animation.gif]]
| [[Image:Praeclarum Theorema CAST 2.0 Animation.gif]]
|}
|}
| (β)
| (2)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Praeclarum Theorema DNF.jpg|500px]]
| [[Image:Praeclarum Theorema DNF.jpg|500px]]
| (γ)
| (3)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (δ)
| (4)
|}
|}
{| align="center" cellpadding="10"
{| align="center" cellpadding="10"
| [[Image:Praeclarum Theorema.jpg|500px]] || (α)
| [[Image:Praeclarum Theorema.jpg|500px]] || (1)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)).jpg|500px]] || (α)
| [[Image:Logical Graph (P (Q)) (P (R)).jpg|500px]] || (1)
|}
|}
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.
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 β 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.
Figure 2 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" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8" style="text-align:center"
| [[Image:Venn Diagram (P (Q)) (P (R)).jpg|500px]] || (β)
| [[Image:Venn Diagram (P (Q)) (P (R)).jpg|500px]] || (2)
|-
|-
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))}</math>
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))}</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>
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 γ 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 31 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:
Figure 3 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 31 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" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8" style="text-align:center"
| [[Image:Venn Diagram (P (Q R)).jpg|500px]] || (γ)
| [[Image:Venn Diagram (P (Q R)).jpg|500px]] || (3)
|-
|-
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q ~ r \texttt{))}</math>
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q ~ r \texttt{))}</math>
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)).jpg|500px]] || (δ)
| [[Image:Logical Graph (P (Q)) (P (R)) = (P (Q R)).jpg|500px]] || (4)
|}
|}
{| align="center" cellpadding="8"
{| 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]]
| (ε)
| (5)
|}
|}
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
|}
|}
| (ζ)
| (6)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P (Q)) (P (R)) DNF.jpg|500px]]
| [[Image:Logical Graph (P (Q)) (P (R)) DNF.jpg|500px]]
| (η)
| (7)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (θ)
| (8)
|}
|}
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
| [[Image:Equational Inference Bar -- DNF.jpg|500px]]
|}
|}
| (ι)
| (9)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (P Q R , (P)).jpg|500px]] || (κ)
| [[Image:Logical Graph (P Q R , (P)).jpg|500px]] || (10)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph ((P , P Q R)).jpg|500px]] || (λ)
| [[Image:Logical Graph ((P , P Q R)).jpg|500px]] || (11)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (μ)
| (12)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (ν)
| (13)
|}
|}
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
| (ξ)
| (14)
|}
|}
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
| [[Image:Logical Graph (( (P (Q)) (P (R)) , (P (Q R)) )).jpg|500px]]
| [[Image:Logical Graph (( (P (Q)) (P (R)) , (P (Q R)) )).jpg|500px]]
| (ο)
| (15)
|}
|}
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
|}
|}
| (π)
| (16)
|}
|}