12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 18:20, 21 August 2009
, 18:20, 21 August 2009→Variations on a theme of transitivity: TeX markup
In accord with my experimental way, I will stick with the case of transitive inference until I have pinned it down thoroughly, but of course the real interest is much more general than that.
In accord with my experimental way, I will stick with the case of transitive inference until I have pinned it down thoroughly, but of course the real interest is much more general than that.
At first or maybe second sight, the relationships seem easy enough to write out. Figure 65 shows how the various logical expressions are related to each other: The expressions "(p (q))" and "(q (r))" are conjoined in a purely syntactic fashion — much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about — and the best way to sum up the state of information implicit in taking them together is just the expression "(p (q)) (q (r))" that would the canonical result of an equational or reversible rule of inference. From that equational inference, one might arrive at the implicational inference "(p (r))" by the most conventional implication.
At first sight, the relationships seem easy enough to write out. Figure 65 shows how the various logical expressions are related to each other: The expressions <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))} {}^{\prime\prime}</math> and <math>{}^{\backprime\backprime} \texttt{(} q \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> are conjoined in a purely syntactic fashion — much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about — and the best way to sum up the state of information implicit in taking them together is just the expression <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}{}^{\prime\prime}</math> that would the canonical result of an equational or reversible rule of inference. From that equational inference, one might arrive at the implicational inference <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> by the most conventional implication.
<pre>
<pre>