Changes

For example, we might begin as follows:

For example, we might begin as follows:

|

|                                                          |

<math>\begin{array}{l}

|            B=>C  C                                        |

(y \overset{ }{\underset{B}{\Downarrow}} ~

|  (y: (x: z:    ): ):                                    |

(x \overset{ }{\underset{A}{\Downarrow}} ~

|    B  A A     B C                                     |

  z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}

  ) \overset{B}{\underset{C}{\Downarrow}}

  ) \overset{ }{\underset{C}{\Downarrow}}

|            A=>B B         B=>C  C                       |

|  ((x: (y: K:    ): ): (x: z:    ): ):                    |

|      A   B  B    A B  A  A    B C                   |

((x \overset{ }{\underset{A}{\Downarrow}} ~

(y \overset{ }{\underset{B}{\Downarrow}} ~

o===========================================================o

  K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}

  ) \overset{A}{\underset{B}{\Downarrow}}

|            A=>B  B  B=>C  (A=>B)=>(A=>C) A=>C C      |

  ) \overset{ }{\underset{B}{\Downarrow}} ~

|   (x: ((y: K:    ): (z:    S:              ):    ): ):    |

(x \overset{ }{\underset{A}{\Downarrow}} ~

|    A   B B    A  A     A=>(B=>C)       A=>B  A  C   |

   z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}

   ) \overset{B}{\underset{C}{\Downarrow}}

o===========================================================o

  ) \overset{ }{\underset{C}{\Downarrow}}

=

(x \overset{ }{\underset{A}{\Downarrow}} ~

</pre>

((y \overset{ }{\underset{B}{\Downarrow}} ~

   K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}

  ) \overset{A}{\underset{B}{\Downarrow}} ~

  (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~

   S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}

  ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}

   ) \overset{A}{\underset{C}{\Downarrow}}

  ) \overset{ }{\underset{C}{\Downarrow}}

=

\end{array}</math>

If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term.

If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term.