在邏輯學和數學中，形式證明或推導是一個有限的句子序列，其中每個句子都是一個公理，一個假設，或通過一個推理規則從序列中的前面的句子推導出來。它與自然語言論證的不同之處在于，它是嚴格的、不含糊的和可機械地驗證的。如果假設集是空的，那么形式化證明中的最后一句話就被稱為形式化系統的定理。定理的概念在一般情況下并不有效，因此可能沒有任何方法可以讓我們總能找到一個給定句子的證明或確定不存在。菲奇式證明、順序計算和自然演繹的概念是對證明概念的概括。該定理是證明中它前面的所有形式良好的公式的語法結果。為了使一個形式良好的公式有資格成為證明的一部分，它必須是對證明序列中前面形式良好的公式應用演繹裝置的規則的結果。形式化證明往往是在交互式定理證明的計算機幫助下構建的。重要的是，這些證明可以自動檢查，也可以通過計算機檢查。檢查形式證明通常很簡單，而尋找證明的問題通常在計算上是難以解決的和/或只是半可解的，這取決于使用的形式系統。

形式語言是一組有限的符號序列。這樣的語言可以在不參考其任何表達的任何意義的情況下被定義；它可以在任何解釋被分配給它之前就存在，也就是說，在它有任何意義之前。形式證明是用一些形式語言表達的。

形式語法（也叫形成規則）是對形式語言的良好形式公式的精確描述。它與形式語言的字母表上的字符串集合同義，這些字符串構成形式良好的公式。然而，它并不描述它們的語義（即它們的含義）。

形式系統（也叫邏輯微積分，或邏輯系統）由形式語言和演繹裝置（也叫演繹系統）組成。演繹裝置可以由一組轉換規則（也叫推理規則）或一組公理組成，或者兩者都有。形式系統被用來從一個或多個其他表達式中推導出一個表達式。

一個形式化系統的解釋是對符號的意義的分配，以及對形式化系統的句子的真值。對解釋的研究被稱為形式語義學。給出一個解釋與構造一個模型是同義的。