[cocolog:93262667] の因明の話つづき。…

jrf> [cocolog:93262667] の因明の話つづき。

とりとめのない話。いくつか。

とりとめのない話 その１。

2022年1月22日追記の「時間的な推移」の τ(Q,P,x) についてもう少し詳細に考える。

x はオブジェクトみたいなもので、x の中に様々な情報が入っていると考え、それをメンバ関数で呼び出す…みたいな考え方をしてみる。

τ(Q,P,x) は、ある時刻 t1 における x を特別に選ぶ at 関数を使って P(at(x, t1))  が成り立ち、Q(at(x, t2)) が成り立っていて、t2 < t1 で t2 と t1 が重なる部分があるみたいに定義すれば良いのだろうか？

いや、しかし時間が重なっていても原因と結果になっていなければ意味がない場合もありうる。すると、オブジェクト x は履歴も含んでいて、そこに Q が P につながったという原因結果の履歴があることをチェックするという形にすればいいのではないか。

τ(Q,P,x) とは x.GenninRireki('Q', 'P') …みたいにすればいいのだと思う。

これを使うとき x はそういうオブジェクトでないといけないから、その型を指定するのを T(x) とする…より T(x) の名前を適切にして RirekiAriObject(x)  としよう。そういうオブジェクト x はある程度のタイムスパンを持っていて、ただ注目しているデフォルト時というのがあるとしよう。

すると因明は、x がデフォルト時に述語 P を満たすことを x.dtp('P') と表すとすると、

IM'2(P, Q) == ((∃y. RirekiAriObject(y) ∧ y.GenninRireki('Q','P')) → (∀x. RirekiAriObject(x) → (x.dtp('P') → ◇ x.dtp('Q'))))

…みたいにすれば良いのだろう。P Q が '' に囲まれてるのがちょっと嘘くさいが、まぁ、そういうものとここでは読んで欲しい。なお、y.GenninRireki('Q','P') → (y.dtp('P') ∧ y.dtp('Q')) は成り立っているものとする。

2022年2月8日の追記で、仮定を落として可能性を導く演算を考えたが、直上の例は、仮定を落とすのに似ているが少し違い、原因履歴の参照を落として可能性を導く演算になっていると言える。

……。

ここで新たな記号を導入しよう。

Γ |- A (前提の列 Γ から A が証明手続きによって導出できる。)
Γ !|- A (前提の列 Γ から A が証明手続きによって導出できない。)

ちなみに Γ !|- A はどうやっても導出できないことを示せないとダメなのでいうのがかなり難しい。

……。

とりとめのない話 その２。

「仮定を落として可能性を導く演算」の仲間として A ∨ B ==> ◇A が挙げられる。これは A にも B にも言えることだから結局、

A ∨ B ==> ◇A ∧ ◇B

…ということになる。これを存在記号・全称記号に拡張すると、

(∃x. P(x)) ==> (∀x. ◇P(x))

…となる。これに先の仮定を落とす演算を加える。

Γ,A |- X ==> Γ |- ◇X

さて、こういった演算を使っていいか、矛盾が出てこないかが問題となる。

確かマズかった気がするのだが、詳しく今はなぜダメなのか私は示せない。

……。

とりとめのない話 その３。

「あり得ないわけではない」ということと、「可能性がある」には、差がある。…という話だが、「あり得ないわけではない」というのは、必然的に P(a) でないようなものは導けないということつまり、

Γ !|- □¬P(a)

…のとき ◇P(a) を仮定しても問題ないということだった。つまり、…

(Γ !|- □¬P(a)) ∧ (Γ !|- ⊥) ==> (Γ, ◇P(a) !|- ⊥)

これをどう推論規則に仕上げたら良いものか…。