Changes

Line 1,384: Line 1,384:  
We took up the Equation <math>E_1\!</math> that reads as follows:
 
We took up the Equation <math>E_1\!</math> that reads as follows:
   −
: (p (q))(p (r)) = (p (q r)).
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\texttt{(} p \texttt{~(} q \texttt{))(} p \texttt{~(} r \texttt{))} = \texttt{(} p \texttt{~(} q~r \texttt{))}.</math>
 +
|}
   −
Each of our proofs is a finite sequence of signs, and thus, for a finite integer n, takes the form:
+
Each of our proofs is a finite sequence of signs, and thus, for a finite integer <math>n,\!</math> takes the form:
   −
: ''s''<sub>1</sub>, ''s''<sub>2</sub>, ''s''<sub>3</sub>, &hellip;, ''s''<sub>''n''</sub>.
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>s_1, s_2, s_3, \ldots, s_n.</math>
 +
|}
   −
Proof 1 proceeded by the ''straightforward approach'', starting with ''e''<sub>2</sub> as ''s''<sub>1</sub> and ending with ''e''<sub>3</sub> as ''s''<sub>''n''</sub>.  That is, it commenced from the sign "(p (q))(p (r))" and ended up at the sign "(p (q r))" by legal moves.
+
Proof&nbsp;1 proceeded by the ''straightforward approach'', starting with ''e''<sub>2</sub> as ''s''<sub>1</sub> and ending with ''e''<sub>3</sub> as ''s''<sub>''n''</sub>.  That is, it commenced from the sign "(p (q))(p (r))" and ended up at the sign "(p (q r))" by legal moves.
   −
Proof 2 lit on by ''burning the candle at both ends'', changing ''e''<sub>2</sub> into a normal form that reduced to ''e''<sub>4</sub>, and changing ''e''<sub>3</sub> into a normal form that also reduced to ''e''<sub>4</sub>, in this way tethering ''e''<sub>2</sub> and ''e''<sub>3</sub> to a common stake.  In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure.
+
Proof&nbsp;2 lit on by ''burning the candle at both ends'', changing ''e''<sub>2</sub> into a normal form that reduced to ''e''<sub>4</sub>, and changing ''e''<sub>3</sub> into a normal form that also reduced to ''e''<sub>4</sub>, in this way tethering ''e''<sub>2</sub> and ''e''<sub>3</sub> to a common stake.  In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure.
   −
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&nbsp;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''.
    
Review:
 
Review:
12,080

edits