論理学の質問です

すみません。

論理学の数学寄りの質問です。

演繹とか、推論で、正しい手続きによって、ある結論が得られたとき、その一連の流れを証明という。

とのことですが、一般的な、数学の証明とは、区別すべきと聞きました。

つまり、一般的な、数学の証明は、日本語などの自然言語を、交えた形で構わないが、演繹などの証明は、ただの正しい手続きの羅列にすぎない、形式的な証明ということだと思われます。

この演繹、推論における形式的な証明のことをメタ証明と言い、一般的な、数学の定理の証明などと区別してるという考えでいいのでしょうか？

詳しい人、教えて下さい。お願いします。

質問者からの補足コメント

• 

  なるほど。
  
  つまり、通常の数学の証明は、演繹システムにおける形式的な証明と互いに行き来できるような、対応がある。
  
  ということですね。
  
  つまりは、形式的な証明とは、自然言語を含めて記述された普通の数学の証明から、意味論的なものを取り除いて、数学の証明の持つ、式変形等の構造のみを記号列でつないで表現したものであるが、普通の数学の証明も、形の上では、当然これに従う。
  
  また、逆に、記号列である形式的な証明に、意味的なものを付加して考慮することで、自然言語で記述した普通の数学の証明に置き換えることが出来るということですか？
  
  確認のため、教えて下さい。よろしくお願いします。

  No.1の回答に寄せられた補足コメントです。 補足日時：2017/07/28 14:02

• 捕捉質問:
  
  すみません。再度、質問よろしくお願いします。
  
  一般的な、自然言語で表現された、定理などは、
  簡単な例として、ピタゴラスの定理は、
  
  「３角形が、直角３角形の場合、斜辺aと他の2辺の間に、a^2 = b^2 + c^2が成立する。」のような、表現で与えられると思われます。
  
  これを何かしらの公理系の推論式で、表現するのであれば、
  
  推論形式:直角３角形である。→a^2=b^2＋c^2
  (ここで、→は、推論記号とする)
  
  に対応するということでしょうか？

  No.3の回答に寄せられた補足コメントです。 補足日時：2017/08/03 16:35

• 捕捉質問続き:
  
  このように、自然言語で与えられる多くの定理は、公理系の推論形式で表現できるので、自然言語での証明が、妥当であるならば、公理系における推論に、正しい推論式の羅列(形式的な証明)が存在することになるという理解でよろしいでしょうか？
  
  今の場合、推論の前件が、「直角３角形である。」
  推論の結論が、「a^2=b^2+c^2」
  にあたり、何かしらの公理系において、この間を推論規則で、正しくつなぐことができる(言い換えると、公理系の推論に形式的な証明が、存在する)ので、
  この自然言語で与えられた、ピタゴラスの定理は、正しい定理である。
  
  と考えれる、ということでよいのでしょうか？
  
  不勉強、お恥ずかしいですが、何卒よろしくお願いします。

    補足日時：2017/08/03 16:38

• すみません。上記の、捕捉質問、及び捕捉質問続き
  
  のなかで、公理系の推論、と書いてますが、演繹システムにおける推論、の間違いです。
  
  よって、書き直すと、以下のようになります。
  
  捕捉質問(改):
  
  すみません。再度、質問よろしくお願いします。
  
  一般的な、自然言語で表現された、定理などは、
  簡単な例として、ピタゴラスの定理は、
  
  「３角形が、直角３角形の場合、斜辺aと他の2辺の間に、a^2 = b^2 + c^2が成立する。」のような、表現で与えられると思われます。
  
  これを何かしらの演繹システムの推論式で、表現するのであれば、
  
  推論形式:直角３角形である。→a^2=b^2＋c^2
  (ここで、→は、推論記号とする)
  
  に対応するということでしょうか？

    補足日時：2017/08/03 18:22

• 捕捉質問続き:
  
  このように、自然言語で与えられる多くの定理は、演繹システムの推論形式で表現できるので、自然言語での証明が、妥当であるならば、演繹システムにおける推論に、正しい推論式の羅列(形式的な証明)が存在することになるという理解でよろしいでしょうか？
  
  今の場合、推論の前件が、「直角３角形である。」
  推論の結論が、「a^2=b^2+c^2」
  にあたり、何かしらの演繹システムにおいて、この間を推論規則で、正しくつなぐことができる(言い換えると、演繹システムの推論に形式的な証明が、存在する)ので、
  この自然言語で与えられた、ピタゴラスの定理は、正しい定理である。
  
  と考えれる、ということでよいのでしょうか？
  
  不勉強、お恥ずかしいですが、何卒よろしくお願いします。

    補足日時：2017/08/03 18:24

No.1 ベストアンサー 回答者： t_fumiaki 回答日時： 2017/07/23 21:14

形式的体系で検索して調べて下さい。

「ペアノの算術の公理」を含む形式的体系が普通の数学になります。

形式的体系では、定義・公準から始まり、証明図の積み上げ演算によって、最終的にA→A（トートロジー)が導き出されたら証明完了となります。

この体系の記号列を自然言語に置き換えれば、普通の数学の証明になります。

逆に言えば、普通の数学の命題を形式的な記号列に置換すれば良い訳です。

この方法によって、証明学とか方針学と言った「神学」を除く、「普通の数学」の全てを記述する事が可能となります。

No.3 回答者： t_fumiaki 回答日時： 2017/07/28 15:29

No.1です。

補足に対して。
その通りです。
その体系が「ペアノの算術の公理」を含んでいれば、普通の数学と同等です。

この回答へのお礼

ありがとうございます。

論理学を勉強してるのですが、一般の数学の証明との対応が、分からなかったのです。

例えば、ゲンツェンの自然演繹を公理化した、ＮＰＬでしたっけ？それも、ペアノ公理系を含んだ形なのでしょうか？それくらいは調べますね。

とにかく、ありがとうございます。

お礼日時：2017/07/28 16:06

No.2 回答者： Mokuzo100nen 回答日時： 2017/07/23 22:47

演繹法だけを使う推論であれば、数学の証明と同じと考えて良いです。

だたし、自然言語による推論には帰納法やAbductionといわれる方法もあり、これを使う推論は数学の証明のように厳密な証明なりません。
この推論・論証は、読者が納得するか納得しないかになります。