A B A ∧ B ∧I A ∧ B A ∧E A ∧ B B ∧E [A]n .... B A → B → I,n A A

論理学 述語論理の NK の推論図
A B
∧I
A∧B
A∧B
∧E
A
[A]n
..
..
B
→ I, n
A→B
A A→B
→E
B
[A]n
..
..
⊥
¬A
⊥
A
A ¬A
¬E
⊥
¬I, n
A
∨I
A∨B
A∧B
∧E
B
B
∨I
A∨B
⊥E
A(xi /t)
∃I
∃xi A(xi )
[A]n
..
..
A∨B
C
C
[B]n
..
..
C ∨E,
n
[¬A]n
..
..
⊥
RA, n
A
∀xi A(xi )
∀E
A(xi /t)
ただし、上の推論図の A(xi /t) は、A(xi ) 中の自由変項 xi のすべてを任意の変項または
個体定項 t で置き換えた論理式を表す。t が変項の場合、A(xi /t) において t は自由変項
となっていなければならない。
[A(xi )]n
..
..
C
∃E, n
..
..
A(xi )
∀I
∀xi A(xi )
∃xi A(xi )
C
A(xi ) が依存している仮定には xi
C および C が依存している
は自由変項としては現れない。
A(xi ) 以 外 の 仮 定 に は xi は 自
由変項としては現れない。