12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 15:36, 21 August 2009
, 15:36, 21 August 2009→Proof as semiosis: TeX markup
|}
|}
Proof 1 proceeded by the ''straightforward approach'', starting with <math>e_2\!</math> as <math>s_1\!</math> and ending with <math>e_3\!</math> as <math>s_n\!.</math> That is, it commenced from the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> and ended up at the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}</math> by legal moves.
'''Proof 1''' proceeded by the ''straightforward approach'', starting with <math>e_2\!</math> as <math>s_1\!</math> and ending with <math>e_3\!</math> as <math>s_n\!.</math>
Proof 2 lit on by ''burning the candle at both ends'', changing <math>e_2\!</math> into a normal form that reduced to <math>e_4,\!</math> and changing <math>e_3\!</math> into a normal form that also reduced to <math>e_4,\!</math> in this way tethering <math>e_2\!</math> and <math>e_3\!</math> to a common stake. In more detail, one route went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{,~(} p \texttt{))} {}^{\prime\prime},</math> and another went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{(} q~r \texttt{))} {}^{\prime\prime}</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{, (} p \texttt{))} {}^{\prime\prime},</math> thus equating the two points of departure.
: That is, Proof 1 commenced from the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> and ended up at the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}</math> by legal moves.
Proof 3 took the path of reflection, expressing the met-equation between ''e''<sub>2</sub> and ''e''<sub>3</sub> in the naturalized equation ''e''<sub>5</sub>, then taking ''e''<sub>5</sub> as ''s''<sub>1</sub> and exchanging it by dint of value preserving steps for ''e''<sub>1</sub> as ''s''<sub>''n''</sub>. Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that <math>\operatorname{Ex}</math> recognizes as the value ''true''.
'''Proof 2''' lit on by ''burning the candle at both ends'', changing <math>e_2\!</math> into a normal form that reduced to <math>e_4,\!</math> and changing <math>e_3\!</math> into a normal form that also reduced to <math>e_4,\!</math> in this way tethering <math>e_2\!</math> and <math>e_3\!</math> to a common stake.
: Filling in the details, one route went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{~,~(} p \texttt{))} {}^{\prime\prime},</math> and another went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{~,~(} p \texttt{))} {}^{\prime\prime},</math> thus equating the two points of departure.
'''Proof 3''' took the path of reflection, expressing the meta-equation between <math>e_2\!</math> and <math>e_3\!</math> in the form of the naturalized equation <math>e_5,\!</math> then taking <math>e_5\!</math> as <math>s_1\!</math> and exchanging it by dint of value preserving steps for <math>e_1\!</math> as <math>s_n.\!</math>
: This way of proceeding went from <math>e_5 = {}^{\backprime\backprime} \texttt{((~(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))~,~(} p \texttt{~(} q~r \texttt{))~))} {}^{\prime\prime}</math> to the blank expression that <math>\operatorname{Ex}</math> recognizes as the value <math>\operatorname{true}.</math>
Review:
Review: