可判定邏輯系統

可判定邏輯系統(decidable logic system)具有能行判定算法的邏輯系統一個邏輯系統S是可判定的，是指存在一個能行的算法，使得該算法能夠判定S中的任何公式是否可證.若使用哥德爾編碼，則可以得到更為精確的描述。

具體定義

若G是S中公式到自然數集的一個能行一一映射，且對S中可證公式的集合P,G(P)為遞歸集，則稱該邏輯系統可判定，否則稱其不可判定.最基本的可判定邏輯系統是古典命題演算系統.此外，像直覺主義的命題演算系統、模態邏輯的命題演算系統(包括T,K4,S4,D4,S5)都是可判定的.有窮值邏輯的命題演算系統也是可判定的，但它們相應的一階謂詞演算系統都不可判定.不過它們的一些子類仍然是可判定的.

系統子類

目前已知的可判定的古典一階謂詞演算系統的子類主要有:

1.只含一元謂詞的公式類.
2.只含等號，不包含其他謂詞、函詞的公式類.
3.形為E/xlE/xZ...dxm} yu yZ"..} y A的公式類.
4.形為yxl yxz ... dxm } y, 3yZ ".. 3 y dzl yzZ "..d zA的公式類.
(在子類3和4中，A為不含量詞、函式符號與自由變元的公式)