12,089
edits
Changes
Directory:Jon Awbrey/Papers/Differential Logic and Dynamic Systems 2.0 (view source)
Revision as of 21:32, 8 July 2008
, 21:32, 8 July 2008→Propositions as Types and Higher Order Types: spacing
| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math>
| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math>
|}
|}
<br>
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.
| <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>
===Reality at the Threshold of Logic===
===Reality at the Threshold of Logic===