| 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. | | 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. |
| First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type. | | First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type. |