Changes

Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic.  This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How].  In another formulation it says that terms are to types as proofs are to propositions.  See [LaS, 42–46] and [SeH] for a good discussion and further references.  To anticipate the bearing of these issues on our immediate topic, Table–3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question.

Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic.  This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How].  In another formulation it says that terms are to types as proofs are to propositions.  See [LaS, 42–46] and [SeH] for a good discussion and further references.  To anticipate the bearing of these issues on our immediate topic, Table–3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question.

{| align="center" border="1" cellpadding="4" 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%"

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

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

|- style="background:ghostwhite"

|- style="background:ghostwhite"

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

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

! <math>\longleftrightarrow</math>

! <math>\longleftrightarrow</math>

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

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

|-

|-

| '''R'''^''n''

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

| Basic Space

| <math>\mbox{Basic Space}\!</math>

| '''B'''^''n''

| <math>\mathbb{B}^n</math><sup>

|-

|-

| '''R'''^''n''&nbsp;&rarr;&nbsp;'''R'''

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

| Function Space

| <math>\mbox{Function Space}\!</math>

| '''B'''^''n''&nbsp;&rarr;&nbsp;'''B'''

| <math>\mathbb{B}^n \to \mathbb{B}</math>

|-

|-

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

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

| Tangent Vector

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

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

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

|-

|-

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

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

| Vector Field

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

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

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

|-

|-

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

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

| ditto

| <font size="4">"</font>

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

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

|-

|-

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

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

| ditto

| <font size="4">"</font>

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

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

|-

|-

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

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

| Derivation

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

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

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

|-

|-

| '''R'''^''n''&nbsp;&rarr;&nbsp;'''R'''^''m''

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

| Basic Transformation

| <math>\mbox{Basic Transformation}\!</math>

| '''B'''^''n''&nbsp;&rarr;&nbsp;'''B'''^''m''

| <math>\mathbb{B}^n \to \mathbb{B}^m</math>

|-

|-

| ('''R'''^''n''&rarr;'''R''')&nbsp;&rarr;&nbsp;('''R'''^''m''&rarr;'''R''')

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

| Function Transformation

| <math>\mbox{Function Transformation}\!</math>

| ('''B'''^''n''&rarr;'''B''')&nbsp;&rarr;&nbsp;('''B'''^''m''&rarr;'''B''')

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

|-

|-

| ...

| <math>\ldots\!</math>

| ...

| <math>\ldots\!</math>

| ...

| <math>\ldots\!</math>

|}

|}

<br>

<br>