合式定義形式系統

合式定義形式系統中用初始符號和在先的定義符號確立一個新符號的意義。所謂在先的定義符號是指一個理論中的第一個定義是某一個形式語句，它用該理論的初始符號確立該理論一個新符號的意義。一個理論中的第二個定義是又一個形式語句，它用該理論的初始符號和第一個定義符號確立該理論的第二個新符號的意義。後面的定義亦按此方法處理。

理論中的定義總是依某個確定的次序引進的，這樣就能區分在先的定義符號。這種方法必須滿足可消去性準則和非創新性準則。