導言
形式化問題是邏輯學數學以及燈的技術科學中的中心問題。這科學家中廣泛地應用了形式化方法（或者說“形式方法”）。而關於究竟什麼是形式化，有概念有待於澄清。例如形式化與嚴格化、形式化與公理化、形式結構與解釋等等。其次近代數理邏輯與數學基礎的重要結果就是發現形式係統（也就是形式方法本身）是有局限性的。對複雜到一定程度的形式係統而言，如果它是邏輯上無矛盾的，則它必然是不完備的（即並非所有的真命題都是可證的，必然是不可判定的（即不存在可以用來判定其中的任一命題是否是可證命題的算法）；它的真的概念在係統中是不可定義的。真理性概念的不可定義性定理分別表達了形式係統的上述的三方麵的局限性。
還有，形式方法在用時，還會導致邏輯上自相矛盾的結果，即導致“悖論”（所謂“悖論”是一個命題，由設定它為真，可以推出它為假；而由設定它為假，可以推出它為真。例如古希臘時代就已經發現的“說謊者脖論”）集合論在早期發展中，曾發現了不止一個的悖論其中最有名的是“俘論”（“由所有不包含自身的集合組成的集合”）。本世紀前五十年中，有些木這是為1985年12月在北京召開的《金嶽霖學術思想討論會》寫的一篇短文。金先牛是最早係統地介紹數理邏輯到中國的人之一。因此我在紀念他的會上獻上這篇小文，也許是可以的。作者著名的數學家和邏輯學家所構造的形式係統，如在30年代初提出的關於轉換的理論和在1940年提出的集合論係統不久都被發現可以在其中推出“悖論”。現在的演算和係統都是經過修改的。集合論和邏輯的早期發展史中這些教訓，是在應用形式方法時必須記取的。
關於形式化的幾對概念
形式化與嚴格化形式化和嚴格化是不同的兩個概念。這裏所說的“嚴格化”指要求一個理論，一個係統滿足數學嚴格性，而數學嚴格性是指在下定義和進行證明過程中的嚴格性。具體說來，是兩條要求，即除初始概念以外，任何概念必須有由初始概念或已經定義過的概念構成的定義。除初始命題(即公理）以外，任何斷言必須是經過證明的，不允許引進初始命題以外的假定作為證明的根據。符合上述要求，就算是滿足了嚴格性的要求，而這是不容易的。數學史上不乏違反上述要求的例子。如選擇公理（“對任一給定的由集合構成的集合8而言，從每一元素中選取一個元素，放在一起，即構成一個新的集合”）是20世紀初年才正式提出的，而在此以前，已經在集合論和其它數學分支中被不止一次地，在證明定理時用到過。
這種引用未經明確提出的前提的錯誤，又有幾種情形。一種是引用的前提是可以當作公理來用的，錯誤隻在於沒有明確提出，關於選擇公理的例子就屬於這種情形。另一種情形是，引進的假定是不能成立的。在本世紀20年代中曾一度自認為已解決了連續統問題，並做出了一個證明大綱。後來發現，這個證明是錯誤的，錯誤在於假定一切自然的集合都是遞歸的，而這是一個假命題，就是一例。
形式化自然要求嚴格化，但嚴格性的要求並不限於形式係統，非形式化的數學也要求具有嚴格性。
形式化與公理化公理係統+—定是形式係統，因形式化與公理化是不同的，但在近代數學中，形式係統大都是形式化的公理係統。
我們在此附帶討論，形式化與數學化（即數學的刻畫）這兩個概念。數學指抽象化與嚴格化，和限於使用演繹推理。形式化可以說是這幾個特征都具有，而抽象化的程度高於數學化。
形式結構解釋個形式係統的形式結構與其解釋的關係問題，也就是當我們將這一係統看作一種語言時的語法與語言的關係.一種形式語言有它的語法語言兩種不同的性質。而所說的一種特定的語言中一個表達式的形式語言，實際是指另一特定的形式語言中一個某種映射關係的表達式
形式化的局限性
如前所述係統，如果它是無矛盾的，那麼它就具有下列的局限性，不完整性，在1931年證明了下列的重要定理。
“如果一個形式的數學理論是足夠複雜的，而且它是無矛盾的，那麼在這一理論中存在一個語句，而這一語句在這一理論中是既不能證明。”
這裏所說的“足夠複雜的”是有嚴格定義的，也就是：複雜到所有的遞歸函數在其中都能夠表示而所說的“所有遞歸函數在其中都能夠表示”就是說，設有任何自然數，如果在這一形式理論中有一表達式，表達一個真命題。
如具體地構造出來一個非常奇特的語句，這個語句斷言，本身是不可證的（也就是說，它本身是不可證的然後他證明了這個語句構成一個遞歸謂詞，而且是既不能證明，從而證明了上述定理，這個語句在後來的文獻中，被稱作語句。容易看出語句和古希臘時期已經發現的下列語句“我正在說謊”類似，但是不同，因為由“我正在說謊”之真可以推出它為假，而由它為假又可以推出它為真。因之是一個“悖論”，而哥德爾語句卻不構成“悖論”。