哥德爾編碼

哥德爾為證明他的不完全性定理而創立的一種算術化方法。他把形式系統的每一元素與自然數建立一一對應：
１．任給形式系統的一元素，可在有限步內算出它所對應的自然數；
２．任給一自然數可在有限步內確定系統有沒有元素與它對應，如果有的話，可在有限步內確定這個元素。這樣確定的自然數稱為形式系統元素的哥德爾編碼。利用哥德爾編碼將形式系統的元數學命題轉化為數論命題的方法稱為元數學的算術化。