Changes

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math>  One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math>  But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math>  The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "<math>\to\!</math>" and products "<math>\times\!</math>" with the respective logical arrows "<math>\Rightarrow\!</math>" and products "<math>\land\!</math>".  Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math>  One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math>  But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math>  The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "<math>\to\!</math>" and products "<math>\times\!</math>" with the respective logical arrows "<math>\Rightarrow\!</math>" and products "<math>\land\!</math>".  Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

Finally, examine the middle four rows of Table&nbsp;3.  These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''.  A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space.  In symbols, a vector field is a function of the form <math>\xi : X \to \bigcup_{x \in X} \xi_x</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\xi_x\!</math> [Che46, 82&ndash;83].  If <math>X\!</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of the type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math>  This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

Finally, examine the middle four rows of Table&nbsp;3.  These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''.  A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space.  In symbols, a vector field is a function of the form <math>\xi : X \to \textstyle\bigcup_{x \in X} \xi_x</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\xi_x\!</math> [Che46, 82&ndash;83].  If <math>X\!</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of the type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math>  This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

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%"

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

 

{| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%"

|- style="background:ghostwhite"

|+ <math>\text{Table 4.}~~\text{An Equivalence Based on the Propositions as Types Analogy}</math>

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

|- style="background:#f0f0ff"

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

| <math>\text{Pattern}\!</math>

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

| <math>\text{Construct}\!</math>

| <math>\text{Instance}\!</math>

|-

|-

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

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

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

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

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

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

|}<br>

|}

 

<br>

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

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