哥德爾定理是一階邏輯的定理，故最終只能在這個框架內理解。在形式邏輯中，數學命題及其證明都是用一種符號語言描述的，在這裡我們可以機械地檢查每個證明的合法性，於是便可以從一組公理開始無可辯駁地證明一條定理。理論上，這樣的證明可以在電腦上檢查，事實上這樣的合法性檢查程序也已經有了。

為了這個過程得以進行，我們需要知道手頭有什麼樣的公理。我們可以從一組有限的公理集開始，例如歐幾里得幾何。或者更一般地，我們可以允許無窮的公理列表，只要能機械地判斷給定的命題是否是一條公理就行。在計算機科學裡面，這被稱為公理的遞歸集。儘管無窮的公理列表聽起來有些奇怪，實際上自然數的的通常理論中，稱為皮亞諾公理的就是這麼一樣東西。