FANDOM


独自研究よりの内容のメモ。

超数学の視点から、ある理論で全域性を証明できることを以て計算可能性の証明としてもいいが、そういうのはやめておく。その理論の無矛盾性の証明がなければ数学的な正確さに缺けるというのもある。

動機

証明とは、公理と呼ばれる前提条件から推論規則を有限回適用して、正しいということを示したい論理式を導き出すことを言う。

矛盾した公理からは任意の論理式が証明できてしまうため、本当に正しい証明を得るためにはその前提条件が無矛盾でなければならない。しかし無矛盾であることの証明自体にも同じことが言えてしまう。そのため、本当に正しい証明は、たとえ存在するとしてもそれがなんであるかを知ることができない、ということになってしまう。

そこで、逆に無条件で正しいとする前提条件を作り、そこから矛盾が導かれる場合は推論規則なり方法論なりが間違っているとする立場について考える。

たとえば、「1」を入力されたら「真」という記号を、「0」を入力されたら「偽」という記号を返して停止する機械があるとする。この機械は「真」と「偽」を同時に出力することはないと議論する者は無条件で信じるため、あるいはそのような現象が起こる要因、もしくはその現象そのものの存在を認めないため矛盾(の形)が導かれてしまうことはない。

端的にいえば無矛盾性と実在性(モデルの存在)は等価であると考える。

計算と証明の関係

type as proposition の立場から、モダスポーネンスが関数の適用に当たる。

ゲーデル数を利用して妥当性を形式的に確認することができるために不完全性定理が成り立ってしまう。

論理が健全であることを示すのに、その任意の形式的証明が論理的帰結に反しないことが挙げられるが、形式主義的には論理が健全であることが先に定義される。健全でないと主張する者に対しては証明の解釈や読み方が間違っていると延々と指摘し続ければ否定しようがない、ただし自分自身その論理が理解できなくなってしまうというリスクが伴う。要するにゴリ押し。

計算複雑性について

チューリング完全よりも弱い言語で目的のプログラムを出力するだけなら、そしてチューリング完全よりも弱い言語でいい限り、プログラムを記述する計算可能なプログラムが存在する。

言語Lによって書かれるプログラムの列 σ_0,σ_1,σ_2,...

原始再帰

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。

FANDOMでも見てみる

おまかせWiki