Changes

In a contextual, implicit, or paraphrastic definition of this sort, the ''definiendum'' is the symbol to be defined, in this case, <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime},</math> and the ''definiens'' is the entire rest of the context, in this case, the frame <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime},</math> that ostensibly defines, or as one says, is supposed to define the symbol <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime}</math> that we find in its slot.  More loosely speaking, the side of the equation with the more known symbols may be called its ''defining'' side.

In a contextual, implicit, or paraphrastic definition of this sort, the ''definiendum'' is the symbol to be defined, in this case, <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime},</math> and the ''definiens'' is the entire rest of the context, in this case, the frame <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime},</math> that ostensibly defines, or as one says, is supposed to define the symbol <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime}</math> that we find in its slot.  More loosely speaking, the side of the equation with the more known symbols may be called its ''defining'' side.

In order to find a minimal generic typing, start with the defining side of the equation, freely assigning types in such a way that the successive applications make sense, but without introducing unnecessary complications or creating unduly specialized applications.  Then work out what the type of the defined operator <math>\operatorname{T}</math> has to be, in order to function properly in the standard context, in this case, <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime}.</math>

In order to find a minimal generic typing, start with the defining side

of the equation, freely assigning types in such a way that the successive

applications make sense, but without introducing unnecessary complications

or creating unduly specialized applications.  Then work out what the type

of the defined operator T has to be, in order to function properly in the

standard context, in this case, (x(y(z__))).

Again, this gives:

Again, this gives:

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

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

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

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

<math>\begin{array}{l}

(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}}

=

(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}}

Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type,

Thus we have <math>\operatorname{T} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow (B \Rightarrow (A \Rightarrow C)),</math> whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

read as a proposition, is a theorem of intuitionistic

propositional calculus.

===Step 3 (Optional)===

===Step 3 (Optional)===