ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 7
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The Case Analysis-Synthesis Theorem (CAST)
The task at hand is to lay out what I think of as the pontoon bridge
between the model-theoretic and the proof-theoretic shores, and thus
between their diverging perspectives on logical procedure, even if I
can construct it at a point but so close to their common source that
it may not seem like it's worth the candle. Irregardless here it is.
The substance of this principle was known to Boole a sesquicentury ago,
tantamount to the "Boolean Expansion" that he uncovered while nameless.
So the only novelty here will rest in a certain manner of presentation,
in which I will prove the basic principle from the axioms given before.
One name for this rule is the "Case Analysis-Synthesis Theorem" (CAST).
The preparatory materials that we need are these:
I am going to revert to my customarily sloppy workshop manners
and refer to propositions and proposition expressions on rough
analogy with functions and function expressions, which implies
that a proposition will be regarded as the chief formal object
of discussion, enjoying many proposition expressions, formulas,
or sentences that express it, but worst of all I will probably
just go ahead and use any and all of these terms as loosely as
I see fit, taking a bit of extra care only when I see the need.
Let Q be a proposition with an unspecified, but context-fitting
number of variables, say, none, or x, or x_1, ..., x_k, as the
case may be. (More precisely, I should've said "sentence Q".)
Strings and graphs sans labels are called "bare".
A bare terminal node, "o", is known as a "stone".
A bare terminal edge, "|", is known as a "stick".
Let the "replacement expression" of the form "Q[o/x]" denote
the proposition that results from Q by replacing every token
of the variable x with a blank, which is to say, erasing "x".
Let the "replacement expression" of the form "Q[|/x]" denote
the proposition that results from Q by replacing every token
of the variable x with a stick stemming from the site of "x".
In the case of a proposition Q, that is, an expression of it,
not having a token of the designated variable "x", let it be
stipulated that Q[o/x] = Q = Q[|/x].
I think that I am at long last ready to state the following:
o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem (CAST) |
o-----------------------------------------------------------o
| |
| x |
| o |
| x | |
| Q[o/x] o---o Q[|/x] |
| Q \ / |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| Q = ( Q[o/x] x , Q[|/x] (x) ) |
| |
o-----------------------------------------------------------o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o