12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Friday November 22, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Futures Of Logical Graphs (view source)
Revision as of 03:27, 28 August 2009
, 03:27, 28 August 2009→Example: convert graphics
===Example===
===Example===
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's Praeclarum Theorema as a way of illustrating how. It will suffice to work within the Existential interpretation.
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's Praeclarum Theorema as a way of illustrating how.
{| 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"
|-
| Praeclarum Theorema. Proof by CAST. |
| [[Image:Proof Praeclarum Theorema CAST 00.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 01.jpg|500px]]
| b o o c o bc |
|-
| [[Image:Equational Inference Bar -- Cast A.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 02.jpg|500px]]
|-
| | |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 03.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| bc |
| [[Image:Proof Praeclarum Theorema CAST 04.jpg|500px]]
|-
| | | | | | |/ |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| \ / | \ / | |
| [[Image:Proof Praeclarum Theorema CAST 05.jpg|500px]]
|-
| | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| | | |
|-
| a o-----------------------------o---o a |
| [[Image:Proof Praeclarum Theorema CAST 06.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast D.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 07.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 08.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 09.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
| o o d o d o--o o d o |
|-
| \ / | \ / | |
| [[Image:Proof Praeclarum Theorema CAST 10.jpg|500px]]
| o-------o o-------o |
|-
| | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 11.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast B.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 12.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 13.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 14.jpg|500px]]
| b o o c o bc o c |
|-
| | | | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 15.jpg|500px]]
| o-------o o-------o |
|-
| [[Image:Equational Inference Bar -- Cast C.jpg|500px]]
| | | |
|-
| [[Image:Proof Praeclarum Theorema CAST 16.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 17.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 18.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
|}
|}
| b o o c o bc |
| | | | |
What we have harvested is the succulent equivalent of a ''disjunctive normal form'' (DNF) for the proposition with which we started.
| o o d o d |
{| align="center" cellpadding="8"
| [[Image:Praeclarum Theorema DNF.jpg|500px]]
| a o-----------------------------o---o a |
| b o o c o bc |
| | | | |
| o o d o d |
| \ / | |
| a o-----------------------------o---o a |
| \ / |
| | | |
| a o---o---o a |
| b |
| | | |
| | | |
| \ / |
| b |
| | | |
| | | |
| \ / |
| \ / | |
| | | |
| | | |
| \ / |
| b o o c o bc |
| | | | |
| o-------o |
| d o-------------------------o---o d |
| \ / |
| \ / |
| | | |
| \ / |
| o c o c o c o c |
| | | |
| b o-------------------------o---o b |
| \ / |
| o c o c |
| | | |
| | | |
| \ / |
| o-------o |
| | |
| b o-------------------------o---o b |
| d o---o---o d |
| \ / |
| \ / |
| o-------o o-------o |
| | | |
| \ / |
| \ / |
| d o---o---o d |
| a o---o---o a |
| o-------o o-------o |
| | | |
| c o-------------------------o---o c |
| \ / |
| \ / |
| d o---o---o d |
| @ |
| |
| b o---o---o b |
|}
|}
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="10" style="text-align:center; width:90%"
|
|
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| |
| |
|}
|}
That is tantamount to saying that the proposition being submitted for analysis is true in every case. Thus we are justified in awarding it the title of a ''Theorem''.
==Logic as sign transformation==
==Logic as sign transformation==
