★暗算する?より(人形を)産むが易し?のジレンマ。

”型”の自己確証は可?不可?のジレンマ
〜「私って何型?」って自分で判断できるの?判断できるとは限らないの?〜
　
　は置いといて、
　
----------------------------------
　
　ある複雑な論理式があったとする。それさえ解ければ、アノ人へのpropose(命題)の答えがtかfか予め判断できるであろう。
　残念ながら、もし自分に適切な計算能力(;標的が明後日の場所に移動しちゃう前にとか)がない場合でも、それを知っていたら、そういう論理式を表現する機械の　設計図(情報)　と　部品　とを買ってきて、実際に作成して、問題解決を委任して、自分は実況検分(実験)と保守を決め込めばよい。それが工学技術者(別名「チェンジニア」)らしいやり方だ。
　――ぉぃぉぃ、そんなにproposeのジレンマを繰返すつもり?w　――いやいや! ただ『備えあれば憂いなし』なだけだってばw
　昔(ノイマン型以前)は、本当に、ある問題を解く毎に、その問題専用の「program一体型方式」computerをhardwareで造って実現していた、というのだから驚き!
　下記の 真理値表の関数を実現する物理ゲートdevice は、そういう単機能computerをbottom upに製造するやり方の全てである。さて、それ以上の
＜万能computer ;現在の「stored program方式」(ノイマン型)のcomputer
も、こういうロジックdeviceだけで製造できるかな?
　常識ではなく、自分の頭で考えてみると、非常に面白い。
　おそらくは、アナタがこういうロジックdeviceだけで造れるcomputerの何と役立たずに見えることか!
　／え、そんなの現実的でない?　*1
そう言うのなら、後半のように、その論理式の記号列を自分で形式的に手計算したり、予めtop downに、解法の見通しを立てて、様々な定理を駆使できるようにならなければ、問題は解けませんよ!　…どうもそれが、論理学者や数学者のやり方らしい。
　（でも、ちょっと待った。記号だけと格闘してても、真実は掴めないよ? 記号にすれば、大切なことが抜け落ちちゃうんだから。おまけに、もし証明が間違ってたとしても、気が付かないかも知れないよ!!
　／ぷんぷん。じゃあ、やっぱり論理ゲートで組立てちゃった方が早いわけ?? @@ぐるぐる〜!!
　
　
　
◆computerを作るw　＜単機能／万能
　動作原理や、論理式の値の求め方とかを知らなくても、はたまた物理ゲートの呼び名とか記号表記すら知らなくても、

  • 設計図(情報)と、
  • 物理ゲートdeviceの実物たくさんたくさん

がそこに用意されてれば、computerは組立てられることに注意。　――6石ラジオ キットみたいだなw　――ガンプラと違って、「動作する」し!
　
　
｛命題論理の演算記号の定義。(真理値表による定義)　*2
　2値論理学では、*3
　
† 0項0bit入力、1通り
0項関数R(つまり定数)は、2^(2^0)= 2コしかない。

(入力パターン)
　(なし)
(出力パターン　　　　　　　⇔関数(名))
＜任意の物理現象，抽象識別型，意味
;基準電位以下　　L 0 　　　　F(負論理解釈ならT)　―― F ⇔ ⊥
;基準電位以上　　H 1 　　　　T(負論理解釈ならF)　―― T ⇔ ⊥ ⊃⊥
――どんなに複雑な論理式であっても、入力が0bit(変数がない)なら、常に定数値(2通りのどっちか)しか返さない。
――定数マクロは、compile時に確定可能ということか。

　
　
†　1項1bit入力、2通り。
1項関数Rは、2^(2^1)= 4コしかない。
0項関数を差引くと、2コしかない。しかも、1コはnop。

(入力パターン)
　10: (Rq)
(出力パターン　　⇔関数(名))
　00　F
　01　　~q　not
　10　　 q　nop ――no operation　　;p≡(p≡q)は3項関数のように観えるが、1項関数まで堕ちてくる。
　11　T
　
――どんなに複雑な論理式であっても、入力が1bit(変数が1コ)なら、ある1項関数と同等。
　1bit入力関数の場合、任意の入力変数xと、任意の1bit入力関数RST…について、
　　　　Q x ≡ RST… x
となるような関数Qが存在する。
　
　たとえ2項関数が16コあったとしても、入力を実質的に1bitしか使ってないと、
＜対角的な用法　≒　1項1bit入力、2通り。
対角的な2項関数Rは、2bit、4コしかない。けっきょく1項関数になってしまう。
0項関数を差引くと、2コしかない。しかも、1コはnop。
3--0(入力パターン)
1--0:(qR  )　　――pを入れるところに、qをcopy。つまり偶々p≡qの場合。対称的な入力。実質的には1項関数。
1--0:( Rq)
　
( qRq の圧縮された出力パターン　⇔　関数名)　――左に右のが「縮退同化」されてる。あるいは、＜左から右に進化?
0--0　F　!⊃　!⊂　neq
0--1　　~q　　nand　nor　　――☆これでもって1項関数の ~q を定義できる。
1--0　　 q　　and 　 or　　――nop
1--1　T　 ⊃　 ⊂　 eq
　
( qRq の未圧縮の出力パターン　⇔関数(名))
0000　F　　F
0001　　~q　　nor !v
0010　F　　　　　　　　!⊃
0011　　~q　　~p
　
0100　F　　　　　　　　!⊂
0101　　~q　　~q
0110　F　　neq !≡
0111　　~q　　nand !&
　
1000　　 q　　and &
1001　T　　 eq  ≡
1010　　 q　　q
1011　T　　　　　　　　 ⊂
　
1100　　 q　　p
1101　T　　　　　　　　 ⊃
1110　　 q　　or v
1111　T　　T

　
　
† 2項2bit入力、4通り。
2項関数Rは、2^(2^2)= 16コしかない。――nandかnorの組合わせで他を定義できる。定数⊥があれば否定形でなくても大丈夫。

  • 対称的なものは　F，T，xnor(ないしeq)，xor(ないしneq)，and，nand，or，nor　の、8コのみ。
  • 非対称なものは　p，q，~p， ~q，⊃，!⊃，⊂，!⊂　の、8コのみ。

0項関数F，T，を差引くと、14コ。
1項関数(他項を無視なp，~p，q， ~q。2コ*2で)、　4コも差引くと、10コのみ。そのうち、

  • 対称的なものは　xnor(ないしeq)，xor(ないしneq)，and，nand，or，nor　の、6コのみ。
  • 非対称なものは　⊃，!⊃，⊂，!⊂　の、4コのみ。

　

3210(入力パターン)
1100: (pR )
1010: ( Rq)
　
( pRq の出力パターン　⇔関数(名))
0000　F
0001　　　　nor !v 　　　　　　　　　両否定↓
0010　　　　　p!⊂q　　;~p & q。　　　負論理の⊃。~p!⊃~q。
0011　　~p
　
0100　　　　　p!⊃q　　; p &~q。　　　負論理の⊂。~p!⊂~q。 
0101　　~q
0110　　　　xor，neq !≡　　　　　　　負論理の≡。~p!≡~q。
0111　　　　nand !&　　　　　　　　　非両立|　――cf 反対対当
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　――正論理と負論理とが、上下対称になっているのが興味深い。
1000　　　　and &　　　　　　　　　　;p≡p⊃q
1001　　　　xnor，eq ≡
1010　　 q　　　　　　　　　　　　;p≡(p≡q)
1011　　　　　p⊃q
　
1100　　 p　　　　　　　　　　　　;q≡(q≡p)
1101　　　　　p⊂q
1110　　　　or v　　　　　　　　　　　　　　　――cf 小反対対当
1111　T

――どんなに複雑な論理式であっても、入力が2bit(変数が2コ)なら、ある2項関数と同等。
;p≡p⊃qとか、p≡(p≡q)とか。

><

　
† 3項3bit入力、8通り。
3項関数Rは、2^(2^3)= 256個しか!ない。
――2項関数の組合わせで定義可能。
――どんなに複雑な論理式であっても、入力が3bit(変数が3コ)なら、ある3項関数と同等。
　｛列挙してー!?
　
　
　
† n項nbit入力、2^n通り。
n項関数Rは、2^(2^n)通りしかない。
　nが有限なら、、ゲーデル数によって、凡ての関数にindex可能。
　nが可算無限に行くと、、関数の個数は非可算無限に、index不可能。
*4
――どんなに複雑な論理式であっても、入力がn bit(変数がnコ)なら、あるn項関数と同等。
　
　------
　memory部分の作成につき、
＜flip-flopの「禁止入力」が、気になってたりする…。何か、純論理的でなく物理形態に依存してるような感じ。resetされる前はどう動いているのだろう…? 高性能だと、発振して電波出しちゃったりしてるのかな?
＜立ち上がり、とか立ち下がりとか、時間のアナログ関数になってるところも、純論理的ではないみたい。
　------
＜様相式についても、真理値表による評価は、可能?


　
　記号化　　　　――観察論理学?の創設?
( 各computer内で蠢ける記号 と、我々の観察論理学の用語 の定義)
◆　(様相)記号式の定義　*5
　記号式　とは、有限の記号列であり、まず、　　　　　　――再帰的定義や、再帰的証明が可能

  • ⊥は記号式である。　　　　　　　　――論理矛盾を表わす記号。　　　　――nilかよ。
  • a, b, c,...は記号式である。　　　　――変数を表わす記号。　　　　　　――symbol atomかよ。
  • XとYとが記号式ならば、(X⊃Y)も記号式である。――含意関係を表わす記号。――list(cons)かよ。
  • Xが記号式ならば、A(X), B(X), C(X),...は(様相式という)記号式である。――様相関係を表わす記号。――新機軸?

以上で全部である。
　記号文　変数記号を含まない記号式
――　記号式を(意味)評価した場合の「真理値」と全く無関係に、形式的に定義できてしまったことに注意。
　computerは、(真偽など)記号の意味にお構いなしに、既存の記号式と、予め定められた推論規則に従って、定理ないし認識を確証していくだけである。ただし、ある妥当な解釈の下に、もし既存の記号式が真であったならば、続いて確証された記号式は、(真理値表でも、事実を観察して追跡してみても)同じ解釈の下に、例外なく凡て真である!!　(ように我々はcomputerの推論規則をprogramする)　／外界観察則だけは、"蓋然的に"真であるにとどまる。
――「記号式」という言葉は、我々がcomputer内部について語るときの言葉である　ことに注意。――我々は造computer主ね。
　もし我々がcomputer内部を観察することができず、語る言葉も知らず、製造修理改良できなかったとしても、
いったんcomputerが製造されてしまえば、それは壊れるまで動き続ける。
　他方、computerは、自分の内部について語るための、こういう言葉を必ずしも知らないが、それでも普通に動作する。
ただし、computerが確証する、ある記号式を他のcomputerや自分が観察して解釈すると、たまたま、自分や他者の状態を語っているようにとれることも多分にあり得る。;computerBやCが、「B」を含む記号式を確証した場合。
　
　
　――「( )」が省略されているとき
＜違う関数記号式が連続した場合の、優先順位
高)　B類，~，&類，v類，⊃類，≡類　(低
　
＜同じ関数記号式が連続した場合の、優先順位
　&類v類　副作用なければ同じだけど、とりあえず
　　　　　　左付　; (p&q)&r
　⊃類≡類　　右付　; p⊃(q⊃r)
　~ 　　　　　右付　; ~(~(~p))
　 B類　　　　右付　; B(B(Bp))
　
　
‡｛命題論理の演算記号の定義。(primitive原始記号(形式定義放棄記号)から形式的に始める定義)　――けっきょく、
(左辺　　≡　　右辺)が、恒真式になるという意味。

pとか　　　　個々の命題。p≡T。(p≡T)≡T。((p≡T)≡T)≡T。　　　―― (x≡T)は 1周期不動点を持つ。多値論理でも成立つ。
　　　　　　　　　　　　　　　 (p≡g)≡g (goodman恒真式)。　(((p≡g)≡g)　≡g)≡g 。―― (x≡g)は 2周期
　　　　　　　　　　　　T&p。Fvp。　p&(pvq)。　pv p&q。　(p⊃q)⊃p。
　　　＜評価値　観察とか接続とかで、割付けられた値、すなわち、⊥、または⊥⊃⊥、または、値無し(現時点で不明)。
　
　
⊥　　(原始記号)　　　――馴染み深いnotからではなく⊥から始めている。非古典論理? 
　　　＜評価値　⊥。――その意はfalse(偽)。
　　　〔任意の、論理矛盾、恒偽式、空虚nil。不可能を意味する記号。どんな宇宙にも存在し得ないが、観念しうるもの。アレの反対w?
　
~p　　　　　p⊃⊥。　p≡⊥。((p⊃⊥)　⊃⊥)⊃⊥。((((p⊃⊥)　⊃⊥)⊃⊥)　⊃⊥)⊃⊥。
　　　　　　　　　　　　　　―― ~xは 2周期不動点を持つ。多値論理でも、完璧な論理否定であれば、成立つ。
　　　　　　＜pの論理否定。not(p)。pではない。　――背理法・無矛盾律 的な定義。
〔　　　　　　　　　　　　　　　　　　　　　　――非古典論理では意味がズレてくることになりそう
〔　　　　 (p⊃⊥)⊃~p　　　~(p⊃⊥)v ~p。　~~p v~p。　pまたは~p、は必然(排中律)。
〔　　 ~p⊃(p⊃⊥)　　　　　~pならば、pは不可能。~pかつpは不可能(無矛盾律)。
〔――定義の両辺を否定
〔 p　⇔　 (p⊃⊥)⊃⊥
〔　　　〔* ~p … →⊥〕以上より、~p⊃⊥。~~p。つまり、pは真(背理法)。
　
 T　　　　⊥⊃⊥。つまり~⊥。対偶反転すると、~⊥⊃~⊥でT⊃T。任意の恒真式tautology。
　　　＜評価値　T。――その意はtrue(真)。
　
p ⊃q　(原始記号)
　　　＜評価値　pの評価値が⊥　または、qの評価値が⊥⊃⊥　ならば、評価値⊥⊃⊥。そうでなければ評価値⊥。
　　　　　　　　　　　　　　　　　　――＜循環定義?　／定義ではないし、底もある。評価操作の手順に記号「⊃」が出てくるだけ。
　　　　　〔pが偽か、qが真のときにのみ、「真」と評価される記号式。　ならば。pはqを含意する(メタ意)。
　　　　　　　　　　　　　　　　　　　　　(――非対称　 ⊂　ばらな、　　　逆含意)
　　　　　　〔T& p ⊃q v⊥　と補っておくと、対偶移動を一般化できる。;ド モルガンの法則
 　　　　　　p!&~q。　 ~q ⊃~p。　~p v q。((――集合論の逆?　pが真なものの集合ならば、部分集合のqもそうである。と解釈するのか?))
p!⊃q　　　　p &~q。　 ~q!⊃~p。　~p!v q。　　　　　　　　　ノットならば。ならば…ということは、ない。pはqを含意しない(メタ意)。
　　　　　　　　　　　　　　　　　　　　　(――非対称　!⊂　ノットばらな。ばらな…ということは、ない。…逆含意しない(メタ意)。)
　　　　　　　　　　　　　　　　　　↑pを対偶移動すると、T!⊃~pvqだから、T& ~p!v q。
　　　　　　↑qを対偶移動すると、p &~q !⊃⊥。
　　　　　 「xは⊥を含意し　ない」(x　　⊃⊥)⊃⊥　　≡x(つまり~~x≡x)はttだから、単にx。
　
p vq　　 (p⊃q) ⊃q。　~p ⊃ q。　T!⊃p!vq。　~p!&~q。　　　または。(両立的)論理和or　少なくとも一方が成立つ。
p!vq　　 (p⊃q)!⊃q。　~p!⊃ q。　~(pvq)。　　~p &~q。　　　　pノットまたはq。pでもqでもない。　　nor両否定。
p &q　p ≡p⊃q ※　　　 p!⊃~q。　~p!v~q。　　p&q!⊃⊥。　　かつ。論理積and。　(※curry恒真式(仮))。
　　　　　　　　　　　↑pは~qを含意しない。――もし含意するなら~qで、p&qでなくなるし。
p!&q　p ≡p&~q　　　　　p ⊃~q。　~p v~q。　~(p&q)。　　　　　pノットかつq。　pでないかqでないか。nand非両立。
　
p  ≡ q　　　　　　　 (p ⊃q)&(p ⊂q)。　 p &q v~p&~q。　p vq　⊃ p &q。　p!&q　⊃p!vq。
　　　　論理値が　同値(メタ意)(平行対称)。　　両方揃ってのみ成立ち得る。　　　負排他的論理和xnor。((非同値を表わす演算子に!))
(　⇔　「(左辺)が成立つ　ならばそのときにかぎり　(右辺)が成立つ」という"日本語の"略記。　ならな　ならばば　if( and only i)f。　)
p !≡ q　　　p≡~q。　(p!⊃q)v(p!⊂q)。　(p!&q)&(p vq)。　p vq !⊃ p &q。　p!&q !⊃p!vq。
　　　　論理値が非同値(メタ意)(交叉対称)。　　一方だけ成立って他方は成立たない。排他的論理和 xor。
　　　　　　　　　　　(p⊃q)⊃(p!⊂q)
　　　　　　　　　　　(p⊂q)⊃(p!⊃q)


記号式の(評価)値　ある記号式DATAを、programとしての扱いで評価機構に渡したら、返ってきた値。
記号式の評価　　　所定の形式的決定手続により、記号式の値を求めること。
(評価eval操作　の定義)
　　　　computerBで、
　　　　環境Envの下に、
　　　　記号式f(p,q,r,...)を評価する 操作
とは、次の評価値を得られる操作。
　　computerBを、
　環境記号式Envの実体を看取し得る所定の環境に置いたり、
　所与の前提として、環境記号式Envを入力した場合に、
　　もし fが　⊥　　　なら、　fの値は、F。
　　もし fが p,q,r,...なら、　fの値は、たとえば p、の逆記号化が、Bの近傍世界で事実と合致して正しければT。そうでなければF。
　　もし fが g⊃h 　　なら、　fの値は、gp(...)の評価値がFであるか、hp(...)の評価値がTであれば、T。そうでなければF。
　　もし fがB(g)　　　なら、　fの値は、gがBで確証されるまで機会を待って、Tを返す。　　――こんなんで動くのか?
　　　　　　　　　　　　　　　　　　＜~gがBで確証されるまで機会を待って、Fを返す。　　――整合かつ安定の自己仮定!
　　　　――問われる毎度に、とりあえず「現在〜につき案件保留中」を返す?
以上により、もし値が求められたら、記号式Envが直接入力だったら削除してから、値を返す。　　――手計算かよ；
　
　
　
tt　恒真式tautology　――これも注釈用。恒真式が何かを定義できなくても、computerは動く。
　式に含まれる各々の自由変数の値がT(rue)，F(alse)のどちらをとろうとも、常に論理値Tを返す記号式
　
――記号の世界と、実体の世界とを 峻別 してしまった報い。
＜恒真式とは?　　　　　　　　　　　　　　　　　そもそも＜真とは

  • ◎形式主義(演繹的?　先験主義?　定義主義?)

　　　→*6公理式だけを前提に、*7機械的な導出規則によって、結論された記号式。(論理学の一定の範囲で、凡ての実質的意味の恒真式が導出できるように、仕組まれている(完全性定理))　――＜自明≡必然的?
　　　　――「真」の定義は、とりあえず不要

　　→実際に、値を求めてみると、だれがいつどこでどんなときでも普遍的に、真理値T を返す記号式。
　　 ;真理値表主義　→凡て(nコ)の命題の、真理状況の凡ての組合わせ(2^n通り ――非可算無限；)のいずれにおいても、真理演算関数の定義から、その評価値が真Tとなる記号式。　(――変数3コまでなら、こっちも早い?)
　　　　――「真T」と「偽F」の定義が一応必要。逆転させると負論理。実は「+極と-極は逆だった?」と発見されたりしてw
＜完全性定理が成立つ範囲では、両者は一致するので、備えてくれて憂いなし。　;命題論理、一階述語論理
＜様相記号を含んでくると、複雑化。

  • (Ⅰ型のcomputerが)命題論理によって公理から導出できる記号式　*8
  • (任意のKripkeモデルの)任意の具体的可能世界で成立つ :確立された記号式。

　(任意の型の)　　　　　任意の具体的computerで(正しく)確証される記号式。
　

;＜ Bx≡Bx は、恒真式か?
- 恒真式 q≡q の形から、qをBxで置換えて導けるので、恒真式。両辺が文字通り同じことから「≡」が成立つ。
　　　――Bxの真偽は必ずしも明かでないが…。
- 評価主義から、再帰呼出しで、Bxの値を評価しようとすると、
　　☆「B」を「遅かれ早かれ」Bがxと確証する(証明可能性)、と意味づけたい場合、
　　＜盲目的に T が観察されるまで待たなければならないとすれば、
　　恒真式 かどうか、必ずしも判別できない。――xの内容と、Bの知識とか、Bのcomputer型による。
　　　――たとえ実際にBを走らせてみても、Bxの真偽は、mortalな人間に判るとは限らない。
　
＜Bがxを確証した場合(eval(Bx)==T)は、T≡Tの値としてTが返る。ので、(整合性の問題は置いといて、)とりあえず良し。
／その他の場合は…… ；
(凡てで2bit4通り)　→1コの論理否定は他の3コ。2コの論理否定は他の2コ。
 B B
 x~x
 00 　Bが(xも確証せず、~xも確証しない) ので、xにつき不完全
　　　　――single taskなら帰ってこない(無限loop，底無再帰，bug，熱暴走，etcetc)。
　　　　――00の場合、4通りのどれなのか、観察によっては、有限時間内には判別できない。
　　　　　　　　――debuggerで、強制disclosureさせられれば、解り易いけど。
 01 　Bが(xは確証せず) ~xを確証。　　　　　　　　　――効率重視で停止させたいなら、整合自己仮定を置く。
 10 　Bが xを確証、　 (~xは確証しない) 。　　　　　――効率重視で停止させたいなら、整合自己仮定を置く。
 11 　Bが xも確証、　　~xも確証して、不整合。　――整合自己仮定があれば、ここには来ない。
　
　☆　(カッコ内の事実~B-は積極的現象として観察できない)ので、3つに観える。――
さらに、
　☆　整合性自己仮定が置かれていると、他方のx(ないし~x)の検査を怠るので、2つに観える!
　
　
 B　　＜Bxと事実xとの関係
 xx 　　　　　(Bx)　　　　　　　(x)　　　(Bx⊃x)　　　　(x⊃Bx)
 00 　~B&x　　Bが xを確証せず。同~x。　xにつき正確　　　　　完全
 01 　~B&x　　Bが xを確証せず。違 x。　xにつき正確。　けど不完全。
 10 　~B&x　　Bが xを確証。　　違~x。　xにつき不正確。　　　完全
 11 　 B&x　　Bが xを確証。　　同 x。　xにつき正確。　　　　完全

　
｛命題論理について　
　観察論理学の理解には、computer言語の" if 文"が自信を持って書ける程度の論理力で十分です。述語論理も扱いません。
*9
が、ここでは命題論理の理論的基礎と実践を包括的に説明するのには力不足なので、
　形式的にしっかりやりたい人は
参考URL　http://www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/index.html
*10
*11
*12
　
　
† (様相記号) ―― "Logic of provability", or "Logic of Inter-Cognitivitiy" ?
環境世界　あるcomputerを含まない、そのcomputerの観察の届く物理世界。
近傍世界　あるcomputerを含んだ、　そのcomputerの観察の届く物理世界。　　*13
BX　　(原始記号　box [B])　BがXと確証する。~XはBで反証される。~XはBと整合しない。――cf. Xは必然的に真。
　　　　　　　　　　　　　　　　　　　　　　　　　　;BBX　BがBXと確証する。
　　――(観察v推論して)　認識する、信じる、確信する、証明可能である　――遅かれ早かれ
　　――箱詰関数の結果を表わす記号　「近傍の具体的事実が、抽象的記号Xに変換され、computerBという箱に詰込まれた」
(B├X　　「BがXと確証する」という"日本語の"略記　　; B├BX　BがBXと確証する。)
　　――Xを確証しているからといって、Xが客観的現実に合致して真であるとは限らない。
~BX　　　　BがXと確証しない。　　　　　　　　　　　　　;~BBX　BがBXと確証しない。
(B !├X　　「BがXと確証しない」という"日本語の"略記　　; B !├BX　BがBXと確証しない。)
~B~X　　　(diamond < B>)　Bは~Xを確証しない。XはBで反証されない。XはBと整合する。　――cf. Xは可能的に真。　*14
様相式、様相記号式　　　　様相記号を含む記号式
様相文　変数記号を含まない様相式
(X中の)部分記号式Pが〔Bについて〕様相化されている　　様相式Xの中のPの凡ての出現が、〔様相記号たとえば〕Bのscope内にあること

(様相文の例)　Bは整合なG型　と仮定すると、
　~B⊥　〔⇔~B~T〕Bは整合。　　　　　　　　　　　　　　　　　――真だが、　Bで確証されない。
　　　　 B~B⊥　　Bは 上の行の事実 を確証する。　　　　　　　――偽。(← 上の行の事実を確証するとBは不整合になってしまうから。)
(B) ├
　~B⊥⊃~B~B⊥　　Bは整合ならば、Bは「Bは整合」と確証しない。――真であり、Bで確証される。(⇔ Bは左の記号式ないし事実につき正確。)
B(~B⊥⊃~B~B⊥) 　Bは 上の行の事実 を確証する。　　　　　　　――真であり、Bで確証される。(⇔ Bは左の記号式ないし事実につき正確。)
┤
  • -

　
｛　BX と X との関係
B& X　　B X & X。　BはXを正認する。正しく確証する。Bの証明結果は現実と合致して正しい。
B@~X　　B~X & X。　Bは誤りの~Xを認める。~Xと誤認。 Xを観誤る。Bの証明結果~Xは現実 Xと合致せず間違い。
B@ X　　B X &~X。　Bは誤りの Xを認める。 Xと誤認。~Xを観誤る。Bの証明結果 Xは現実~Xと合致せず間違い。
Bv X　　B X v X。　BはXに反逆的。Xに保守的ではない。
　
　
--
B X　≡X　　　BはXについて完璧に理解する。Xないし~Xについて　正確かつ　完全。
B X !≡X　　　BはXについて完璧に誤解する。Xないし~Xについて反逆的かつ虚言的。
　
B~X　≡X
B~X !≡X
　

><
「BXならば〜」
　 B X ⊃ X　　~X⊃~B X　　　~B X v X　Bは Xに　正確。 Xと　誤認しない~B@ X。　correct! ――専門用語でいう「健全sound」性に近い
　~B X ⊃ X　　~X⊃ B X　　　 B X v X　Bは Xに反逆的。 Xに保守的でない Bv X。
〔 B~X ⊃ X　　~X⊃~B~X　　　~B~X v X　Bは~Xに虚言的。~Xと　正認しない~B&~X。
〔~B~X ⊃ X　　~X⊃~B~X　　　 B~X v X　Bは~Xに　完全。~Xに不完全でない。
 --
　 B X ⊃~X　　 X⊃~B X　　　~B X v~X　Bは Xに虚言的。 Xと　正認しない~B& X。
　~B X ⊃~X　　 X⊃ B X　　　 B X v~X　Bは Xに　完全。 Xに不完全でない。
〔 B~X ⊃~X　　 X⊃~B~X　　　~B~X v~X　Bは~Xに　正確。~Xと　誤認しない~B@~X。
〔~B~X ⊃~X　　 X⊃ B~X　　　 B~X v~X　Bは~Xに反逆的。~Xに保守的でない Bv~X.
　
 ----
「BXならば〜」の論理否定
　 B X !⊃X　　~X !⊃~B X　　 B X &~X　Bは誤りの Xを認める。　 Xに不正確 B@ X　 Xと　　　　誤認。
　~B X !⊃X　　~X !⊃ B X　　~B X &~X　Bは誤りの Xを認めない。 Xに保守的~Bv X　 Xに反逆的でない。
〔 B~X !⊃X　　~X !⊃~B~X　　 B~X &~X　Bは正しい~Xを認める。　~Xと　正認 B&~X　~Xに虚言的でない。
〔~B~X !⊃X　　~X !⊃ B~X　　~B~X &~X　Bは正しい~Xを認めない。~Xに不完全 　　　~Xに　完全でない。
 --
　 B X!⊃~X　　 X !⊃~B X　　 B X & X　Bは正しい Xを認める。　 Xと　正認 B& X　 Xに虚言的でない。
　~B X!⊃~X　　 X !⊃ B X　　~B X & X　Bは正しい Xを認めない。 Xに不完全 　　　 Xに　完全でない。
〔 B~X!⊃~X　　 X !⊃~B~X　　 B~X & X　Bは誤りの~Xを認める。　~Xに不正確 B@~X　~Xと　　　　誤認。
〔~B~X!⊃~X　　 X !⊃ B~X　　~B~X & X　Bは誤りの~Xを認めない。~Xに保守的~Bv~X　~Xに反逆的でない。

　
　
　
(理論的背景)http://ja.wikipedia.org/wiki/%E6%A7%98%E7%9B%B8%E8%AB%96%E7%90%86%E5%AD%A6
――　様相記号としては、ふつう□とかが使われる。
――　N(ecessarily)を使えば、――「必然的に真」とか。――「可能世界」とかね。哲学的@@
―― しかし、本稿では、ゲーム理論の各playerの心理・行動の決定分析が深まればいいだけの話なので、
様相システムGの系譜に妥当する意味を与える。つまり、「B」を、(数学;peano算術とか)論理システム(≒機械computer)において「証明可能」BeweisbarのB(というかBeliefのB?)の意から転じて「認識／確証する」の意とする。□(box)のBでもあるし。いや、人の思考を形式化formalize□して、囚人としてinternする□かw。――なんかこの単語にも不動点「人」が観えるぅ〜
――　「B」をBさんの「B」と読むことが、☆複数人の認識の相互関係を形式化するのに、不可欠なのでw　――記号の革新的な使い方だね♪
　
(タルスキの(断片的)真理定義T)
(記号化)
x:　　　　「雪が白い」　　――引用符「」を省略すること多し。厳重注意。
　　　　　　　　　　　　　;改行強調してある場合，日本語の文脈でabcが出てくるなど明か?な場合 *15
＜ xの真偽判定
　記号式ないし情報(idea?)(台詞、発話)　　――形而上的、内部的内心的で、現に書かれ話されなくても。
　　　　x ないし「雪が白い」　――(我々による記号の引用・言及などで通じた)記号世界の事象と
が　　真である　　のは、　　　　　　　　　――True(x)は、実はTrue(x, y)だったってこと?
　　　　(実際に)　雪が白い　　――(我々による記号の評価・使用などの結果の)現実世界の事象と(あるいは、ある可能世界の…
ならばそのときに限る。　　　　　　　　――の1対1対応を受容れるってこと。
　そして、2値論理(ジレンマ)なので、真である とは、偽でないこと。逆も同じ。
　
＜Bxの真偽判定
　記号式ないし情報
　　　　　　Bx　ないし「Bがxを確証する」　――記号世界の事象
が　　真である　　のは、
(実際に)　B├x　ないし　Bがxを確証する　　――現実世界の事象　　＜我々から観て?
ならばそのときに限る。
　
＜Bxの値を求める(eval)実験操作
　computerBを、所定の環境に置いたり、所与の前提入力を与えて、観てみて、
　　　　遅かれ早かれ、Bがxを確証する
ならばそのときに限り、 Bx の値は真true。
そうでないときに限り、 Bx の値は偽false。
――おっと、有限時間内に判るとは限りませんね ； まったく人間ってヤツは。。。　だからこれを「algorithmによる解法」とは呼ばない。
／しかし、高レベルのcomputerは、(自分や他人で)実験しなくても、様相式の単なる計算によって、その種の事実を知っていることがある。




(computerたちの世界)

  • あるcomputer物体をmediaとしてその上に蠢く"記号世界"
  • "自然物理的世界(とその一部たるcomputer物体たち)"

　Bという記号は、computerBについて、両世界の関係を表現する関数記号である。(証明論の記号から転用)
これを使うと、従来は外界のことしか記号化できなかった(記号化できなければ何もできない)computerが、
　　　　自分と近傍世界(自分+環境世界)との関係　――再帰的であっても!
を記号的に押潰し内部化して取扱うことができるようになる。
　これを区別することで、意識的に対角線論法(Gの公理)を使うことができる。;数字と数を使って、整数の実数に対する不完全性を証明するようなもの。
　
(人間たちの世界)
　記号を見・聞きすると、直ちに実体的な意味を取りだしてしまう。――脳の中では記号的に処理している(はずな)のに。
つまり、記号を、その意味する実体と容易に混同してしまう。多くの論理的パラドックスのもと。
;qと、qが証明可能なこととの混同とか。←→　pと、pが真と、「pが真」は真…とは同じことなのだが……




† 推論規則(とその記号)　　*16
　――programとか状態推移関数と言っていい。
　――Ⅱ型Ⅳ型G型のように、推論規則をDATAに矮小化し自認して、「自分の殻を脱皮(自己認知能力の深化」することも可能。
　
　
　→　三段(推論規)則modus ponens　　　　(その特殊例) ;⇒
　　　　「X」と、「X⊃Y」とから、「Y」を確証すること。　　　　　　　　――非対称的
　
　((((　様相式の置換え定理　))))　　　　　　　　　　(普通の置換え定理、置換え推論)
　　　　　　　　　　　　　　　　 ―― f-p( )に様相記号が含まれなければ、Ⅰ型でも同様。
　
　　　　ⅢB├ X≡Y 　ならば　B├ fp(X)≡fp(Y)　。ただし、f( )は任意の論理式
　
――　この定理から、次の推論規則を使って論証過程を略記できる。
　⇒　置換え推論、同値推論、可逆推論　(則)
　　　　「f(X)」と「X≡Y」とから、「f(Y)」　を確証すること。すなわち、　――対称的
　　　　確証された記号式の部分記号式について、
　　　　　　　　　　　その部分記号式と同値性が確証されている記号式によって、
　　　置換え(代入)した記号式を確証すること。
　
〔(様相式の置換え定理の自己確証)
〔　　　――cf.Ⅱ型は、「三段推論を使える」と確証している。
〔　Ⅳ型のBは、「自分は置換え推論を使える」と確証している。すなわち、
〔　　　　ⅣB├ B&(X≡Y) ⊃( f(X)≡f(Y) )　。
　
　
　(様相記号を増やす推論規則)
(観察直観(認識規)則、観観測)
　――　　　　　　　　　　　　　　computer物体をmediaとしてその上に蠢く"記号世界"
　――"自然物理世界(とその一部たるcomputer物体)"
のレベルの差を、明確に区別することが大切。
(箱詰関数)　近傍の具体的事実を、記号に抽象化し、computerBという箱に詰込む!
――箱詰め関数0　最外殻の箱Bの外にあるモノを、写像して、新たに、最外殻の箱Bに箱詰めする。*17
　…>　外観則:環境世界観察(;他者観察)　環境事実Xを、観察して、記号式「X」を確証すること。
　
――箱詰め関数1　最外殻の箱Bの中にあるモノを、copyして、透明な小さな箱「B」に詰めて、最外殻の箱Bにしまう。
　->　内観則:自己直観、正常性　たとえばBが、

  • 「X」から、「BX」を確証すること。別の観方で言えば、
  • 「X」の基底たる物理事実としての内部事実*18を、自己観察?して、「BX」を確証すること。

　
(　)　正常性自認からの推論規則　たとえばBが、　　　　――Ⅲ型なら必要なし。
　「BX」から、「BBX」を確証すること。
　
　
　
　(様相記号を減らす推論規則)
(??)　正確(推論規)則　　　　たとえばBが、
　　「X」(Bを含まず?)から、"実際にXになる"ように、行動すること。　――B(0)が「B(-1)」にまで減る。外部観察則の反対。
すなわち、近傍世界を、自分の認識Xに合致するように変更する推論?行動規則(実現的?抑圧的?独裁的?唯脳論的??)。
　内部状態の自己認識に応じて、「自発的に」状態を変えていく心理や行動のprogramも可能である。
　　今私はここにいて、
　　ここから補給所に行くまでに、私の燃料が足りなくなりそうだから、
　　今から、補給所に、私の場所(という自己認識と物理状態と)を移動する。
　　　　　とか。　――ホントにそうなったどうかかは、外部観察則によって、feedbackして確認する。
　　＜他のcomputerの認識を実現させてあげる推論規則は?　;茉莉ちゃん「サンタはいる」
　
=>　安定(推論規)則　　　　たとえばBが、
　　　　「BX」から、「X」を推論すること　　　　――正常性、内部観察則の反対。
　　　　―― 「BX⊃X」を公理DATAとして持つよりは、弱い。論理矛盾に陥る危険も少ない。
　
-L>　レーブ(推論規)則　　　たとえばBが、「BX⊃X」から、「X」を推論すること




† 公理式と基礎的定理式

  • 公理axiomには、
    • *19
    • 「〜公理式」　システムに予め証明確証されている記号式　しかないが、　　　　――成文憲法?
  • 定理theoremには、2種類ある。
    • 「〜定理」　　システムについて観察して実証/論証される我々の言葉による定理

　　　;ある記号式Xを証明すれば、別の記号式Yを証明する　とか有象無象。;レーブの定理

    • 「〜(定理)式」　システムによって証明される記号式としての定理式

――　システムの記号化形式化能力が高いと、我々の証明を模倣して、定理式に取込める♪
　　　　*20
　　　　*21
　
(「世界はcosmos」「T系事実は実在する。それ以外の可能な事実はとりあえず知らない」))
Ⅰ)　任意の恒真式　――お好みの公理系の命題論理計算機が実装されている。
　　　　――「 B(tt)」 は恒真式ではないが、「B(X)≡B(X)」などの記号式は、その「p≡p」などの形から、恒真式として自動生成自動検証可能。Ⅰ型のcomputerは、直接入力によって教えられない限り「B(X)」の値を求められないのに、B(X)≡B(X)という真実を予め知っている! ――「当り前」って言うなyo!
　　　　――整合なⅠ型のBは、「⊥系事実は実在しない」と知っている　のと結果的に同じ。(Bの辞書に⊥は永劫に追記されない)
　　　　――／上の行の事実(~B⊥)を、ゲーデル的で整合なBは、知らない。(第二不完全性定理)
　
------------------------------------------
｛ computerBに関する記号式
　
(「Bは恒真式を自認」　　――恒真式確証式)
Ⅱ)　BX (ただしXは任意の恒真式) *22
　　　　――「B(tt)」 は恒真式ではないが、BがⅡ型ならばその値は真t。
　　　*23
(「Bは三段推論を使える」――様相記号分配式)
Ⅱ)　BX & B(X⊃Y) ⊃BY
　　　　　B(X⊃Y) ⊃(BX ⊃BY)　でも同じ
　
　
(「Bは外部観察則を使える」――環境観察式)
＜　Bは、「X⊃BX」の形の凡ての記号式を確証する。
＜ただし、Xは、
　　　　　BによるXの「観察蓋然条件」を充たす、Bの環境世界の事実
　を表わす記号式。＜「B」を含む可能性あり。
＜必要? ／事実をそのまま記号化できるならば、不要?　／他者観察には必要
＜観察蓋然条件

  • 観測事実Xとの適合 観測装置、機能整備
  • 観測射程距離
  • 遮蔽隠蔽物など、障害なし
  • 注目など、注意の集中　;予告・前兆ありか、突然不意にか
  • 擬態など錯覚なし
  • 観察後受動反応(気付いた動作行動など、相応の状態推移)

　etc,......
　
　
(「Bは内部観察則を使える」――内部観察式)
Ⅳ)　　　BX⊃BBX
(「Bは置換え推論を使える」――置換え定理式)
Ⅳ)　　　B&(X≡Y)　⊃(f(X)≡f(Y))　(ただし、f( )は任意の記号式。)
　
　------
(「Bは安定」　　――安定性確証式)
　　　　 BBX⊃BX　　　　　　　　――＜G系との整合性に疑念が…
　
(「Bは正確」　――正確性確証式、Xの自信過剰命題)――Bの定理式であればBは自信過剰。
T)　　　　BX⊃ X　　　　　　　　―― G系と不整合!!
　　　　　　　　　　　　　　　　――論理矛盾に陥る危険も多い。不正確になる危険も多い。
　
　------
(「Bは反射的」――反射同値式)
R)　　　k ≡ Bk⊃q　　　　を、(任意のqについてkがあって)確証する。――G系。
　
(「Bはレーブ推論則を使える(謙虚)」――Gの公理式)
G)　　　B(BX⊃ X) ⊃BX




◆computerの型
＜以下の能力を持つcomputer B のType階層分類
　　　　――下に向かうほど「万能」度が高い。外側だけでなく、内側への観察能力(自意識)も発達。(半面、自己矛盾に陥り易く…)
0型のcomputer:　観察装置と記憶装置とのセット
-----------＜認知能力の外側への拡張--------------------

  • (観察的:)　Bは、Bの近傍世界の物理事実 に含まれる情報を、Bとの関係で、形式的記号に捨象抽象化して、Bの中に取込める。

　――基本(底)はこちら　　　　　　　　　　　　――論証過程では(外部)観察則「…>」として出てくる
　　　　　　　　　;OCR機器，(Digital)VideoCamera+DVD　*24
----↑↑↑↑-----------------------------------------

  • (接続的観察 的:)　Bは、Bに記号レベルで接続された近傍のcomputerを観察し、その出力の記号式をそのまま受取って、Bの中に取込める。

　*25
　　　　　　　　　　　　　　　　　　　　　　　――論証過程では所与の前提「・」として出てくる

  • (状態変移的:)　Bは、取込んだり生成した、記号DATAを、自己の状態を変移させることで記憶保持しておける。必要に応じ誰かから観察可能な形で。discloseすれば、他人からも。

　*26
　
　
(以下、演算能力)
Ⅰ型:　0型のcomputerで、かつ、

  • Bは、任意の恒真式を確証する。
  • Bは、xと、x⊃yとを確証すれば、yを確証する。　――論証過程では三段則「→」として出てくる。

　(つまり、B├x かつ B├ x⊃y ならば、B├y 。)
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　――ここまでが「無垢な白箱」
----↓↓↓↓＜認知能力の内側への拡張 -----------------------
Ⅱ型:　Ⅰ型のcomputerで、かつ「自分がⅠ型」と(正しく)確証している。

  • Bは、「BX (ただしXは任意の恒真式)」の形の凡ての記号式を確証する。
  • Bは、「BX & B(X⊃Y) ⊃BY」 の形の凡ての記号式を確証する。

　　――「B(X⊃Y) ⊃(BX ⊃BY)」でも同じ――B分配公理

  • ＜環境観察式?

　
Ⅲ型:　Ⅱ型のcomputerで、かつ、(正常的):　　　　　　　　　　　　(≒様相システムK(3、クリプキ型))
　Bの場合は、xを確証すればBxを確証する。　　　　　　　　　――論証過程では(内部)観察則「->」
　(つまり、B├x ならば、B├Bx 。)
〔　(様相式の置換え定理)
〔「X≡Y」と「f(X)」とを確証すれば、「f(Y)」も確証する。　――論証過程では置換え推論則「⇒」
　
Ⅳ型:　Ⅲ型のcomputerで、かつ「自分がⅢ型(正常である)」と(正しく)確証している。(≒様相システムK4)
　Bは、「BX⊃BBX」の形の凡ての記号式を確証する。
〔　(置換え定理式)
〔Bは、「B&(X≡Y)　⊃(f(X)≡f(Y))」の形の凡ての記号式を確証する。ただし、f( )は任意の記号式。
　
　
----｛ 複雑化　----------------------------------------
(自己の安定性を確証)
　Bの場合は「BBX⊃BX」の形の凡ての記号式を確証する。――「私Bは、(凡ての) Xに関して安定。」
　　　　　　　　　　　　　　　　　　　　　　　　　　――「私Bは、(凡ての)BXに関して正確。」
　
Ｔ型:　Ⅲ型のcomputerでかつ、(自信過剰的):　――「B」を、確証、証明可能と解釈すると、自信過剰
　Bの場合は「BX⊃X」の形の凡ての記号式を確証する。　――「私Bは、(凡ての) Xに関して正確。」
　
　
　
　　-----------------
R型:　Ⅳ型のcomputerでかつ、(反射的:)　任意の記号式qについて、記号式kが存在し、
　Bの場合は、　k ≡ Bk⊃q　を確証すること。
　　　　――　kは、記号式Bk⊃qの不動点
　　　　――qが⊥でも已むを得ないので、ゲーデル的に。
　
GL型(G型と、L型と、反射的なⅣ型とは同等)　
　L型:　Ⅳ型のcomputerでかつ、謙虚(レーブ的):
　　　Bの場合は Bx⊃x を確証するとxも確証する。　　　　――論証過程ではレーブ則「-L>」
　　(つまり、　　　　　　　　　　　　　　B├Bx⊃x ならば、B├x 。)
　G型:　Ⅲ型のcomputerでかつ、「自分が謙虚だ」と確証している。
　　　Bは、「B(BX⊃X)⊃BX」の形の凡ての記号式を確証する。
　　(しかも、B├　B(Bx⊃x)⊃Bx　ならば、(B├Bx⊃x ならば、B├x )。)　――自己充足信念の1例
　　　　　　　　――Xが⊥でも已むを得ないので、「Gの念仏」id:mind:20050924　
　　　　――G型では、記号式Bk⊃qの、不動点kは Bq⊃q　。すなわち G├　Bq⊃q ≡ B(Bq⊃q)⊃q　。なので、Gは反射的。
　　　　　　　　――qが⊥でも已むを得ないので、ゲーデル的に。「灰色構成式」id:mind:20050925
　
　
(おまけ)
(ゲーデル的:)　Bの場合は「 X !≡ BX 」の形の記号式を1つでも確証していること。
　;GL型
　; R型



                                                                                                                              • -

*1:いまそこにあるのに?

*2:――digital hardware技術者にとっては普通でも、論理学者にとってはユニークに映るらしい

*3:どんなに複雑な論理式(真理関数)も、2値しかとらない。たくさんの入力(変数)を持ってても、2値しかとらない。この動作は、1コの神経細胞の出力に似ている。デジタルかアナログかが違うだけ。

*4:――対角線論法を使って証明する。逆に、＜対角化公理がなければ無限には1通りしかなく、あれば無限には階層があるということか?　＜実数を許容するなら対角化公理は必要と言うことか?

*5:「命題」と言う言葉は、命題文としての言葉ないし記号式と、それにより表現される事実と、その区別が曖昧になるので、なるべく避けることとする。「論理式」という言葉も、その嫌いを捨て切れないので、「記号式」と呼んでみる。LISPでいうS式SymbolExpression。

*6:「先験的自明に」真に観えるらしい

*7:「先験的自明に」正しく観えるらしい

*8:――循環定義w。ここは古典論理におまかせね

*9:――てゆうか、Bは多階(述語の述語の…)を許す一項述語(性質記号)のようなもの。とすると、役者A,B,C,…,Q,…が舞台に登場してくると、様相論理は述語論理のようなもの?　でもって、カリー化を使えば多項述語も表現できる?

*10:――　慣れてくると、無意識には形式的にしか推論を進められなくなりますw

*11:――頭が固くなる訳じゃないと思うが…　むしろ、「形式から意識的に外れる自由な世界」を手に入れられるって感じ?

*12:――小学生用の公文式?"論理計算ドリル"も造るべきだよな!　って「小賢しい小学生」は嫌われるから教育制度に取入れないんだろうけど。and or判らなきゃネット検索もできないじゃん。国語や択一テスト対策にも絶大な威力を発揮するってのに……「親権者な人々」は考えときましょうw

*13:――俗に言う環境問題は近傍問題だったってことねw

*14:――可能的に真であるとか偽であるとか、を認めると、実質的には3値論理学になってしまうような…。それに比べ、証明可能性の様相論理学は、遙かに実用的な感じ。ロボット工学にも応用できる?　

*15:，ホントに混同してる場合w ；――私はalphabetと混用してますが…

*16:――記号論証過程の中に示しているが、それは我々読み手に解り易くするため、という感じ。注釈入れるより一目瞭然なので。

*17:――最外殻の箱Bは、不透明(諸々の表現器官を通じて透明

*18:;神経細胞の繋がり具合と蓄積された興奮状態?

*19:「〜公理」　　システムについて成立って欲しい、我々の言葉による公理。設計原理。――不文憲法? 憲法理念?

*20:「真似っ子」は幼稚園児には嫌われたものだが、芸能人や政治家にとっては「才能」として人々に認められる模様w

*21:「真似碁」というTFTに似た面白い戦略もある　――名人とやっても完璧に上手く行く!! ――中央の不動点付近で対称性が破られるまではw ；

*22:――Ⅲ型に出世すれば用済み

*23:――「恒真式についてだけⅢ型」と言っても良い。

*24:アナログでも、高音域とか赤外線とか捨象して抽象化は行われる

*25:従来の計算機、論理機械は、この直接入力direct inputだけ。人間が主人、自動人形は囚人と、対等でないので、「入力」と言う言葉を使ってた。――「agent programが必要に応じserverなどにrequestして、欲しい入力を選んで取ってくる」の域に達すると、もはや「入力」の名詞は相応しくない。

*26:;なんでもないただの石ころ も、地学的time scaleで、環境から刻まれてくる情報を保持するという点で、0型のcomputerではある。