Changes

===Propositions as Types and Higher Order Types===

===Propositions as Types and Higher Order Types===

The arrangement of types collected in Table 3 (repeated below) serve to introduce the themes of ''higher order propositional expressions'' and the ''propositions as types'' (PAT) analogy.

The types collected in Table 3 (repeated below) serve to illustrate the themes of ''higher order propositional expressions'' and the ''propositions as types'' (PAT) analogy.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table&nbsp;4.  Observe how the function <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y\!</math> in the pattern, moves through its paces from the second to the first position.  In this way, the vector field <math>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_x\!</math> to the site <math>x\!</math> where it acts in <math>X,\!</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> of the same type.

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table&nbsp;4.  Observe how the function <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y\!</math> in the pattern, moves through its paces from the second to the first position.  In this way, the vector field <math>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_x\!</math> to the site <math>x\!</math> where it acts in <math>X,\!</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> of the same type.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:96%"

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:96%"

|+ '''Table 4.  An Equivalence Based on the Propositions as Types Analogy

|+ '''Table 4.  An Equivalence Based on the Propositions as Types Analogy

'''

'''

|- style="background:ghostwhite"

|- style="background:ghostwhite"

! Pattern

! <math>\mbox{Pattern}\!</math>

! Construction

! <math>\mbox{Construct}\!</math>

! Instance

! <math>\mbox{Instance}\!</math>

|-

|-

| ''X''&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;''Z'')

| <math>X \to (Y \to Z)</math>

| Vector Field

| <math>\mbox{Vector Field}\!</math>

| '''K'''^''n''&nbsp;&rarr;&nbsp;(('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;'''K''')

| <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K})</math>

|-

|-

|(''X''&nbsp;&times;&nbsp;''Y'')&nbsp;&rarr;&nbsp;''Z''

| <math>(X \times Y) \to Z</math>

| &nbsp;

| <math>\Uparrow</math>

| ('''K'''^''n''&nbsp;&times;&nbsp;('''K'''^''n''&nbsp;&rarr;&nbsp;'''K'''))&nbsp;&rarr;&nbsp;'''K'''

| <math>(\mathbb{K}^n \times (\mathbb{K}^n \to \mathbb{K})) \to \mathbb{K}</math>

|-

|-

| (''Y''&nbsp;&times;&nbsp;''X'')&nbsp;&rarr;&nbsp;''Z''

| <math>(Y \times X) \to Z</math>

| &nbsp;

| <math>\Downarrow</math>

| (('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&times;&nbsp;'''K'''^''n'')&nbsp;&rarr;&nbsp;'''K'''

| <math>((\mathbb{K}^n \to \mathbb{K}) \times \mathbb{K}^n) \to \mathbb{K}</math>

|-

|-

| ''Y''&nbsp;&rarr;&nbsp;(''X''&nbsp;&rarr;&nbsp;''Z'')

| <math>Y \to (X \to Z)</math>

| Derivation

| <math>\mbox{Derivation}\!</math>

| ('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')

| <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})</math>

|}

|}

===Reality at the Threshold of Logic===

===Reality at the Threshold of Logic===