哲学的(?)議論の形式化 - (保存用) 檜山正幸のキマイラ飼育記メモ編

たまたまみた http://sets.cocolog-nifty.com/blog/2017/11/post-ee0f.html に次のような"証明”(?)があった。

（前提1）すべての事象は、特性Ｐと特性Mのいずれか、または、両者を持つ。つまり、すべての事象は、特性Ｐのみを持つＰ事象か、特性Mのみを持つM事象か、両者をもつＢ事象かのいずれかであるとする。
（前提2）Ｐ事象はＰ事象かＢ事象にのみ影響することができ、M事象には影響しない。
（前提3）M事象はM事象かＢ事象にのみ影響することができ、Ｐ事象には影響しない。
（前提4）或る事象aの影響が他の事象bに及び、さらにその影響がもう一つの事象cに及んで、結果的に事象aの影響が事象cに到達するような関係を「影響の経路がある」と言うとするとき、或るＰ事象のあらゆる影響の経路がいずれのM事象にも達しない場合、そのＰ事象を「純粋なＰ事象」と呼ぶとする。また、或るM事象のあらゆる影響の経路がいずれのＰ事象にも達しない場合、そのM事象を「純粋なM事象」と呼ぶとする。
（前提5）「或る純粋なＰ事象pと或る純粋なM事象mがともに存在する」が発言されたという事象を事象sとする。
（前提6）事象sの文の内容は真であり、その正しさは経験的に確かめられる可能性を持つ。

（証明）上の前提1〜6が同時に成り立つことはあり得ない。

（7）sがMだと仮定する。
（8）7のとき、「或る純粋なＰ事象pが存在する」は経験的に確かめられない。
（9）しかし、これは前提6に矛盾する。ゆえに、7は偽。
（10）sがPだと仮定する。
（11）10のとき、「或る純粋なM事象mが存在する」は経験的に確かめられない。
（12）しかし、これは前提6に矛盾する。ゆえに、10は偽。
（13）9と12より、sはMでもPでもない。
（14）しかし、これは1のすべての事象はMかPのどちらかであるというものに矛盾する。
（15）よって、上の前提1〜6が同時に成り立つことはあり得ない。■

こういうのって形式化できるのだろうか？

（前提1）∀e:Evt.( (P(e)∧¬M(e)) ∨ (¬P(e)∧M(e)) ∨ (P(e)∧M(e)) ), B(e) :⇔ P(e)∧M(e)
（前提2）∀x, y:Evt. Affect(x, y) ⊃ ( (P(x)∧P(y)) ∨ P(x)∧B(y))∧¬(P(x)∧M(y))
（前提3）∀x. y:Evt. Affect(x, y) ⊃ ( (M(x)∧M(y)) ∨ P(x)∧B(y))∧¬(M(x)∧P(y))
（前提4）PureP(x) := P(x)∧(¬∃y.( M(y)∧Affect^*(x, y) ) ), PureM(x) := M(x)∧(¬∃y.( P(y)∧Affect^*(x, y) ) )
（前提5）s := Spoken(`∃p.∃m.( PureP(p)∧PureM(m) )`)
（前提6）事象sの文の内容は真であり、その正しさは経験的に確かめられる可能性を持つ。

前提6はうまく翻訳できなかった。これはメタな言明 |= s なのか？「sの文の内容」が何を意味するか不明。「経験的に確かめられる可能性」も分からんが、||= (|= s) のようなメタメタ文と関係があるのか？

それと「すべての事象」が何を意味するかもわからない。

（証明）上の前提1〜6が同時に成り立つことはあり得ない。

とりあえず先に進む。

（7）assume M(s)
（8）7のとき、¬(|= ∃p.PureP(p))
（9）しかし、これは前提6に矛盾する。つうことは、前提6は |= ∃p.PureP(p) を導くはず。
（10）assum P(s)
（11）10のとき、¬(|= ∃m.PureM(m))
（12）しかし、これは前提6に矛盾する。つうことは、前提6は |= ∃m.PureM(m) を導くはず。
（13）9と12より、sはMでもPでもない。
（14）しかし、これは1のすべての事象はMかPのどちらかであるというものに矛盾する。ということは、s∈Evt でなくてはならない。
（15）よって、上の前提1〜6が同時に成り立つことはあり得ない。■

うーん？？ `…` をゲーデル符号化として、論理式がEvtに埋め込まれるとはしているが、「発話された」とが意味不明。s := `∃p.∃m.( PureP(p)∧PureM(m) )` なのか、「発話された」も含めた s := Spoken(`∃p.∃m.( PureP(p)∧PureM(m) )`) かも不明。

「事象」とか「文」とか「発話」とかが正確に定義されてないので、とりあえずなんともいえん感じ。