人気ブログランキング | 話題のタグを見る

完全性定理の証明についての疑問

『数学基礎論講義』の命題論理の完全性定理の証明の中で、無矛盾な命題の集合を Σ とする時、

任意の論理式 An について An ∈ Σ または ¬An ∈ Σが言える。

という文があったが、これは明らかに間違いだと思う。論理式の文法によって生成される論理式の命題の中には、トートロジーではないものがあるので、An がトートロジーでなければ ¬An もトートロジーではない。上の命題が成立するのは、An がトートロジーであるか、または An が恒偽命題であるかのどちらかの場合だ。

上の命題が間違っていたら、完全性定理の証明に影響がある気がする。完全性定理の最初は 命題 A が定理でなければ {¬A} は無矛盾であるとしているが、命題 A が定理でなくても、命題 A が恒偽命題でなければ、{¬A} は無矛盾ではない。

訂正: コメントで御指摘を受けました。A が証明可能でないとき {¬A} が矛盾なら¬Aの否定も証明可能なので、 ¬¬A から A が証明可能になってしまい仮定に反します。したがって {¬A} は無矛盾であるという結論になります。

なぜなら、A -> B はトートロジーではないが、A にトートロジーの命題、B に恒偽の命題を割り当てると、これは恒偽命題になる。明らかに、


{A -> B} |- (A -> B)

であるから、結果として恒偽命題を仮定から演繹できることになるので、{A -> B} は無矛盾ではない。また、その否定 ¬(A -> B) も同様の理由で無矛盾ではない。

したがって、完全性定理は証明できないことになる。

この議論の発想は、任意の命題はトートロジーでも恒偽命題でもないものがあるはずだ、したがって An ∉ Σ かつ ¬An ∉ Σ の場合もあるはずではないかというものだったと思う、自分でも忘れている。しかし、この場合はそのような An という命題が論理式の再帰的定義に即しているかどうかという検討が必要だったのではないだろうかと思う。

無矛盾は公理系から演繹される考え方で、トートロジーは真理表から計算される概念だ。したがって、命題がトートロジーであることを、公理系の概念である無矛盾性から証明することはできないのではないだろうか。完全性定理で証明できるのは、命題が無矛盾であれば、それは定理であるということで、無矛盾とトートロジーとは異なる概念のような気がする。また、完全性定理で導入される真理関数は、明らかにトートロジーを判別する関数ではなく、命題が無矛盾かどうかを判別する関数である。

トートロジーが定理であることを証明するためには、論理計算の法則が全て公理系から演繹できて、任意のトートロジーについてそれは公理からも演繹できることを言わなければならないのではないだろうか。

数学は素人だが、命題論理の完全性定理の証明が納得できない理由だ。

by tnomura9 | 2016-09-23 06:49 | 考えるということ | Comments(11)
Commented by 通りすがり at 2016-10-29 12:04 x
まずは冒頭の
> 無矛盾な命題の集合を Σ とする時、任意の論理式 An について An ∈ Σ または ¬An ∈ Σが言える。
は正確な引用ではないでしょう?「無矛盾な命題の集合を」ではなく「無矛盾な命題の極大集合を」のようになっているはずです。
元の引用文のままなら明らかに間違いです。たとえば、Σ={p} (pは何らかの原子命題)はすぐにその反例になりますから。
そのうえでもまだ、その後のtnomuraさんの論述は意味がありますか?
Commented by tnomura9 at 2016-10-29 14:26
通りすがりさんコメントありがとうございました。

教科書ではΣは極大な無矛盾集合となっていました。極大な無矛盾集合の意味を誤解しているのかもしれませんが、仮に、極大な無矛盾集合を、無矛盾な論理式すべてを集めた集合と考えたとしても、任意の論理式 An について An または ¬An がΣの要素であるといえるかどうかはわからないような気がします。つまり、任意の論理式の中には、トートロジーではない論理式が含まれており、このような論理式では論理式自身も、その否定の論理式もトートロジーではないからです。
Commented by 通りすがり at 2016-10-29 15:04 x
「トートロジーではない論理式の否定はトートロジーではない」とおっしゃっているなら、それは間違いですね。
たとえば、A∧¬A は恒偽式であり、もちろんトートロジーではありませんが、その否定¬A∨Aはトートロジーですから。
Commented by 通りすがり at 2016-10-29 15:10 x
そもそも、(極大な)無矛盾集合の中にはトートロジーでない論理式も入っていてよい(ふつう入っている)のですが、その点誤解されていませんか?
Commented by tnomura9 at 2016-10-29 15:36
おっしゃる通り極大な無矛盾集合について誤解しているのでしょう。極大な無矛盾集合の要素である論理式はトートロジーでなくてはならないような気がしていたものですから、その辺で誤解しているのかもしれません。

ただ、トートロジーでない命題の否定が、トートロジーでも恒偽命題でもない論理式は存在します。原子命題 A は論理式ですが(論理式の文法を満たしていますが)トートロジーではありませんし、原子命題 A の否定もトートロジーでも恒偽命題でもありません。

極大な無矛盾集合でトートロジーではない論理式を含むのはどんな場合なのでしょうか。
Commented by 通りすがり at 2016-10-29 21:17 x
> ただ、トートロジーでない命題の否定が、トートロジーでも恒偽命題でもない論理式は存在します。
それはそうです。そして先にも書いたように、トートロジーでない命題の否定がトートロジーであることもあります。

> 極大な無矛盾集合でトートロジーではない論理式を含むのはどんな場合なのでしょうか。
極大な無矛盾集合は、原子命題Aあるいはその否定¬Aのどちらか一つ(どちらもトートロジーでない)を必ず含みます。
Commented by tnomura9 at 2016-10-29 22:56
コメントありがとうございました。大分極大無矛盾集合のイメージを変えることが出来たと思います。原始命題 A を公理のようなものと考えれば、¬A は恒偽命題として扱えますから。少なくとも原始命題(あるいはその否定)に関しては、それを極大無矛盾集合の要素と考えることができるというのは納得できる気がします。しかし、A -> B のような命題は極大無矛盾集合の要素とは考えにくいのではないかと思ったのです。これを極大無矛盾集合の定理である公理図式として考えると、A にトートロジー、Bに恒偽命題を当てはめると、これは恒偽命題となってしまうので矛盾します。これは ¬(A -> B) の場合も同じです。しかし、このような場合は原始命題の真理値で真偽値が決まっている命題と考えることになるのでしょうか。ウカシェビッチの公理図式から演繹される定理は全て命題図式です。それとは異なり、極大無矛盾集合の命題は全て真偽の確定した原始命題から構成される命題で、命題図式は含まれていないと考えるのでしょうか。
Commented by 通りすがり at 2016-10-29 23:17 x
はい。(私の理解では)極大無矛盾集合は(通常の)命題の集合であり、命題図式などは含まないと思います。
Commented by tnomura9 at 2016-10-30 01:08
通りすがりさん、コメントありがとうございました。
極大無矛盾集合が、原始命題と論理結合子論理結合子で構成される論理式の集合の部分集合で、その要素間の関係が無矛盾であるような集合というイメージならよく分かるような気がします。また、Σがそのような集合であれば、任意の命題 A が Σ の要素であるか、その否定が Σ の要素であるというような排中律が少なくとも命題論理の世界では成立するというのも納得がいく気がします。命題論理の生成規則では、無限の再帰のようなややこしいことは起きないからです。また、ウカシェビッチの公理図式から演繹される定理図式はあくまで図式であり、通常の命題を論理的に変形するための推論規則の体系であると考えるとスッキリします。もう一度参考書の証明に取り組んでみたいと思います。
ありがとうございました。
Commented by 匿名 at 2019-11-08 05:15 x
Aが証明できないとき{¬A}は無矛盾、というのは正しいです。
もし矛盾するとしたら、(命題論理における)背理法から、¬¬A、すなわちAが証明できることになります。
よって(メタな意味での)背理法により、無矛盾となります。
Commented by tnomura9 at 2019-11-08 08:55
> 匿名さんコメントありがとうございました。

矛盾すれば、Aが証明できてしまうということですね。納得しました。ありがとうございました。
<< 48時間 Scheme 記事リスト 論理式のパーサ >>