用計算技術的術語來說，就是存在著正確的程序，它們的正確性是在任何一種程序邏輯中都無法證明的。換言之，對於建立在古典的一階邏輯之上的任何一種程序邏輯而言，如果它是協調的，那麼它就是不完備的。對於建立在無窮邏輯之上的程序邏輯而言，那就是另外一回事。建立在無窮邏輯上的程序邏輯是完備的，但這種邏輯與現實計算的關係是微弱的。
形式化的“陷阱”
在本世紀初被發現的那些“邏輯悖論”中，最有名的是悖論，它說明了邏輯與集合論的有些基本假設是錯誤的。
概括性原則
所謂“概括性原則”可陳述如下：
對任一給定的集合而言，存在著一個謂詞，使得是集合的刻畫性質；並且對任-特定的謂詞？，存在集合使得以為其刻畫性質。
上述命題中的後半句在集合論的早期曾被默認為假設，後來證明了它是錯誤的。悖論以及其他若幹種悖論都可以溯源於這一錯誤的假設。
“邏輯悖論”如“悖論”是任意定義的謂詞，對這些謂詞而言，不存在相應的集合。
這一事實應該看作對1現在正在研究各種謂詞的計算機科學家的一種警告，這說明當我們引人新的謂詞時，我們必須設法證明和這些謂詞相應的集合是存在的。
歸納法原則是錯誤地賴了。我們對實際可算件的直觀概念進行形式化時所遇到的困難，可以歸納為同樣的原因。實際可計算性概念複雜理論中已被形式化為多項式時間可計算性，即：函數就沖算而言是可行的，當且僅當是多項式時間的述原理時常被稱作，這一原理至今在計算技術界未被普遍接受，因為從直觀上來看，複雜性為函數很難算做實際可計算的函數。看來可行性這一概念包含了“小的”這一概念，詳細地說，是“時間、空間足夠小到在一台現實的計算機上可計算”這一概念。由此可得出教訓即：在形式化過程中，數學歸納法原則不應當用於那些含混的，不能看作是算術的概念。
形式化恰當性的論證
直觀概念或一組直觀判斷的形式化，可以看作是一個直觀概念映射到數學理論中的一個相應的精確概念，或者是一組直觀判斷映射到一個數學係統之中。將直觀概念“能行可計算性”映射到“遞歸性”可計算性，這種映射過程是成功的，而將可行性映射到“多項式時間可計算性”就不是很成功了。將這兩種情形加以比較（也就是將論題和作-論題加以比較）將對於直觀概念的形式化問題起澄清作用。
一個直觀概念的形式化，例如論題或論題中包含的那種形式化，是將一個詳細說明了的直觀概念的內容借助於一個形式化的概念加以捕捉（形式概念是一個在邏輯-數學係統中有定義的概念所以，一個詳細說明了的形式概念是否確切的問題是不能用形式的方法加以證明的，而隻能用經驗的證據加以證實或否證。對於論題這一論題是說一個函數是能行可計算的，當且僅當它們是遞歸的我們認為其中包含的形式化是充分的，因為至今沒有發現反例。另一方麵，對論題而言這一論題是說一個函數是實際可計算的，當且僅當這個函數是多項式時間可計算的，我們容易發現直觀的反例（例如，複雜性為函數所以在其中所包含的形式化過程是可疑的）。
一組直觀判斷的形式化的可靠性，也就是將一組直觀判斷映射到一個詳細說明的邏輯數學係統之中，我們必須訴諸於經驗。在他1947年發表的《什麼是連續統問題》一文中指出，集合論的公理是和物理令中的假設類似的。它們的正確性是由經驗來保證的，雖然在這個情形中.它是通過間接的方式。
這一事實說明一個詳細說明丫的直觀概念或一組直觀判斷的形式化的！：確性，隻能通過經驗的方式來加以證實。
結束語
有些計算機科家近年來認為：形式化方法對計算機科學是必要的，正如數學對是必要的。這一事實看來已被計算機科學家中的大部分人所承認看來尚未得到足夠注意的問題是.形式化方法是燈隻限件的,關於是有可能出現“陷阱”的。在這方麵，對於形式化在邏輯學的數學中應用的曆史進行研究將足很有幫助的。