根岑謂詞演算系統

根岑謂詞演算系統(Gentzen system of predi- cate calculus)古典的和直覺的謂詞演算系統的總稱.根岑系統是根據根岑(Gentzen , G.)提出的根岑方法建立起來的,根岑方法的兩個顯著特徵是:
  1. 通常的公理系統是儘量使用較少的規則,為此而不惜增加公理.但根岑方法與之相反,寧可增加規則而減少公理.在兩種根岑系統中,公理均只有一條,但規則卻很多.
  2. .大多數謂詞(或命題)演算系統都使用分離規則,而該規則的特點是由繁到簡,即由公式a和a--> 月得到公式月,月為a-->}3的子公式.以被證公式月為子公式的公式有無窮多個,所以月是否可證不能行地判定.但是在根岑系統中,除切痕規則外,其他規則都是由簡到繁,即前提公式是後承(被證)
    公式的子公式.根岑還證明了在他的系統中所有可證公式均可不使用切痕規則來證明,因而在根岑系統中,一個公式是否可證,可以能行地判定.根岑系統的這些特點使得它在計算機科學中有著廣泛的套用.該系統是根岑於1934年建立起來的.

相關詞條

熱門詞條

聯絡我們