FANDOM


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

動機

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

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

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

計算と証明の関係

これまで人間がやっていた証明を機械で自動的に扱うことはできないか、「証明する」という行為や証明そのものについて、メタな視点からなんらかのメタな定理を得られないか、という研究が20世紀初頭から興り始めたとか、詳しいことはgoogle先生に聞いてください。

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

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

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

計算複雑性について

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

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

原始再帰

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


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

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