論理式の有限列 A_{1}, ·, A_{n} を Γ, Π, Δ, Λ などで表す．この LK では

A_{1}, ⋯, A_{m} ⊢ B_{1}, ⋯, B_{n}

というもの（以下これを式と呼ぶ）が対象となる．後でわかることであるが，この式に込められている気持ちは「A_{1}, ⋯, A_{m} のすべてが成立しているとき B_{1}, ⋯, B_{n} のうちどれかが成立する」ということである．また m = 0 または n = 0 つまり A_{1}, ⋯, A_{m} あるいは B_{1}, ⋯, B_{n} が空列である場合も含めてとりあつかっている。

公理は論理式 A について

A ⊢ A

である．

推論規則は式の構造についての推論と各々の論理記号に関連しての推論にわけられ，横線の上にある１つあるいは２つの式（上式）から横線の下にある１つの式（下式）を導くという形式である．まず式の構造についての推論規則について述べる．

増 :

左 : \frac{Γ ⊢ Δ}{A, Γ ⊢ Δ}, 右 : \frac{Γ ⊢ Δ}{Γ ⊢ Δ, A}

減 :

左 : \frac{A, A, Γ ⊢ Δ}{A, Γ ⊢ Δ}, 右 : \frac{Γ ⊢ Δ, A, A}{Γ ⊢ Δ, A}

換 :

左 : \frac{Γ, A, B, Π ⊢ Δ}{Γ, B, A, Π ⊢ Δ}, 右 : \frac{Γ ⊢ Δ, A, B, Λ}{Γ ⊢ Δ, B, A, Λ}

三段論法 :

\frac{Γ ⊢ Δ, A A, Π ⊢ Λ}{Γ, Π ⊢ Δ, Λ}

次に論理記号に関する推論規則のついて述べる．

¬-左 : \frac{Γ ⊢ Δ, A}{¬A, Γ ⊢ Δ}  ¬ -右 : \frac{A, Γ ⊢ Δ}{Γ ⊢ Δ, ¬A}

∧-左 : \frac{A, Γ ⊢ Δ}{A ∧ B, Γ ⊢ Δ} および\frac{B, Γ ⊢ Δ}{A ∧ B, Γ ⊢ Δ}

∧-右 : \frac{Γ ⊢ Δ, A  Γ ⊢ Δ, B}{Γ ⊢ Δ, A ∧ B}

∨-左 : \frac{A, Γ ⊢ Δ  B, Γ ⊢ Δ}{A ∨ B, Γ ⊢ Δ}

∨-右 : \frac{Γ ⊢ Δ, A}{Γ ⊢ Δ, A ∨ B} および\frac{Γ ⊢ Δ, B}{Γ ⊢ Δ, A ∨ B}

→-左 : \frac{Γ ⊢ Δ, A  B, Π ⊢ Λ}{A → B, Γ, Π ⊢ Δ, Λ}

→-右 : \frac{A, Γ ⊢ Δ, B}{Γ ⊢ Δ, A → B}

∀-左 : \frac{A[_{t}^{a}], Γ ⊢ Δ}{∀xA[_{x}^{a}], Γ ⊢ Δ}  ∀-右 : \frac{Γ ⊢ Δ, A}{Γ ⊢ Δ, ∀xA[_{x}^{a}]}

ただし，自由変数 a は下式に現れない．

∃-左 : \frac{A, Γ ⊢ Δ}{∃xA[_{x}^{a}], Γ ⊢ Δ}  ∃-右 : \frac{Γ ⊢ Δ, A[_{t}^{a}]}{Γ ⊢ Δ, ∃xA[_{x}^{a}]}

ただし，自由変数 a は下式に現れない．