Changes

find a minimal generic typing (simplest non-degenerate typing) of each term in the specification that makes all of the applications on each side of the equation go through.

find a minimal generic typing (simplest non-degenerate typing) of each term in the specification that makes all of the applications on each side of the equation go through.

For example, here is one such typing:

For example, here is one such typing:

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

{| align="center" cellpadding="8" width="90%"

  (y: (x: z:    ): ):  =   (x: (y: (z:    T:        ):    ): ):

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

<math>\begin{array}{l}

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

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

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

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

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

=

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

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

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

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

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

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

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

In a contextual, implicit, or paraphrastic definition of this sort,

In a contextual, implicit, or paraphrastic definition of this sort,

the "definiendum" is the symbol to be defined, in this case, "T",

the "definiendum" is the symbol to be defined, in this case, "T",