期刊刊名：揭諦 卷期：22期
篇名出版日期：2012年1月1日
作者：傅皓政
語言：Chinese
關鍵字：可決定性,自然演繹法,樹枝法,語意真值圖,證明,decidability,natural deduction,tableaux system,semantic tableaux, proof
被點閱次數：66次
閱讀時間：3922sec
摘要： 邏輯經驗論者R. Carnap在1930年提到，雖然G. Frege的新邏輯出現已逾數十年，但是大部分的教科書仍未意識到新邏輯與Aristotle的舊邏輯有著根本上的差異。有趣的是經過數十年的發展，我發現古典邏輯的演算系統也出現相同情況，截至目前為止，大部分的教科書也未意識到樹枝法的重要性，主要原因在於雖然在限定的範圍中，樹枝法和真值表法同樣能夠提供證明可決定性的程序，卻無法如自然演繹法等以直接證法為主要證明策略的方法一般，呈現如何從前提逐步推論到結論的過程。但是，以直接證法為主要證明策略的演算系統而言，無論是公理法或自然演繹法，要建構這類演算系統的證明其實有個困難之處，因為這些演算系統並未提供如樹枝法般能夠有效率地找到證明的操作程序。不過，在這篇論文中，我要說明的是樹枝法不但具有找到證明的操作程序，而且透過樹枝法的原型，即E. W. Beth提出的語意真值圖，還能夠進一步建構自然演繹法的證明，如果透過Beth的方法能夠成功地建立樹枝法與其他以直接證法為策略的演算系統之間的轉換形式，那麼對於建構以直接證法為策略的演算系統的證明將會有相當大的助益。
[ 關閉視窗 ]