12,080
edits
Changes
Directory:Jon Awbrey/Essays/Prospects For Inquiry Driven Systems (view source)
Revision as of 20:18, 21 January 2008
, 20:18, 21 January 2008→3.2. Differential Extensions of Propositional Calculi: markup
: d''U'' = <font size="4">×</font><sub>''i''</sub> d''A''<sub>''i''</sub> = d''A''<sub>1</sub> × … × d''A''<sub>''n''</sub>.
: d''U'' = <font size="4">×</font><sub>''i''</sub> d''A''<sub>''i''</sub> = d''A''<sub>1</sub> × … × d''A''<sub>''n''</sub>.
Here, dAi is an alphabet of two symbols, dAi = {(dai), dai}, where (dai) is a symbol with the logical value of "not dai". Each dAi has the type B, under the ordered correspondence {(dai), dai} = {0, 1}. However, clarity is often served by acknowledging this differential usage with a distinct type D:
Here, dA<sub>''i''</sub> is an alphabet of two symbols, dA<sub>''i''</sub> = {(da<sub>''i''</sub>), da<sub>''i''</sub>}, where (da<sub>''i''</sub>) is a symbol with the logical value of "not da<sub>''i''</sub>". Each dA<sub>''i''</sub> has the type '''B''', under the ordered correspondence {(da<sub>''i''</sub>), da<sub>''i''</sub>} = {0, 1}. However, clarity is often served by acknowledging this differential usage with a distinct type '''D''', as follows:
: D = {(dx), dx} = {same, different} = {stay, change}.
: '''D''' = {(dx), dx} = {same, different} = {stay, change}.
Finally, let U' = U x dU = <A'> = <A + dA> = <a1, …, an, da1, …, dan>, giving U' the type Bn x Dn.
Finally, let ''U''′ = ''U'' × d''U'' = <font face="symbol">á</font><font face="lucida calligraphy">A</font>′ <font face="symbol">ñ</font> = <font face="symbol">á</font><font face="lucida calligraphy">A</font> + d<font face="lucida calligraphy">A</font><font face="symbol">ñ</font> = <font face="symbol">á</font>a<sub>1</sub>, …, a<sub>''n''</sub>, da<sub>1</sub>, …, da<sub>''n''</sub><font face="symbol">ñ</font>, giving ''U''′ the type '''B'''<sup>''n''</sup> × '''D'''<sup>''n''</sup>.
All propositions of U have natural (and usually tacit) extensions to U', with p: U = Bn -> B becoming p: U' = Bn x Dn -> B. It is convenient to approach the study of the differential extension U' from a globally democratic perspective, viewing all the differential propositions p: U' -> B as equal citizens. Devolving from this standpoint, the various grades of differential forms are then defined by their placement in U' with regard to the basis A'. Extending previous usage, we say that p is singular in U' if it has just one satisfying interpretation in U'. A proposition p: U' -> B is called singular in U if its projection to U is singular in U, that is, if all its interpretations in U' share the same cell in U.
All propositions of ''U'' have natural (and usually tacit) extensions to ''U''′, with ''p'' : ''U'' = '''B'''<sup>''n''</sup> → '''B''' becoming ''p'' : ''U''′ = '''B'''<sup>''n''</sup> × '''D'''<sup>''n''</sup> → '''B'''. It is convenient to approach the study of the differential extension ''U''′ from a globally democratic perspective, viewing all the differential propositions ''p'' : ''U''′ → '''B''' as equal citizens. Devolving from this standpoint, the various grades of differential forms are then defined by their placement in ''U''′ with regard to the basis <font face="lucida calligraphy">A</font>′. Extending previous usage, we say that ''p'' is singular in ''U''′ if it has just one satisfying interpretation in ''U''′. A proposition ''p'' : ''U''′ → '''B''' is called singular in ''U'' if its projection to ''U'' is singular in ''U'', that is, if all its interpretations in ''U''′ share the same cell in ''U''.
Using the isomorphism between function spaces:
Using the isomorphism between function spaces: