國立臺灣大學哲學論評

Abstract /

自然演繹系統（natural deduction systems），依其創始者G. Gentzen之立意，係指僅只由一組設定之推衍規則（rules of inference）所構成的邏輯系統。而在此類系統中，一個推衍之建構（the construction of a derivation）係由某些特定的假設出發，利用適當的推衍規則逐步推論出所要的結論。由於此類系統不預設任何設基（axims），因而得以避免有關設基是否為真的哲學爭論。復次，系統中每一規則的訂定，概皆依循相對應之邏輯連詞（connectives）之真值表，如此一來，推衍的運作可以「自然地」按照吾人對於相對應之連詞之（真值表）理解而進行。例如，若由假設P成立，可推知Q亦成立，吾人可斷言P→Q成立。此一推衍顯示結論中的「→」並沒有出現在前提（指P與Q）中，因此，欲由前提得知P→Q，吾人需建立一規則可資引進（introduce）「→」記號。職是吾人可設一「引進」→規則（introduction rule for→）來進行上述推衍。相對地，假設（P→Q）成立而且P成立，吾人可推衍出Q成立，此一推衍顯示在提出現的→記號已不復出現在結論中。因此，吾人可設定一「消去」→規則（Elimination rule for→）來進行上述推衍。整個自然演繹法的建立即在於將此一基本方法應用至所有之連詞。若然對應於每一連詞都有一組「消去規則」與「引進規則」，吾人得以「自然地」進行任何語句的推衍。由於上述優點，自然演繹系統已成為一般認為最優雅的表現方式。　　然則，本文將指出，在一個滿足的自然演繹系統中，對於每一個連詞而言，都應有一組自然的「消去規則」與「引進規則」。而且，更重要的，此一組規則必須是局部完備的（Local-complete）。所謂一組規則是局部完備的，係指所有的中效的句式（Valid Sequents），若其只含此一組規則所關連之連詞。則此一句式可只藉由此一組規則推衍而得。很明顯地，在一般常見的自然演繹系統中，對應對「 」與「 」的一組規則，如Van Dalen d{( I),( E)}與{( I),( E)}，即各具備此一條件。更且，所有中效的句式若其連詞只包含 與 ，則此的句式可利用此兩組規則推衍而得。因此，若針對每一連詞，都有一組完備的規則，則整個系統自然是完備的。「　　就命題邏輯而言，吾人已知{﹁, }或{﹁, }是一組完整的連詞，意謂任一命題皆可利用一只包括﹁與 的語式（formula）來表現。因此，若對於﹁而言，吾人亦可建立一組完備且自然的規則，則此一規則加上對於﹁而言，另一組對於{﹁ }或者{﹁ }的規則都可組合成一個完備且自然的演繹系統。　　然而，本文將討論並指出，目前所常見的否定記號之推衍規則，有些雖是完備的但不夠自然，有些雖是自然的，但本身並非完備，此一觀察顯示出自然演繹系統並非如一般所認為的優雅。就其「自然性」而言，似乎比樹枝法（tableau system）要略遜一籌。就規則組之局部完備性而，言顯然又不如Sequent Calculi。