推論規則と定理、公理は違うもの?

質問

推論規則というものがイマイチ何なのかよく分かりません。
公理や定理などとは違うものなのでしょうか?

これまで本など読んだところの印象だと、定理でも公理でもよくて
A → B
の様な形になっていればいいのかなぁと、勝手に思っています。
(↑が正しい場合、もちろん A ⇔ B でもいいと思っています)

ただ僕が思っている事が正しい場合、何でわざわざそんな言葉を使いたくなるのかが、やはり分かりません。
公理や定理という言葉を使っていれば十分ではないかと思うのです。
それは単に僕が不勉強なので、その言葉が便利だと思う状況を知らないだけなのかもしれませんが、そういう状況をご存知であれば教えて下さい。
なにかキーワードの様なものでも結構です。

よろしくお願いします

回答No.3

alice_44

何を公理にして、何を推論規則にするかは、
作った人が、その日の気分ではなく、それなりの考察の上で、
主観的に主張したものです。
様々な人が、様々な論理系を提案しています。
それぞれに特徴があり、どれが正しいというモノではありません。
貴方の引用 URL でも、「形式的定義」の節で
いくつか紹介していますね。

回答No.2

alice_44

公理や定理は、論理式です。
論理式とは、論理系の定めるルールに従って記号を並べたモノのこと。
論理系の定義時に真であると仮定された論理式が、公理。
論理系によって真であると証明された論理式が、定理。
推論規則は、定理から別の定理を導く変形ルールを記述したもので、
それ自体は論理式ではありません。

公理と定理の区別には微妙な部分があって、同値な二つの定義がある場合、
どちらを公理に採用して、他方を定理として証明してもよいですから、
どっちが公理か定理かというのは、多分に恣意的、規約的なものです。
それに対して、公理・定理と推論規則の間には、
前者が論理式で後者は論理式でないという明確な区別がありますから、
どちらでもよいという訳にはいきません。形式的には、全く別のものです。

では、数学の内容のどれが公理で、どれが推論規則かというと、
それは論理系を定義するときのやり方によって異なり、
やり方は唯一ではありません。
自然演繹の体系は、豊富な推論規則を持ちますが、
ヒルベルト流だと、粗方を公理にしてしまうので、三段論法しかありません。
何が公理で、何が推論規則かは、論理系をどのように定義したか次第なのです。

お礼

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

> 公理や定理は、論理式です。[snip]
なるほど、であるなら推論規則は、それ自体が 真 or 偽 という値を持たない
という点で、公理と区別できるという事ですね。

> 推論規則は、定理から別の定理を導く変形ルールを記述したもので、
細かい話で済みませんが、「定理から別の定理を」は
「定理もしくは公理から別の定理を」ですよね?

> 公理と定理の区別には微妙な部分があって、[snip] 多分に恣意的、規約的なものです。
僕も、命題論理の公理が ∧,∨,⇔ を使ったものと、
→ を使ったもののパターンなどを見た事があります。
いろいろ言い出せば、四則演算だって色んな公理から組み立てる事もできるし、
それ自体を公理にしても良いなどという事になるのですよね。

> では、数学の内容のどれが公理で、どれが推論規則かというと、
> それは論理系を定義するときのやり方によって異なり、
> やり方は唯一ではありません。
どれを公理にして、どれを推論規則にするのか? という合理的な理由が知りたいです。
例えば
http://ja.wikipedia.org/wiki/%E8%87%AA%E7%84%B6%E6%BC%94%E7%B9%B9#.E8.87.AA.E7.84.B6.E6.BC.94.E7.B9.B9.E8.AB.96.E7.90.86
に、「モーダスポネンス」や「二重否定の規則」が規則(これは推論規則の事ですよね)だとありますが、それぞれ
A ∧ (A → B) → B
￢￢A → A
という公理ではダメなのでしょうか?
実は合理的な理由などなく、どちらでも良いので、作った人がその日の気分でなんとなく推論規則にしてしまったという程度のものなのでしょうか?

質問を出した後で気付いた事ですが、代入など字句的(syntax)操作(といえばいいのでしょうか?)であれば、公理ではどうにもなりそうもないので、「推論規則が全て公理に書換えられるわけではない」というところまでは、理解が進みました(進んだつもりかもしれませんが)

もしよろしければ、回答お願いします

回答No.1

uyama33

"PROOF THEORY"
という本が
NORTH-HOLLAND 社
から出版されています。
著者は、竹内外史　さんです。
この本を読まれることをお勧めします。
昔買ったときの値段は25000円でした。
高いです。
ここでは、
　論証を進めるときに
使ってよい規則について明確に記載されています。
たとえば、
Γ→Δ
のとき、
D,Γ→Δ
としてよいとか、などなど
これらを推論規則といいます。

お礼

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

折角紹介してもらったのですが、本の方は見付ける事はできましたが、とても高くて、買っても現状の僕には読めそうもないので、今のところは遠慮しておきます。読めそうになったらまた考えます(多分僕よりもこれを生かす事のできる人が世の中にいると思いますし)。

> Γ→Δ
> のとき、
> D,Γ→Δ
の部分は、よく分からなかったのですが、時間を置いて考えやっとピンときました

Γ→Δ
-------
D,Γ→Δ
とか書くやつですね。
僕の持っている同じく竹内外史先生の「層・圏・トポス」の直観論理のところに「増左」として載っているのを思い出しました。

具体例が出て僕としても考えやすくなったので、よろしければ関連して答えて頂きたいのですが、この推論規則を

(Γ→Δ) → (D∧Γ→Δ)

という公理で置き換えると何か都合が悪いのか? という事が知りたいです。
これでは、同じ機能を果せないでしょうか?