有窮可定義函式(finitely definable function)亦稱等式系有窮可定義函式.一種由等式系定義的函式.用等式系定義函式的想法最初是由法國數學家埃爾布朗(Herbrand, J.)於1931年提出的.他稱等式系。<f}}fz,...fn,Z)定義函式f，指的是下列兩個條件成立:
1.存在函式fmfz,...,fn，滿足:(f,,fz,...,f,.,z)中所有等式，即3f‑3.fz,...,3fnfz(E(f‑fz,...,fn}z>).
2.若fl,fz,".., f，滿足￡的每個等式，則f} _f.即dzE(fl}fz,…，人，Z)->yx ( f, (x) = f <x)).也即，由E可惟一地刻畫函式f,<=f>.
但是，由於上述條件2缺乏能行性，因此，埃爾布朗的方法不能用以刻畫全體能行可計算函式，實際上，卡爾馬(Kalmar,L.)於1955年證明了埃爾布朗的等式系可定義函式(即有等式系￡來定義的函式)恰好與所謂超算術函式一致，這些函式已大大超出了遞歸函式範圍.克萊瑟( Kreisel , G.)和泰特(Tait,W. W.)於1961年對埃爾布朗的定義進行了改進，把上述條件2改為下列條件:
2'.對每個x，存在有限個Z,,Zz,"..}Zh，使得只要把它們對￡中等式實施代人運算，便可確定f<x>之值.即對每個fl ,f2,... }fn,ECf1,f2,... }fn,Z,}…乙ECfl,f2，…，人,Zp}}fl}x}=f }x}.
此時，稱f為由。而有窮定義的函式.若存在等式系:(有窮)定義函式f，則稱f為(有窮)可定義函式，更明確地稱為等式系(有窮)可定義函式.克萊瑟和泰特還證明了有窮可定義函式恰好為遞歸函式.等式系(有窮)可定義函式的概念，可以很容易推廣到部分函式情況，此時稱為等式系(有窮)可定義的部分函式，或簡稱(有窮)可定義部分函式.
