命題論理における消去法
結論が論理式 B,C を用いて B∨C で表される推論が与えられたとき、推論の前提に加えて ¬B が真であるということを出発点として C が真であることを示すことができれば、もとの推論が妥当であることを示したことになります。これを消去法と呼びます。
命題論理における対偶法
推論の結論が偽であることを出発点として、推論の前提の少なくとも 1 つが偽であることを導くことができれば、対偶律よりもとの推論の妥当性が示されます。このような証明方法を対偶法と呼びます。
命題論理における背理法
推論の結論が論理式 Bとして表されるとき、その否定 ¬B が真であることを仮定した上で、これと推論の前提に対して推論規則を適用して最終的に恒偽式を導くことができれば、否定導入より ¬¬B すなわち B が真になるため、推論式が妥当であることが示されます。このような証明方法を背理法と呼びます。
命題論理における条件付き証明
推論を証明する際には、推論の前提とは異なる論理式を便宜的に真と仮定した上で、その論理式と推論の前提に対して推論規則を適用していく手法が時として有効です。仮定を利用する証明方法の代表的なものは条件付き証明です。
命題論理における証明
推論の妥当性を示すために、前提を出発点として同値変形の法則や推論規則を用いて結論を次々に導出し、最終的に当初の推論式の結論を導出する手法を証明や演繹などと呼びます。
命題論理における破壊的ジレンマ
論理式 A,B,C,D について、「AならばB」「CならばD」「BでないかDでないかの少なくとも一方」という前提から「AでないかCでないかの少なくとも一方」という結論を導く推論規則を破壊的ジレンマと呼びます。
命題論理における構成的ジレンマ
論理式 A,B,C,D について、「AならばB」「CならばD」「AまたはC」という前提から「BまたはD」という結論を導く推論規則を構成的ジレンマと呼びます。
命題論理における双対原理
論理的に同値な2つの論理式が与えられたとき、それらの双対をとるとそれらもまた論理的に同値となります。これを双対原理と呼びます。
全称導入（普遍汎化）
カテゴリーの中から任意に選んだものは同種のものを代表しているため、それが満たす性質は他のすべてのものも共通して持っていることを保証する推論規則を全称導入と呼びます。
全称除去（普遍例化）
すべてのものに当てはまることは、そのカテゴリーに属する特定のものにも当てはまることを保証する推論規則を全称除去と呼びます。
存在除去（存在例化）
ある性質を満たす対象が存在する場合には、その対象に新たな名前をつけてもよいことを保証する推論規則を存在除去と呼びます。
存在導入（存在汎化）
ある性質を満たす特定の対象から、その性質を満たす対象が存在することを導く推論規則を存在導入と呼びます。つまり、具体的に述べられたことは抽象的にも表現可能であるということです。
