Changes

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

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

! Observation 1

| '''Observation 1'''

|-

|-

| '''IF''' we know that the element <math>x\!</math> is of the type <math>X\!</math>

| '''IF''' we know that the element <math>x\!</math> is of the type <math>X\!</math>

|}

|}

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 "x", "f", and "f(x)"

are taken to be names of formal objects.  Some people will call

the latter usage, and recommend sticking with the first option.

In the same context, the notations "X", "X -> Y", and "Y" give us

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.

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", one may of course elect 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

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''.

functional arrow "->" as the logical arrow "=>", 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===