12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 16:34, 20 August 2009
, 16:34, 20 August 2009→Analysis of contingent propositions: convert graphics
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="8" 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]]
|}
| 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 o-------o |
| \ / \ / |
| \ / |
| \ / |
| o o |
| \ / \ / |
| p o-------o---o p |
| \ / |
| o o o |
| | | |
| \ / |
| \ / |
| r r |
| | | |
| \ / |
| \ / |
| r r |
| | | |
| \ / |
| \ / |
| r r |
| | |
| p o-------o---o p |
| \ / |
| r o---------------o---o r |
| \ / |
| \ / |
| \ / |
| \ / \ / |
| \ / |
| \ / |
| \ / |
| r o---------------o---o r |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| (40)
| (40)
|}
|}