数理論理学

勉強

id:peregrinationのまね

全ての素数はそれより小さい数では割り切れない。

\forall x \not \exist y( P(x) \wedge x>y \quad \supset \quad (div(x,y) \in N) )

どの自然数よりも小さい自然数は存在しない。

\not \exist y \forall x ( N(x) \wedge N(y) \supset x>y)

任意のxと任意のεに対してδが存在して、|x-a|<δならば|f(x)-f(a)|<ε

\forall x \forall \varepsilon \exist \delta ( |x-a|<\delta \quad \supset \quad |f(x)-f(a)|<\varepsilon)

全ての非決定性有限オートマトンに対して、それと等価な決定性有限オートマトンが存在する。

\forall n \exist d (NFA(n) \wedge DFA(d) \quad \supset \quad G(d) \equiv G(n) )

無曖昧な文脈自由文法では生成できない文脈自由言語が存在する

\exist Y \forall X (\neg ambiguousCFG(X) \wedge CFL(Y) \quad \supset \quad (\neg G(X) = Y) )

P(x)
素数判定関数
G(x)
文法xによって生成される言語
ambiguousCFG(x)
xは曖昧なCFG

\lbrace A \supset B \rbrace \vdash_{NK} \neg B \supset \neg A

tex記法でやろうとしたら死にそう。後回し。
図にしなければいい。

[仮定1:A \supset B]
補題
\neg A = A \supset \perp
\neg B = B \supset \perp

とりあえず上向きに展開。
 (\neg B \supset \neg A) \Leftarrow (\neg A)　　　　　(⊃導入、\neg Bを仮定2とし、ここで消費。) 
 (\neg A) \Leftarrow (\perp)　　　(⊃導入、 Aを仮定3とし、ここで消費。)

以下、\perpが出たので仮定から頑張って矛盾を導く。下向き。

仮定1、3から
 (1:A) \wedge (3: A \supset B) \Rightarrow B　(⊃削除)
これと、仮定2から
 B \wedge \neg B \Rightarrow \perp　　(⊃削除)

分解証明系

1,2から、以下が導けるはず

  1. S(x)⇒A(x)
  2. ⇒S(s)
  3. S(x),P(y)⇒L(x,y)
  4. A(x)⇒P(f(x))
  5. A(x),L(x,f(x))⇒

これから、”⇒”を導けば、「反駁DAGが存在する」ので、これと必要十分である「充足不能」を示せる。

１．とりあえず(1)と(2)を組み合わせれば一個消えるっぽいので消す。

(1)[s/x]　と　(2)　から　⇒A(s)　(カタツムリは動物だ)

２．上で(4)のAを消せる。

⇒A(s)　と　(4)[s/x]　から　⇒P(f(s))　(カタツムリはなんかの植物を食べる)

３．２を使って直接消せそうなのが無いので、まだ使ってない(3)を見てみる。すると、Sがすぐ に消せそうだ。

(2)　と　(3)[s/x]　から　P(y)⇒L(s,y)　(yが植物なら、カタツムリはyを食べるのがすき)

４．３のLが邪魔、唯一Lが左辺にある(5)を使いたいので、まずは(5)を変形。Aを消すのには１ が使える。

⇒A(s)　と　(5)[s/x]　から　L(s,f(s))⇒　(カタツムリはカタツムリが食べるものを食べるのがすきならば、矛盾。)

５．晴れてLだけの式を手に入れたので、３のLを消せる。

P(y)⇒L(s,y) [f(s)/y]　と　L(s,f(s))⇒　から　P(f(s))⇒　(カタツムリが食べるのがすきなものが、植物だったら、矛盾)

６．Pだけの式を左辺、右辺両方手に入れた！合成。

P(f(s))⇒　と　⇒P(f(s))　から　⇒　(よって矛盾)

ゆえに反駁DAGが存在するので、このКは充足不能。