命題論理の定理の証明

質問

論理学の有名な定理？

A→C,B→C,ならばAvB→C
というのがありますが
http://en.wikipedia.org/wiki/Disjunction_elimination

AvB＝（￢A)→B

それは
命題論理の公理系

１) φ → (χ → φ)
２) (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
３) (￢ψ → ￢φ)→(φ → ψ)

あとモーダスポネンスを使って証明出来るんでしょうか？

よろしくお願いします

回答No.6

stomachman

ANo.5訂正です。

　　((￢A→B)→C)→C
じゃなくて、
　　(￢A→B)→C
を導出する話でしたね。ま、要領は同じです。論理式が推論規則で出たのか、公理（スキーム）から作られたのか、場合分けをしていって、前提(A→CとB→C)だけに還元できれば、証明が構成できたことになるわけです。

回答No.5

stomachman

ANo.3へのコメントについてです。
　結局、
公理(1) φ→(χ→φ)
公理(2) (φ→(χ→ψ))→((φ→χ)→(φ→ψ))
公理(3) (￢ψ→￢φ)→(φ→ψ)
と、推論規則
　　Γ, Γ→Δ ⊢ Δ
から
　　((￢A→B)→C)→C　…(4)
を構成できるか、というパターンマッチングの問題らしい。(形式論理をやる人が舌足らずじゃイカンすね。)

(4)を構成できたとすると、その最後の段階は、[1](4)が公理そのものであるか、あるいは[2](4)は推論規則の結論(Δ)として得られたものか、のどちらかである。
[1] ((￢A→B)→C)→Cは公理そのもの？
　公理(1)～(3)のどれも、最も上位の→の右にあるのは( → )を含む式なので、((￢A→B)→C)→Cとはマッチせず、従って(4)は公理そのものではない。
[2] ((￢A→B)→C)→Cは推論規則で得られたもの？
　　Γ, Γ→Δ ⊢ Δ
の結論ΔがΔ=((￢A→B)→C)→Cであるとすると、Γは公理そのものであるか、あるいは推論規則の結論として得られたものである。そして、Γ→Δも公理そのものであるか、あるいは推論規則の結論として得られたものである。
[2-1] Γ→(((￢A→B)→C)→C)は公理(1)?
　だとすると、φ=Γ, χ=(￢A→B)→C, φ=Cであるから、Γ=Cである。すると、Γ, Γ→Δ ⊢ ΔにおいてΓが前提になるのだから、これより前の段階でΓ、すなわちCが構成されねばならない。これはムリ。
[2-2]Γ→(((￢A→B)→C)→C)は公理(2)?
　公理(2)はこのパターンにマッチしない。
[2-3] Γ→(((￢A→B)→C)→C)は公理(3)?
　だとすると、￢ψ→￢φ=Γ, φ=(￢A→B)→C, ψ=Cであるから、Γ=￢C→￢((￢A→B)→C)。
　これは元の式（((￢A→B)→C)→C）が対偶になっただけですが、もうちょっと追いかけてみましょうか。
[2-3-1] ￢C→￢((￢A→B)→C) はどの公理ともマッチしない。
[2-3-2] ￢C→￢((￢A→B)→C) は推論規則で得られたもの？
　だとすると、
　　Γ', Γ'→Δ' ⊢ Δ'
において、Δ'=￢C→￢((￢A→B)→C)である。
[2-3-2-1]Γ'→(￢C→￢((￢A→B)→C))は公理(1)?
　だとすると、φ=Γ', χ=￢C, φ=￢((￢A→B)→C)だからΓ' = ￢((￢A→B)→C)である。
[2-3-2-1-1]￢((￢A→B)→C)はどの公理ともマッチしない。
[2-3-2-1-2]￢((￢A→B)→C)は推論規則で得られたもの？
　だとすると、
　　Γ'', Γ''→Δ'' ⊢ Δ''
において、Δ''=￢((￢A→B)→C)である。
[2-3-2-1-2-1]Γ''→￢((￢A→B)→C)は公理(1)とはマッチしない。
[2-3-2-1-2-2]Γ''→￢((￢A→B)→C)は公理(2)とはマッチしない。
[2-3-2-1-2-3]Γ''→￢((￢A→B)→C)は公理(3)とはマッチしない。
だから、[2-3-2-1-2]は誤り。
[2-3-2-2]Γ'→(￢C→￢((￢A→B)→C))は公理(2)とはマッチしない。
[2-3-2-3]Γ'→(￢C→￢((￢A→B)→C))は公理(3)?
　だとすると、￢ψ→￢φ=Γ', φ=￢C, ψ=￢((￢A→B)→C)なので、Γ'=￢￢((￢A→B)→C)→￢￢Cである。
　この先続けて行っても、公理(3)で対偶を作るたびに￢の数が増えて行くだけですね。

回答No.4

itshowsun

ごめんなさい。
最初に恒真式
式１：　[(A→C)∧(B→C)]→[(A∨B)→C]
が出ていたので、質問とWikiの参照までちゃんと読んでいなかった。
この式が恒真式（恒等式）なのは
(A∨B)→C = ￢(A∨B)∨C
= (￢A∧￢B)∨C
= (￢A∨C)∧(￢B∨C)
= (A→C)∧(B→C)
よって質問の式は φ→φ と同じ。
一方、Wikiの選言消去の参照を見ると
(A→C), (B→C), (A∨B) |- C
となっており、これは
式２：　(((A→C)∧(B→C))∧(A∨B))→ C　（これも恒真式らしいよ）
に対応する。この式であるならば、推論規則を使うと
((A∨B)→C)、(A∨B) |- C　　（P,(P→Q) |- Q）
最初の恒等式を使って
(A→C)∧(B→C), (A∨B) |- C
が出る。
ただ、質問に挙げられている公理系を使って導出できるかどうかは
やっていない。
上の議論が正しいとすると、
モーダスポネンスとA→B＝￢A∨Bのみで導出できることになるのかな。
式１ではなく式２を考えたので、
また質問の公理系で証明するということが理解できないので、
私はまだ質問の意味を完全には理解していないかもしれない。

回答No.3

stomachman

ANo.1へのコメントについてです。

> A→C,B→C⊨AvB→C

> ではなく、
> A→C,B→C⊢AvB→C

　ANo.1はまさにその話をしています。繰り返しになりますが、"v"に関する公理も、"v"に関する推論規則もないのなら、その形式論理体系には"v"という記号がそもそも含まれていない。その体系において、たとえ形式文法によって「"AvB→C"という文字列も文として認める」という奇妙な定義を与えたとしても、（"AvB→C"を含めて）文字"v"を含むいかなる文も扱う手段がなく、当然、それは形式的証明の対象になりえません。（「奇妙」と言うのは、扱う手段がないような文字列を文として認めても全く無駄だからです。）

お礼

回答ありがとうございます。

私の説明不足で申し訳ありません。
まず”v”の定義については
AvB＝（￢A)→B
と書いたのですが、これは
勿論”v”についての公理も推論規則も上にあげた三つの公理ともーだすぽねんす以外に存在しないのを前提にしています。
簡単に言えば、AvBとは
（￢A)→Bの略であるということです。
なのでvの公理も推論規則も無くて導きだせるはずです。
何故vを使ったのかというと、本題の式はDisjunction Eliminationと言う有名な式だったからで、
説明を促そうとしたんですが、逆に混乱させてしまいました。

つまり、私が知りたいのは

A→C,B→C⊢（（￢A)→B)→C

が三つの公理と、もーだすぽねんすだけで導き出せるのかと言うことです。
よろしくお願いします。

回答No.2

itshowsun

公理というのは演繹によって証明されるものではありません。
普通、公理には恒真式（常に真である式）を採用します。
もし他の公理から演繹できるならば、それは公理ではなく定理です。
たとえば
1) φ→(χ→φ)＝￢φ∨(￢χ∨φ)　(交換可能、括弧をはずせるので)
　　　　　　　＝￢χ∨(￢φ∨φ)　(￢φ∨φ＝１なので)
　　　　　　　＝１
よってφ→(χ→φ)は常に真である。
同様に2)と3)もできると思います。

お礼

回答ありがとうございます。

つまり
A→C,B→C,ならばAvB→Cというのは公理なのでしょうか？

確かに公理は恒真式は真であると設定しますが、
この際、真偽は関係なく、前提が真であろうが偽であろうが
公理系での３つの前提とモーダスポネンスから、本題の式が結論出来るかどうか知りたいのです。

例えば、
A→Bから￢B→￢A
を結論したい場合

A→B、￢B,A⊢A→B
A→B、￢B,A⊢A
A→B、￢B,A⊢B　（モーダスポネンス)
A→B、￢B,A⊢￢B
A→B、￢B,A⊢f　（モーダスポネンス)
A→B、￢B⊢￢A　（演繹定理)
A→B⊢￢B→￢A　（演繹定理)

と言ったように

A→C,B→C⊢AvB→C

と示したいのですが、どうすればいいのか分からないのです。

回答No.1

stomachman

公理系と推論規則をセットにしないと、何も証明できません。
　さて、お示しの公理系には"∨"が全く含まれていない。だから、推論規則に"∨"が出て来るのでない限り、この公理系から"∨"を含むナニカが証明できるはずがありません。で、モーダスポンネスとは「（P→Q）とPからQを結論する」という推論規則ですから、結局、"∨"にはお目にかかれない。

お礼

回答ありがとうございます。

証明という言葉を間違って使っていました。
ここで私が知りたいのは、Vを設定し、常に真であると示すのではなく、
モーダスポネンスという推論規則と、上にあげた三つの前提から、
A→C,B→C,からAvB→Cを結論する、

と言う事が可能なのか、と言うことです。
勿論、AとBとCに真か偽か当てはめて、
A→CとB→Cが真の時は、必ずAvB→Cも真になると言うのは分かりますが、それでなく形式的のみで結論したいのです。
つまり、
A→C,B→C⊨AvB→C
ではなく、

A→C,B→C⊢AvB→C

を示したいのですが、どうすればいいのか分かりません。