「古典論理」の形式的体系−ゲンツェンの「自然演繹」 NK   : トピック一覧

 ・古典論理、形式的体系、自然演繹、NK
 ・
  
※論理関連ページ:論理記号/論理法則−同値/同値変形
参考文献総目次


「古典論理」の形式的体系


古典論理

古典論理classic logicとは、
 一般的な数学において
 (特に証明の際に)つかわれている論理のこと。
 





数学の証明で無意識に使っていた(使われていた?)古典論理を、
 明示的に定義しなおすことによって、
 意識的に扱えるようにしたものが、
 次項の「形式的体系」。

数学のなかには、「古典論理」に疑念を呈す流派も存在する。
 このような流派は、
 「古典論理」とは異なるタイプの論理に依拠して、
 議論を展開している。
 たとえば、直観主義、構成主義。
 これらは、
 計算機科学の世界など、数学の特殊な分野で
 重宝されているらしい。





古典論理の形式的体系 

古典論理の形式的体系とは、
 「古典論理」を、
 幾つかの推論規則公理系によって
 明示的に定義した体系のこと。
  [高崎『数理論理学入門I. 記号論理学とは何か- 3. 数学基礎論との関わり]
 





古典論理の形式的体系は、
一つしかないわけではなく、
  ・ヒルベルト流の形式化
  ・自然演繹(NK
  ・シークェント計算(LK)   
など、さまざま。
しかし、
これらの古典論理の形式的体系の違いは、
あくまでも表現方法の違いにすぎず、
これらが表現している《ことがら》は同一。





 





【文献−数学】

 ・『岩波入門数学辞典』「記号論理symbolic logic」(p.124),「古典論理classic logic」(p.209),「真理表truth table」(p.291).
 ・前原昭二『記号論理入門』はしがき(ii):「ゲンツェンによってNKと名づけられた体系」;
             第2章演繹(pp.36-60):「最小論理」「直観主義論理」「古典論理」はp.60。
 ・高崎金久『数理論理学入門I. 記号論理学とは何か- 3. 数学基礎論との関わり-終わりから2段落:数学基礎論(証明論,モデル論,計算論,集合論)  
                                          形式的体系(公理系,推論規則)
                        -5. さまざまな論理体系:古典論理、直観主義論理、様相論理
    
              VI.論理の形式化 :形式的体系(formal system),公理系(axioms),推論規則(inference rules) 
              VII.自然演繹(その1),  

【文献−分析哲学・論理学】

 ・野矢茂樹『入門!論理学』「導入則」「除去則」(p.79);
             ⇒導入則の意味するところ(p.114);
             「標準的な命題論理の体系」(p.146);
             「公理」「公理系」「定理」「形式的体系」(p.171);
             「自然演繹」(p.188);「述語論理の公理系」(p.238):推論規則?
 ・飯田編『論理の哲学』第四章「完全性と不完全性」の前半(pp.84-97)




 


ボクには、よくわからないこと。
  本によって、
   (a) 「推論規則と公理系をあわせて形式的体系」
  としているものと、
   (b) 「推論規則と公理をあわせて公理系」
  としているものがある。
  これは、いったい、どうなってるの?
  このノートでは、当面、(a)にしたがってみることにする。

  *野矢『論理学』1-2(p.49): 


 




→[トピック一覧:古典論理−自然演繹]
→[総目次]


古典論理の形式的体系─「自然演繹」 NK



自然演繹NKは、
 古典論理の形式的体系の一つ。

 以下の「推論規則」と「公理系」によって、
 「古典論理」を明示的に定義したもの。

推論規則

  ・「かつ」の導入則・除去則
  ・「または」の導入則・除去則
  ・矛盾律
  ・「〜でない」の導入則・除去則
  ・「ならば」⇒の導入則・除去則

  ・∀の導入則・除去則
  ・∃の導入則・除去則



公理系
   排中律 (推論規則の形では、二重否定の除去則)
   どの命題も、真偽いずれか。


  (各導入則・除去則の説明には、別ページを用意。
   ここではリンクだけ。title="詳細はclick.")



※上記推論規則・公理系に従う論理が古典論理であって、
 これらに従わない論理は、古典論理ではないから、
 古典論理を用いた議論においては、
 これらの推論規則・公理系は、すべて成立してしまっていることになる。



※「自然演繹」NK以外にも、
 「古典論理」を「形式的体系」として表現する方法は、いくつもある。
  ex.ヒルベルトの形式的体系,LK,
 それらは、同じことを別の表現で述べている。



 以下の「推論規則」と「公理系」からなる「形式的体系」として
 明示的に定義したものの一つ

 以下の「推論規則」と「公理系」からなる
 明示的に定義した「形式的体系」の一つ。








・「自然演繹」NKとは、
 「古典論理」を
 以下の「推論規則」と「公理系」にまとめて表現した「形式的体系」の一つ。


・「自然演繹」NK以外にも、
 「古典論理」を「形式的体系」として明示的に定義する方法は、いくつもある。



※「自然演繹」NK以外にも、
 「古典論理」を「形式的体系」として表現する方法は、いくつもある。
  ex.ヒルベルトの形式的体系,LK,
 それらは、同じことを別の表現で述べている。
  
※数学のなかには、「古典論理」を否定する流派も存在する。
 このような流派は、「古典論理」とは異なるタイプの論理に依拠して、
 議論を展開している。
 ex.直観主義、構成主義。これらは、計算機科学の世界で使われているらしい。

  古典論理   ーその形式的体系:ヒルベルトの形式的体系、NK,LK,…
  直観主義論理
  様相論理
 








【文献−数学】

 ・『岩波入門数学辞典』「記号論理symbolic logic」(p.124),「古典論理classic logic」(p.209),「真理表truth table」(p.291).
 ・前原昭二『記号論理入門』はしがき(ii):「ゲンツェンによってNKと名づけられた体系」;
             第2章演繹(pp.36-60):「最小論理」「直観主義論理」「古典論理」はp.60。
 ・高崎金久『数理論理学入門I. 記号論理学とは何か- 3. 数学基礎論との関わり-終わりから2段落:数学基礎論(証明論,モデル論,計算論,集合論)  
                                          形式的体系(公理系,推論規則)
                        -5. さまざまな論理体系:古典論理、直観主義論理、様相論理
    
              VI.論理の形式化 :形式的体系(formal system),公理系(axioms),推論規則(inference rules) 
              VII.自然演繹(その1),  
 ・向井国昭,http://web.sfc.keio.ac.jp/~mukai/modular/gentzen-NK.pdf :料理のたとえが素晴らしい。
 ・http://en.wikipedia.org/wiki/Natural_deduction
 ・http://de.wikipedia.org/wiki/Systeme_nat%C3%BCrlichen_Schlie%C3%9Fens
 ・http://de.wikipedia.org/wiki/Gerhard_Gentzen
 ・ Untersuchungen über das logische Schließen. I. In: Mathematische Zeitschrift. 39 (2), 1934, S. 176-210.
 ・

【文献−分析哲学・論理学】

 ・野矢茂樹『入門!論理学』「導入則」「除去則」(p.79);
             ⇒導入則の意味するところ(p.114);
             「標準的な命題論理の体系」(p.146);
             「公理」「公理系」「定理」「形式的体系」(p.171);
             「自然演繹」(p.188);「述語論理の公理系」(p.238):推論規則?
 ・飯田編『論理の哲学』第四章「完全性と不完全性」の前半(pp.84-97)




 


ボクには、よくわからないこと。
 古典論理の形式的体系が自然演繹なのではなくて、
 論理の形式的体系として自然演繹があって、
 古典論理を自然演繹という形式的体系に整理したのがNK,
 直観主義論理を自然演繹という形式的体系に整理したのがNJ,
 と言いたいのかなあとも思いつつ、読み進めるが、
 そうなのかどうか、なんだか、判然としない。





【文献】
  



→[トピック一覧:古典論理−自然演繹]
→[総目次]