先由兩個小故事引入：
我們在現實的生活中，那只憨憨的烏龜很快就被我們追上，莊子的壹尺之捶幾天也就可以用完了。可是，如果我們把它放到我們的腦海意識中，我們發現烏龜居然追不上了，壹尺的捶也用不完了。看是不是很奇怪？
組成我們人體的粒子到底是無數個還是有數個？最小的粒子是否可以繼續分割？
偉大的量子理論也是由此開始的。
妳能產生WU嗎？
首先我會提供妳壹個符號串（WJ），然後告知妳壹些規則，通過運用規則將壹個符號串變成另外壹個。 如果某條規則在某處是適用的，並且妳可以選擇使用或者不使用，如果有多條規則適用的話，那麽完全取決於妳自己。
好了，規則清楚了，下面我們來試著推導壹個符號串， WUJJU 怎麽產生出來的？
（1）WJ ------這是我們所擁有的符號串，稱之為 公理
（2）WJJ ------使用規則2，從（1）中得到
（3）WJJJJ ------使用規則2，從（2）中得到
（4）WJJJJU ------使用規則1，從（3）中得到
（5）WUJU ------使用規則3，從（4）中得到
（6）WUJUUJU -----使用規則2，從（5）中得到
（7）WUJJU ------使用規則4，從（6）中得到
那麽我們把（2）-（7）形成新符號串稱之為 定理
當然我們還有壹種方法，那就是窮舉法
第壹步： 公理 WJ 我們把全部的規則使用壹次，這樣我們就會得到新的定理：WJU，WJJ。
第二步：我們將WJU，WJJ分別使用應用壹次全部規則，可以得到新的定理：WJUJU，WJJU，WJJJJ。
第三步：我們將WJUJU，WJJU，WJJJJ，分別使用應用壹次全部規則，可以得到新的定理：WJUJUJUJU，WJJUJJU，WJJJJU，WJJJJJJJJ，WUJ，WJU，
第N步：...
這樣的話，我們就可以得到所有的 定理 。
下面我們來聊壹下歐幾裏得的壹個定理：它只有兩步，便能得到結論
上面的邏輯推論我想大家都會接受吧，所以我們只需要認為A和B為真，則必定認定Z也是真的。假如，我們不認為A和B為真呢？那麽是不是就無法得到Z這個結論？看來上面的定理中，缺少是壹條A,B為真的步驟，我們稱之為C吧。
好了，這下應該不會有問題了吧，等等，假如有人不認為A,B和C為真呢?我們只好在推導步驟中，繼續加入D:如果A,B和C都為真的話。啊哦，問題來了，如果我們想要得到結論Z，那麽就得我們需要加入E，F，G...等無數個步驟。糟糕，又壹個 “芝諾悖論”
1.pq系統
我們知道pq系統中存在著無窮多條 公理 。由於不能把它們全部寫出來，我們只能由另外的方法描述它們。實際上我們不僅需要對於公理的描述，還需要壹種辨別某個給出的符號串是否是壹條公理的方法。對於公理僅僅做壹個描述也許能充分的刻劃它們，但是這種刻劃是很弱的——與WJU系統中對於定理的刻劃所存在的問題是壹樣的。我們並不想僅僅為確定某個符號串是否是公理而花費壹段不知道有多長的（甚至是無限長的）時間。所以，我們將給公理這樣下定義，使得對於由p，q和短杠所組成的符號串是否是壹條公理，有壹個明顯的判定過程。
請註意 “x” 在兩次出現時必須是代表同壹串短杠。比如： ---q--p- 是壹條公理。
當然 “x-qxp-”這個表達式本身並不是壹條公理（因為 “x” 不屬於pq系統）。它更像是壹個鑄出所有公理的模子——它被稱做公理模式。
pq系統只有壹條生成規則：
正像生成規則通常的形式那樣，這個陳述在壹個符號串是否是 定理 與另壹個符號串是否是 定理 這兩者之間建立了因果關系，但並不斷定這些符號串本身是否是定理。
2.判定過程
我們知道pq系統中的每壹條定理都是有三組分離的短杠，並且起分離作用的成分依次為q，p。（這可以由基於“繼承性”的壹個論證證明，就是證明WJU系統中的定理都是以W開頭的那種方法）。也就是說，僅僅 從形式上 ，我們就可以排除像 ---------q--p--p--p-- 這樣的符號串，它並不是壹條定理。
那麽是 從形式上 呢？
不管在什麽樣的情況下，我們把任何壹個以壹組短杠開頭，然後有壹個q，接著是第二組短杠，然後是p，最後再跟上另外壹組短杠，這樣的符號串都叫做 “構型良好的”（簡稱良構） 符號串。
每個 定理 都會有壹個判定過程，比如，假定給了壹個符號串，首先，檢查它是不是壹條公理（我們來假設有壹個判定公理的判定過程——否則壹切就都沒有希望啦）。如果它是壹條公理，那麽它也可以稱作是壹條定理，這個測試就完畢。於是再假設它不是壹條公理，那麽，它要是壹條定理，就壹定是從壹個較短的符號串得出來的，在逐條地試用各條規則時，不僅能準確地找出可能產生那個符號串的規則，而且還能準確地找出哪壹個較短的符號串會是“家譜”中它的上壹代。用這種方法，把問題“歸約”成為去確定幾個新的，但是較短的符號串是否都是定理，然後對它們依次的進行同樣的測試。可能出現的最壞情形時產生出大量的，越來越多的，但是越來越短的需要測試的符號串，當以這樣方式壹步壹步的回溯時，就壹定會距離壹切定理的源泉——公理模式越來越近。
3.自底向上之別於自頂向下