Changes

|}

|}

In this scheme of inference, the notations <math>^{\backprime\backprime} x \, ^{\prime\prime},</math> <math>^{\backprime\backprime} f \, ^{\prime\prime},</math> and <math>^{\backprime\backprime} f(x) \, ^{\prime\prime}</math> are referred to as ''terms'' and interpreted as names of formal objects.

In this scheme of inference, the notations <math>{}^{\backprime\backprime} x {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} f {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} f(x) {}^{\prime\prime}</math> are referred to as ''terms'' and interpreted as names of formal objects.

In the same context, the notations <math>^{\backprime\backprime} X \, ^{\prime\prime},</math> <math>^{\backprime\backprime} X \to Y \, ^{\prime\prime},</math> and <math>^{\backprime\backprime} Y \, ^{\prime\prime}</math> give us information, or indicate formal constraints, that we may think of as denoting the ''types'' of the formal objects under consideration.  By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.

In the same context, the notations <math>{}^{\backprime\backprime} X {}^{\prime\prime},</math> <math>{}^{\backprime\backprime} X \to Y {}^{\prime\prime},</math> and <math>{}^{\backprime\backprime} Y {}^{\prime\prime}</math> give us information, or indicate formal constraints, that we may think of as denoting the ''types'' of the formal objects under consideration.  By an act of "hypostatic abstraction", we may choose to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were.

If a moment's spell of double vision leads us to see the functional arrow <math>^{\backprime\backprime} \to \, ^{\prime\prime}</math> as the logical arrow <math>^{\backprime\backprime} \Rightarrow \, ^{\prime\prime}</math> then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called ''modus ponens''.  And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of ''modus ponens''.

If a moment's spell of double vision leads us to see the functional arrow <math>{}^{\backprime\backprime} \to {}^{\prime\prime}</math> as the logical arrow <math>{}^{\backprime\backprime} \Rightarrow {}^{\prime\prime}</math> then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called ''modus ponens''.  And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of ''modus ponens''.

===Commentary Note 2===

===Commentary Note 2===