From 2f5054e639dcb8b486dc9521cc63f59d1b14ca9c Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 25 Oct 2023 13:09:51 +0900 Subject: [PATCH] =?UTF-8?q?contradiction=20=E3=81=AE=E8=AA=AC=E6=98=8E?= =?UTF-8?q?=E3=82=92=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 爆発律という言葉を使うようにする --- src/SUMMARY.md | 2 +- src/contradiction.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 12d739ae..cbc2dcde 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -16,7 +16,7 @@ - [cases: 論理和∨を使う](./cases.md) - [choose: 選択関数を得る](./choose.md) - [constructor: 論理積∧を示す](./constructor.md) -- [contradiction: 矛盾](./contradiction.md) +- [contradiction: 爆発律](./contradiction.md) - [conv: 変換モードに入る](./conv.md) - [convert: 惜しい補題を使う](./convert.md) - [done: 証明終了を宣言](./done.md) diff --git a/src/contradiction.md b/src/contradiction.md index 4f8bcd18..22342c6c 100644 --- a/src/contradiction.md +++ b/src/contradiction.md @@ -1,6 +1,6 @@ # contradiction -`contradiction` は，矛盾によりゴールを閉じるタクティクです．矛盾から任意の命題を証明することができます． +矛盾からはどんな命題でも証明することができます．これを爆発律(principle of explosion)と呼びますが，`contradiction` は，この爆発律を使ってゴールを閉じるタクティクです． ローカルコンテキストに `P` と `¬ P` が同時にあるなど，矛盾した状況にあるときにゴールを閉じます．