ノート:命題論理

simplification について

英語版Wikiの命題計算の項目をご覧になっての編集と推察します。

THEN-1とAND-1は、ほぼ同じ意味合いを持ちます。したがって、どちらも simplification と呼ぶことが可能です。たとえば、「記号論理学」清水義夫、東京大学出版会　では、THEN-1 をsimplification と記述しています。

THEN1 に記載した理由は、命題論理の公理系で、原子記号として含意と否定のみを持ち THEN-1、THEN-2、NOT-1': (¬ φ → χ) → ((¬ φ → ¬χ) → φ) の三つの公理図式と modus pones のみで構成される有名な体系が存在することや、演繹定理 deduction theorem という重要な定理が、THEN-1 と THEN-2のみから導き出せれるという有名な結果が存在することから、この公理を特別扱いする意味があると考えたからです。 Buyobuyo 2006年8月29日 (火) 18:05 (UTC)

「記号論理学」をざっと見てみましたが、THEN-1 がsimplificationとよばれているとの記述は見つけることができませんでした。むしろ、p15にはAND-1のことを law of simplification といっている記述もあります。僕としては (AND-1, 2がすぐ隣にある状況下で)THEN-1の方を simplification と言い切ってしまうことには抵抗があります。その理由は

• THEN-1の直接的な解釈「φだったらχ→φ」は単純化には見えない
• AND-1 を simplification と呼んでいる文献・webページが多くある

といったところです。そもそもの問題は、排中律を認める限り、現在の記事の11個の公理（ゲンツェン流？）に重複があるということなのかもしれません。ここはφ ∧ ψ := ¬ (φ → ¬ ψ)とかしてミニマリズムでいくのがいいかもしれませんね。

Fregean syllogism (Frege's syllogism?) という言い方は一般的なものなのでしょうか。Googleではあまり見つかりませんでしたが、こちらも何かソースはありますか？--Makotoy 2006年8月30日 (水) 04:51 (UTC)

清水論理を引かずに記憶で書いたものなので失礼しました。確認しておきます。本件に関してはネットでは十分な情報は得られないという印象を持ちました。Fregean syllogism とともに、文献に関しては後ほどご紹介します。そのほかのいくつかご質問にお答えします。

• THEN-1の直感的な解釈は「φだったらχ→φ」はではなく、「φで、χで、あるならば φ」と考えてはいかがでしょうか。「A&B → C ≡ A → B → C」が成立することも根拠のひとつです。
• AND-1 を simplification と呼んでいるページが多いのは、ゲンツェンスタイルの構造規則や自然演繹の演繹規則からの類推と考えます。ヒルベルトスタイルで、含意と否定のみを primitive として採用した場合は、「単純化」を担保する公理はTHEN-1です。

些細なことですが、現在の11個の公理系はゲンツェン流ではなく Kleene のスタイルです。　Buyobuyo 2006年8月30日 (水) 09:02 (UTC)

誤解を招くといけないので、追記いたします。 AND-1 を simplification と呼称することを記述に入れること自体は賛成です。Buyobuyo 2006年8月30日 (水) 10:07 (UTC)

各節への修正提案

概要

まず、この記事が数理論理学に関するものであると宣言していることから考えると、用いられている用語が哲学系論理のもののみであることに違和感を憶えました。

例えば、文計算、統語的、整式などの用語は現在数理論理の人々の間では一般的に用いられてはいません。propositional calculusとsentential calculusは日本語ではあまり区別せず、ともに命題計算という用語があてられています。残りの用語は、それぞれ文法的、論理式という日本語が対応する用語として使われるところを多く見てきました。--五穀 2006年9月10日 (日) 20:31 (UTC)

文計算という「訳語」は、哲学系と思われる日本語の論理の教科書でも私は見たことはありません。このあたりは、訳語についても査読依頼がでていますので、随時修正するべきでしょう。整式を「論理式」と訳するというご意見ですが、おそらく、「整式」はwffの訳語として採用されたのかと推察しますが、wffについては、述語論理の項目で、「整論理式 (well-formed formula, 通常 wff と略され、単に「論理式」とも呼ばれる) 」との記載がありますので、この記載に合わせる方が無難でしょう。 Buyobuyo 2006年9月10日 (日) 18:44 (UTC)

述語論理の項目で整論理式と記載されていることを確認しました。先行して記述が充実している述語論理に合わせて、整論理式という訳語をあてるのが無難であるというご意見に同意します。--五穀 2006年9月10日 (日) 20:31 (UTC)

文法

アンパサント(&)とチルダ(~)は、メール等で∧や¬が使えない言語環境の場合に代用されるのが主だと認識しています。ですから、「多くの著者が・・・用いている」というのは、数理論理の場合は当てはまらないと思います。工学系のディジタル回路の著書では多く用いられていますが、本稿の性質上、事情を付記するか本文を書き換えるのが適切でしょう。--五穀 2006年9月10日 (日) 20:31 (UTC)

計算

この節では現在一般的な古典命題論理の体系として認知されている、ヒルベルト流・自然演繹・シーケント計算の体系のいずれかを題材にしたほうが、利用者の便利が良いと思われます。具体案として、NKを用いることを提案します。--五穀 2006年9月10日 (日) 20:31 (UTC)

ヒルベルトスタイルと自然演繹の両方を紹介することに一票です。それと、現行の自然演繹の体系をNKなどの確立された体系に変更するか、内容のチェックを行うことも提案させてください。ちょっと時間がないので計算してないのですが、この体系で A→A や A & ~A → B が証明できるかいささか不安です。Buyobuyo 2006年9月11日 (月) 04:08 (UTC)

ヒルベルト流・自然演繹の両方を紹介することに賛成します。現行の体系については、記述が非形式的で利用者の混乱を招く原因となるような気がします。私が計算したところでは古典論理と考えることも可能ですが、言葉の捉えようによっては A→A や A & ~A → B が証明できない体系とみなされかねません。記述をより形式的なものに修正することは必須として、その方向性として何らかの確立された体系を使うのは、安全性や利便性からも妥当であると考えています。--五穀 2006年9月11日 (月) 11:51 (UTC)

査読ありがとうございます。英語版からの訳をした僕としても、もうちょっとかっちりした形式的な記述にすることに賛成です。ただ、この話題になじみのない人が読みやすいように、わかりやすい方（たぶん自然演繹）を前半で説明して、より形式的なアプローチは「別の論理計算の定式化」で解説した方がいいのではないでしょうか。上にもちょっと書きましたが、「別の論理計算の定式化」でヒルベルト流をやるといいかなあと思います。--Makotoy 2006年9月11日 (月) 14:46 (UTC)

また、再び用語の話ですが前件肯定という用語は一般的でなく、三段論法もしくはモーダス・ポネンスと呼ぶ場合が多いです。 三段論法という用語は混乱を招きやすく、シーケント計算のカット規則が三段論法と呼ばれている場合もままあるのですが、カット除去定理を「三段論法除去定理」と呼ぶことはないので、三段論法という記述でよいと考えています。--五穀 2006年9月10日 (日) 18:31 (UTC)

modus ponens に関しては、いちいち和語に直さずに、カタカナ記載かそのまま用いられることが多いと言うことには全く同意します。しかし、「三段論法」は syllogism の定訳として定着している言葉ですし、意味が広範すぎるので、modus ponens の訳語として用いることには賛成できかねます。modus ponens は三段論法の代表的な一つの形にすぎませんから、無用な混乱を招くので訳語としてはよろしくないのでは？ Buyobuyo 2006年9月10日 (日) 19:16 (UTC)

日本語の百科事典なのだから日本語の用語を、と考えた結果の提案でしたが、実際は「モーダス・ポネンス」で通っていることが多く、かつ意味が正確に伝わるというのが実情です。ここは混乱を招かないためにもカタカナ記載などが無難とのご指摘、理解いたしました。改定案として、「モーダス・ポネンス(modus ponens)」のように、初出の箇所で原語と日本語で主流な発音の両方がわかるように記述することを提案します。--五穀 2006年9月10日 (日) 20:31 (UTC)

「前件肯定（式）」は、現実の会話や授業の中で用いられることは少ないですが、複数のテキストで採用されており、そもそもの modus ponens という言葉の来歴から考えても、紹介することが妥当であるという認識でおります。「モーダス・ポネンス(前件肯定式、肯定式とも modus ponens)」という記述はいかがでしょうか？ Buyobuyo 2006年9月11日 (月) 04:08 (UTC)

「前件肯定（式）」という用語が複数のテキストで採用されているとのことですので、提案いただいた通り併記するのが良いと思います。--五穀 2006年9月11日 (月) 11:51 (UTC)

「命題論理の構成」節の除去

命題論理式の現代的な扱いとずれがあること，記事全体の構成をみて他の節に移すほうが適切であることから，「命題論理の構成」節を除去しました．書かれている個々の事項は興味深いものも多いので，数学史的な視点からの記述や導入節などで改めて必要なものを紹介して頂ければ，と思います．具体的には以下の点が問題だと考えています．

• 構文と意味を分けていない．特に「引数として命題を取り真か偽の値を返す真偽関数と考えることができる」は意味不明．
• 等号を論理結合子として導入している．
• 現代では，「X ∧ Y を論理和、X ∨ Y を論理積と呼ぶ」ことは殆どない．
• 論理的関連の不明な「見立て」だけで説明すべきではない．また，挙げられている法則は形式的に証明できるものであるから「計算」の節などで紹介するのが適当．NGiraffe（会話） 2013年7月16日 (火) 23:05 (UTC)

すごい難しいお話ですね、よくわからないです。移す事が適当であると主張しているのに問題点を挙げて削除しているので、理由の書きぶりおかしくないですか。真偽関数の説明はおかしいですが、他は別にそこまで特別視する話なんですかね。あと、結合命題の標準化はあると思いますが、単純に計算と呼ばれる概念なんて命題論理にあるんですか。--I.hidekazu（会話） 2013年7月17日 (水) 13:45 (UTC)

とりあえず、見立てる云々という記述の除去には賛成。元の記述では、各法則が成り立つ根拠が、類似の代数的な法則であるかのように見えます。--60.132.61.214 2013年7月17日 (水) 13:53 (UTC)

そうですか。--I.hidekazu（会話） 2013年7月17日 (水) 14:06 (UTC)

当該分野の専門家や他分野の知識を持つ人，意識の高い学生が百科事典の読者に含まれることを考えると，実情に合わない記述をすべきではありませんし，難しい話とも思いません．ヒルベルトとアッケルマンの本をベースに記事を改稿されているようですが，最近の教科書や記事(例えば 80年代以降に出版されたもの)は確認されているでしょうか．NGiraffe（会話） 2013年7月17日 (水) 16:41 (UTC)

あ、そうかもしれませんね。８０年代以降でいい本見つけられないんですよね。ご指摘ありがとうございますー。--I.hidekazu（会話） 2013年7月18日 (木) 13:23 (UTC)

i.hidekazu さんへの編集へのコメント

i.hidekazu さんの最近の編集に関して質問します．

1. 等号 '=' を論理記号に含めている理由は何ですか？
2. 自然演繹やシーケント計算などの形式的証明について学ばれたことはありますか？
3. 編集の際，参考にされている書籍や記事を教えてください．

上の節にも少し書きましたが，i.hidekazu さんの編集にはヒルベルトとアッケルマンの 1954年の本以外に出典がありません．命題論理の定式化の歴史として書き留めておく価値はあると思いますが，現代での命題論理の扱いとは随分離れております．百科事典である以上，まずはその時点で標準的な定式化を記述するべきです．特に，最近の編集を見ておりますと，論理式を取り扱うのに真偽関数で評価した値をベースにされており，数理論理学の大きな側面である構文への注目と推論の形式化への配慮が全く見られません．このまま進むと「命題論理」の項として適切でない内容になりそうですので，まずはi.hidekazu さんのお考えを伺いたいと思います．NGiraffe（会話） 2013年8月3日 (土) 23:25 (UTC)

回答

1 等号 '=' を論理記号に含めている理由は何か

• 意図：「〜と〜は同値」という文を表すため。
• 正当性：A = B は (A → B) ∧ (B → A) と等価なので、仮に最初から導入しなくても後々 A = B ≡ (A → B) ∧ (B → A) と定義すれば同じ事であるため。
• 質問：前も要出典と書かれたのですが、これは結局 "=" の記号をつかうことを問題視しているのですか？それとも真偽値の比較を行う論理結合子を導入する事を問題視しているのですか？８０年代以降の本 http://www.amazon.co.jp/dp/4627050003 "≡" の記号を割り当てていますが、真偽値の比較演算子は導入しています。

2 自然演繹やシーケント計算などの形式的証明については学んだ事があるか？

• ない。そもそも現在勉強中であるので、基本であるヒルベルト流の形式体系を記載しています。

3 編集の際、参考にしている書籍や記事は何か

• ヒルベルト、アッケルマンの記号論理学の基礎、小松寿の記号論理学入門、前田昭一郎の束論と量子論理の３册です。

４ ヒルベルト、アッケルマンの記号論理学の基礎には歴史的価値しかなくその内容は古いのではないか？

• 要望：そもそもどのような文献を想定しているのかわからない。良い文献があれば自分もしりたいので具体的に挙げてほしいです。
• 古いという事ですが、自分の呼んだ範囲で現代的な数理論理学の本は命題論理についてあまりページがとられておらず、形式的証明を導入する理由が記載されていない、または非常にわかりにくいです。ヒルベルト、アッケルマンの記号論理学の基礎には比較的その理由が明確に記載されていたため、主に参考としています。また、ヒルベルトのプログラムなどは数理論理学において重要な契機となっているため、参考とする事を問題視する必要は無いと考えます。たとえば、ヒルベルト、アッケルマンを読まないと、

命題論理において、なぜ排中律が重要なのかわからない

構文と意味をなぜ分離できるのかわからない。→恒真命題を扱う事を前提としているので分離できる。→そのためそもそも恒真命題とは何かということを記載しないとつながりとしておかしい。いきなり形式的証明だけを導入するとなぜそんなことをしなければならないのかわからないため。

そもそも、現代的な数理論理学の本を当然何冊も読みはしましたが、そもそも著者達が一体何を言いたいのかわからない。何を言っているのかよくわからないので、自分のわかる本を読んでいるだけです。もしオススメ本がありましたら、私も読んでみますので、著者が一体なにをいっているのか教えていただきますか？--I.hidekazu（会話） 2013年8月5日 (月) 14:12 (UTC)

散発的なもので済みませんがコメントします．

• 論理結合子としての等号について．「正当性」として書かれていることの意味が全く判りません．すぐ後で同じ「等価」を定義するのに敢えて '=' を定義する意味はありますか？
• ご質問について回答しますと，i.hidekazuさんの記載された '=' は真偽関数を使った命題論理式の意味づけにおいてのみ意味を持つように思います．'∧'などの他の記号は特定の意味づけによらず形式的証明においても使われるものですので，同列に定義されることには違和感を覚えます．
• 文献について．命題論理の体系は十分に形式化されていますから，最近の書籍においては「命題論理の基本的な考え方と方法を整理された形で示す」ことが目的になるかと思います．その意味で個別の概念の由来や位置づけの説明が少ないのは確かかもしれませんが，古い文献によって記事を執筆する理由にはなりません．ちなみに排中律が重要なのは命題論理においてというよりも古典論理においてだと思います．
• 私の知っている範囲だと「情報科学における論理」(小野)，「論理学をつくる」(戸田山)，"Logic in Computer Science" (Huth and Ryan)などは論理の形式化について丁寧に書かれていたように思います．(これらの書籍に沿った執筆を望んでいるわけではないです)
• 回答を読んだ限りでは，やはり論理式の形式的扱いについて理解が不足されているのではないかと思います．記事の執筆を急ぐ必要は全くありませんので，一通り勉強を終わらせてから記事全体の構成を再度考えられては如何でしょうか．NGiraffe（会話） 2013年8月10日 (土) 00:12 (UTC)