形式系統是一個抽象的結構，用于根據一組規則從公理推斷出定理。這些用于從公理進行推理的規則是形式系統的邏輯微積分。形式系統本質上是一個公理系統。1921年，大衛-希爾伯特提出用這樣一個系統作為數學知識的基礎。一個形式化系統可以代表一個定義明確的抽象思維系統。形式主義一詞有時是形式系統的粗略同義詞，但它也指一種特定的符號風格，例如，保羅-狄拉克的辮子符號。

每個形式化系統都由原始符號（它們共同構成一個字母表）來描述，通過推理形成的規則從一組公理中有限地構建一個形式化語言。因此，該系統由通過原始符號的有限組合建立起來的有效公式組成--這些組合是按照所述規則從公理中形成的。更正式地說，這可以表示為以下幾點。一個有限的符號集，稱為字母表，它將公式連接起來，因此一個公式只是從字母表中抽取的有限的符號串。一個由規則組成的語法，從更簡單的公式中形成公式。如果一個公式可以用形式語法的規則來形成，那么這個公式就被稱為形式良好。通常要求有一個決定程序來決定一個公式是否形式良好。一套公理，或公理圖，由形式良好的公式組成。一套推理規則。一個可以從公理中推斷出的形式良好的公式被稱為形式化系統的定理。遞歸如果公理集和推理規則集分別是可判定集或半可判定集，那么一個形式化系統被稱為是遞歸的（即有效的）或遞歸可列舉的。

通過其邏輯基礎對系統的尾隨是形式化系統與其他可能在抽象模型中具有某種基礎的系統的區別所在。通常，形式化系統將是一個更大的理論或領域（如歐幾里得幾何）的基礎，甚至與模型理論等現代數學中的用法一致。

形式語言是一種由形式系統定義的語言。與語言學中的語言一樣，形式語言一般有兩個方面。語言的語法是語言的樣子（更正式地說：語言中有效語詞的可能表達的集合），在形式語言理論中進行研究。語言的語義是語言的語詞的意思（根據有關語言的類型，以各種方式進行形式化）。形式語法是對一種形式語言的語法的精確描述：一組字符串。形式語法的兩個主要類別是生成語法和分析語法，前者是關于如何生成語言中的字符串的一套規則，后者是關于如何分析一個字符串以確定它是否是語言的成員的一套規則。

簡而言之，分析性語法描述了如何識別字符串是集合中的成員，而生成性語法則描述了如何只書寫集合中的那些字符串。在數學中，形式語言通常不是由形式語法描述的，而是由（a）自然語言，如英語描述的。邏輯系統是由演繹系統和自然語言共同定義的。而演繹系統又只由自然語言來定義（見下文）。

一個演繹系統，也被稱為演繹裝置或邏輯，由公理（或公理圖）和推理規則組成，可用于推導系統的定理。這樣的演繹系統在系統所表達的公式中保留了演繹的品質。通常，我們所關注的品質是相對于虛假的真理。然而，其他的模式，比如說理由或信念，也可能被保留下來。為了維持其演繹的完整性，一個演繹工具必須是可定義的，而不需要參考語言的任何預期解釋。其目的是確保推導的每一行僅僅是其前面幾行的句法結果。對語言的任何解釋都不應該涉及到系統的演繹性質。演繹系統的一個例子是一階謂詞邏輯。

一個邏輯系統或語言（不要與上面討論的那種由形式化語法描述的形式化語言相混淆），是一個演繹系統（見上面一節；最常見的是一階謂詞邏輯），加上額外的（非邏輯的）公理。