命題を記号によって表現し,推論を純粋に記号の操作とする数学の考え方.
命題を記号列であると考え,公理は記号列を変形する出発点としての記号列とします.また,記号列の変形規則を推論と呼び,変形した結果に出てきた記号列を定理とします.
形式主義では,命題は規則に則って記号を書き並べた単なる論理式であって,真とか偽という値は持ち合わせていません.
ヒルベルト David Hilbert は,特定の命題が公理系から形式的推論によって導出できるか否かということを,有限的手続きによって判定できるかという問題（決定問題）を呈示しました．もし,この問題が解けるならば,数学を扱う万能の方法が得られます.
これに対して,ゲーデルは1931年に形式的体系の公理系に自然数論の公理系が含まれる限り,形式的推論では証明も反証もできない論理式が存在する,という「不完全性定理」を提示します.
さらに,1936年,アロンゾ・チャーチは 「An unsolvable problem of elementary number theory（初等整数論の非可解問題）」によって,アラン・チューリングは「On computable numbers, with an application to the Entscheidungsproblem （計算可能数，ならびにその決定問題への応用）」によって,ヒルベルトの決定問題を一般的に解く有限的手続きは存在しない,ということを示しました.
Mathematics is the language with which God has written the universe.