等式演算(equation calculus)一種形式系統.
它最初是由美籍奧地利數學家哥德爾(Godel , K.於1934年為定義一般遞歸函式類引進並加以討論的.在這種形式系統F中，以等式為研究對象.基本符號有:等號一、常元0(表示數0)、常函詞S(表示後繼)、數變元二。，二，，…、函詞符號fo}fi,"..(n任。，廣表示n元函詞).F的項是指由常元0、變元x、或零元函詞fo及其經過函式S和其他函式遞歸生成的合式表達式.特別地，由0齣發，經S作用逐步生成的項O,SO,SSO,…稱為數字.它們可分別記為0,工, 2,…若t,s為F的項，且/形如廠(，。，，:，…，，)(其中n,i E c},t‑t2,...,t，為不含S之外的任何函詞的項，廣為n元函詞)，則稱t=、為F的一個等式，F中等式組成的有窮集‘稱為一個等式系.當等式系￡中諸等式內所出現的全體函詞為f> > fz,..., f‑所出現的全體變元為Z時，:可特記為
等式演算F的規則僅有下列兩條:
1.代人規則.把某個等式中某個變數的所有出現都用某一個數字作代人.
2.替換規則.若已有fj }C} }C2, ".. }C,n}一。，則可以把某個等式中右邊形如f; <c1}c}}"..,}},)的項用c來替換.
等式演算F，實際上就是基於上述兩條規則得到的關於等式的推導系統.可以利用它定義可計算函式(參見“埃爾布朗一哥德爾可計算函式”、“有窮可定義函式”).
