数学と数学的論理において、補助定理は、より重要な定理の証明を行うために依存する中間結果です。
実際、定理を証明する方法は次のとおりであることがよくあります。
- 公理の特定のリストとすでに証明されている他の結果から定理Tを証明したいのですが、これは一見すると明らかではないようです。
- しかし、私たちは、 L が真であることがわかっていれば ( L は補題と呼ばれる別の主張である)、受け入れられている論理規則を考慮すると、すぐに次のように結論付けることができると自分自身に言い聞かせます。
- 次に、証明する結果としてL を設定し、それに定理の証明方法を適用します。
- Lが実証されたら、 T を推定します。
この原則は、特にCoqやPVSなどの証明アシスタントと呼ばれるソフトウェアで使用されます。
証明された補題の中には、それらが作成された定理よりも有名になり、通常は定理として機能しますが、 「XXX の補題」として知られ続けているものもあります。
有名な補題の例
- ゾーンの補題:集合論ZF の選択公理と同等であることで有名 – したがって、この公理の定理結果としての役割だけでなく、公理の再定式化 (したがって公理の) の役割も果たします。
- スター補題:スター定理よりも有名になった形式言語理論の定理。
- 羊飼いの補題、
- ベズーの補題。
- ユークリッドの補題
補題の完全なリストを参照してください。
