Changes

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.

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

|+ '''Table 3. Analogy Between Real and Boolean Types'''

 

|- style="background:ghostwhite"

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

! <math>\mbox{Real Domain}\ \mathbb{R}</math>

|+ <math>\text{Table 3.}~~\text{Analogy Between Real and Boolean Types}</math>

! <math>\longleftrightarrow</math>

|- style="background:#f0f0ff"

! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>

| <math>\text{Real Domain}~ \mathbb{R}</math>

| <math>\longleftrightarrow</math>

| <math>\text{Boolean Domain}~ \mathbb{B}</math>

|-

|-

| <math>\mathbb{R}^n</math>

| <math>\mathbb{R}^n</math>

<p><math>\mbox{Transformation}\!</math></p>

<p><math>\mbox{Transformation}\!</math></p>

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

|}

 

<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&ndash;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&ndash;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.