情報論理の変更点

追加された行はこの色です。
削除された行はこの色です。
情報論理へ行く。
情報論理の差分を削除
** 情報論理 [#r1ca9d63]
- 担当：萩谷昌巳教授
- 2.0単位
- 10:15-11:45 化東236
- 評価：出席，中間試験，期末試験

http://nicosia.is.s.u-tokyo.ac.jp/~hagiya/#lecture

**内容 [#v7ef80ad]
-2項関係 R
--反射的：&mimetex(I\subseteq R);,最小の反射的閉包：&mimetex(R\cup I);
--推移的：&mimetex(R^2=R);，最小の推移的閉包：&mimetex(R^+);
--対称的：&mimetex(R^{\top}=R);，最小の対称的閉包：&mimetex(R\cup R^{\top});
--反対称的：&mimetex(R\cap R^{\top}\subseteq I);
-命題論理：&mimetex(A::= \top|\bot|P|\neg A|A\wedge A|A\vee A|A\supset A);
-一階述語論理：&mimetex(A::=P(t,\dots,t)|\neg A|A\wedge A|A\vee A|A\supset A|\forall x A|\exists x A);
--コンパクト性：論理式の集合に対して，その任意の有限部分集合が個別に充足可能ならば，集合全体を同時に充足可能
--完全性
---弱い完全性：&imgtex(\[\Gamma\vDash A\Rightarrow \Gamma\cup\{\neg A\}\]);が充足不能
---強い完全性：&imgtex{\[\Gamma\vDash A\Rightarrow \Gamma\vdash A\]};
--健全性：&imgtex{\[\Gamma\vdash A\Rightarrow \Gamma\vDash A\]};
-帰納的関数
--原始帰納的関数
---zero():定数0
---後者関数S
---射影関数pr
---合成：&mimetex(h(x_1,\dots ,x_n)=f(g_1(x_1,\dots ,x_n),\dots,g_m(x_1,\dots ,x_n)));
---原始帰納法：&mimetex(h(0,x_1,\dots, x_n)=f(x_1,\dots,x_n)\\h(S(x),x_1,\dots ,x_n)=g(x,h(x,x_1,\dots ,x_n),x_1,\dots,x_n));
--部分帰納的関数
---原始帰納的関数＋最小化演算子
--KleeneのT述語~
---T(e, x, y) = 0 (if y はチューリング機械 e が入力 x で実行されたときの実行過程)
---T(e, x, y) = 1 (otherwise)
--チューリングマシンの停止性判定
---h(p(e,x))=0  (if &mimetex(\exists y. T(e,x,y)=0);)
---h(p(e,x))=1  (otherwise)
--hは計算不能
---hが計算可能であると仮定すると，h(p(x,x))=0ならば停止せず，h(p(x,x))=1ならば停止するようなチューリングマシンMを構成することができるが，MにMのインデックスを入力すると矛盾する．
-帰納的集合
--機能的に加算
---&mimetex(R=\{x\in\mathbb{N}|\exists y.f(x,y)=0\});
---&mimetex(R=\{x\in\mathbb{N}|h(x)\ne \bot\});
--帰納的
---Rと&mimetex(\mathbb{N}-R);の両方が帰納的に加算
---&mimetex(R=\{x\in\mathbb{N}|h(x)=0});
-ゲーデルの不完全性定理
--ω無矛盾
---&mimetex(\exists x A[x]);が証明でき，&mimetex(\forall y.\neg A[\bar{y}]);が証明できるような論理式A[y]が存在しない．
--ω矛盾かあちゃん
---母親｢あれはしちゃだめ､これもしちゃだめ…｣ ~
子供｢ねぇ､何かしていい事はあるの？｣ ~
母親｢ええ､あるわよ｡でもあれもだめ､これもだめ…｣
--ゲーデルの不完全性定理
---算術の演繹体系がω無矛盾であると仮定すると，&mimetex(G);も&mimetex(\neg G);を証明することはできない．




**過去問 [#c74b193c]
-1.&mimetex(y\times y\le x);を満たす最大のyを返すような関数f(x)=g(x,x)を原始帰納法を用いてあらわせ．
--解~
&mimetex(g(x,0)=0);~
&mimetex(g(x,S(y))=if(S(y)\times S(y)\le x)\ S(y)\ else\ g(x,y)\\ \hspace{66em}=(1-(S(y)\times S(y)-x))\times S(y)+(1-(1-(S(y)\times S(y)-x)))\times g(x,y));
-2.停止判定のチューリングマシンが存在するならば矛盾する
-3.帰納的に加算な集合の和集合は帰納的に加算
--解．&mimetex(X=\{x|\exists y.f(x,y)=0\});~
&mimetex(Y=\{x|\exists y.g(x,y)=0\});~
とすると，&mimetex(X\cup Y=\{x|\exists y.f(x,y)*g(x,y)=0\});~
-4.ゲーデルの不完全性定理の議論において，
閉じた論理式G に対して，
&mimetex(G \leftrightarrow \neg \exists y \mathrm{Proof} [\bar{\lceil G\rceil} , y, 0]);
という同値命題が証明可能である．
以下、算術の演繹体系が(無矛盾) であると仮定する．
さらに、G が証明可能であると仮定する．
すると、G の証明が存在する．
その証明の符号である自然数をy0 とおく．
すると、&mimetex(\mathrm{proof} ((\lceil G\rceil), (y_0)) = 0); が成り立つ．
論理式Proof [x, y, z] は関数proof を(表現) しているので，
&mimetex(Proof [\bar{(\lceil G\rceil)}, (y_0), 0]); が証明可能である．
すると，&mimetex((\exists y.Proof [\bar{\lceil G\rceil}, y, 0])); が証明可能である．
ところが，上の同値命題が証明可能なので，
G が証明可能ならば&mimetex(\neg(\exists y.Proof [\bar{\lceil G\rceil}, y, 0]));も証明可能．
したがって、&mimetex((\exists y.Proof [\bar{\lceil G\rceil}, y, 0]) \wedge \neg (\exists y.Proof [\bar{\lceil G\rceil}, y, 0])); が証明可能となり，
算術の演繹体系が(無矛盾) であるという仮定に反してしまう．
-5.
--一階の算術：自然数に関する一階の述語論理
--数学的帰納法：&mimetex(A[0]\wedge \forall x(A[x]\supset A[S(x)])\supset \forall x A[x]));の形の公理
---部分帰納的関数：原始帰納的関数＋最小解演算子
---帰納的集合：帰納的に可算であり，その補集合も帰納的に可算である集合
--部分帰納的関数：原始帰納的関数＋最小解演算子
--帰納的集合：帰納的に可算であり，その補集合も帰納的に可算である自然数の部分集合
情報論理 の変更点

情報論理の変更点
