• 有限集合を1つ固定し、その有限集合の元をアルファベットという。
• アルファベットの有限列を語という。
• 語の集合を言語という。

• 言語を1つ固定し、その言語に属する語を命題という。

• 命題の集合を1つ固定し、その集合に属する命題を事前に認められた仮定として採用し、それを公理と呼ぶ。
• 命題の有限個の組がどのような条件を満たせば、それらの命題から別の命題が導けるのかを決めたルールの組を決め、それらのルールを推論規則という。
• 公理の集合と推論規則の集合の組を公理系と呼ぶ。

Aを公理系とし、(P_1,...,P_n) を命題の列とする。

任意の i≦n に対し P_i が

• P_i は公理である
• P_i は、P_1,..., P_{i-1} から、許された推論規則によって導くことができる

のいずれかを満たすとき、(P_1,...,P_n) を P_n の（公理系 A における）証明と言う。

ある (P_1,...,P_n) があって、(P_1,...,P_n) が P_n の証明であるとき、P_n は（公理系 A において）証明可能である、もしくは P_n は定理であると言う。