【証明】 ( (A⇒B)∧(B⇒C) ) ⇒ (A⇒C) |
||||||||||||
|
命題論理の形式的体系「自然演繹」に準拠した操作 →step01 →step02 →step03 →step04 →step05 →step06 [step1]自然演繹で認められた操作(2)仮定の書き出し
[step2] 自然演繹で認められた操作(3)推論規則による書き換え |
|
|||||||||||
・推論規則「∧除去則」にしたがって、
仮定1「(A⇒B)∧(B⇒C)」
を「A⇒B」
へ
書き換える。
・推論規則「∧除去則」にしたがって、
仮定1「(A⇒B)∧(B⇒C)」
を「B⇒C」
へ
書き換える。
・推論規則「∧除去則」により、
書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
書き換え後の「A⇒B」「B⇒C」は、それぞれ、仮定1「(A⇒B)∧(B⇒C)」
のもとにある。
・これで、推論規則「∧除去則」による書き換えによって、
仮定1「(A⇒B)∧(B⇒C)」
から、
「仮定1『(A⇒B)∧(B⇒C)』
のもとで『A⇒B』」
「仮定1『(A⇒B)∧(B⇒C)』
のもとで『B⇒C』」
が導出されたことになる。
| |
|
|||
|
|
(∧除去) |
|
(∧除去) |
|
|
A⇒B |
B⇒C |
|
→ 推移律 |
|
論理式「A」 を仮定2として書き出す。
| |
|
||||
|
仮定2 |
|
(∧除去) |
|
(∧除去) |
|
|
A |
A⇒B |
B⇒C |
・推論規則「⇒除去則」にしたがって、
仮定2「A」、「仮定1『(A⇒B)∧(B⇒C)』
のもとで『A⇒B』」を「B」
へ
書き換える。
・推論規則「⇒除去則」の規定により、
書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
書き換え後の「B」は、仮定2「A」、仮定1「(A⇒B)∧(B⇒C)」
のもとにある。
・これで、推論規則「⇒除去則」による書き換えによって、
仮定2「A」、「仮定1『(A⇒B)∧(B⇒C)』
のもとで『A⇒B』」から、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『B』」
が導出されたことになる。
| |
|
||||
|
仮定2 |
|
(∧除去) |
|
(∧除去) |
|
|
A |
A⇒B |
B⇒C |
|||
|
|
(⇒除去) |
||||
| B | |||||
・推論規則「⇒除去則」にしたがって、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『B』」
「仮定1『(A⇒B)∧(B⇒C)』
のもとで『B⇒C』」
を
「C」
へ書き換える。
・推論規則「⇒除去則」の規定により、
書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
書き換え後の「C」は、仮定2「A」、仮定1「(A⇒B)∧(B⇒C)」
のもとにある。
・これで、推論規則「⇒除去則」による書き換えによって、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『B』」
「仮定1『(A⇒B)∧(B⇒C)』
のもとで『B⇒C』」
から
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『C』」
が導出されたことになる。
| |
|
|
|||
|
仮定2 |
|
(∧除去) |
仮定1 |
||
|
A |
A⇒B |
||||
|
|
(⇒除去) |
|
(∧除去) |
||
| B |
B⇒C |
||||
|
|
(⇒除去) |
||||
| C | |||||
|
→ 推移律 |
|
・推論規則「⇒導入則」にしたがって、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『C』」を
「A⇒C」へ書き換える。
・推論規則「⇒導入則」の規定にしたがうと、
「A⇒C」への書き換え後に引き継がれる仮定は、
書き換え前の仮定「A」「(A⇒B)∧(B⇒C)」から、仮定「A」を差し引いた分だけとなるから、
「A⇒C」への書き換え後にのこる仮定は「(A⇒B)∧(B⇒C)」だけとなって、
「仮定1『A⇒B)∧(B⇒C)』のもとで『A⇒C』」が得られる。
・これで、推論規則「⇒導入則」による書き換えで、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『C』」から、
「仮定1『A⇒B)∧(B⇒C)』のもとで『A⇒C』」が導出されたことになる。
| |
|
|
|||
|
[仮定2] |
|
(∧除去) |
仮定1 |
||
|
[A] |
A⇒B |
||||
|
|
(⇒除去) |
|
(∧除去) |
||
| B |
B⇒C |
||||
|
|
(⇒除去) |
||||
| C | |||||
|
|
(⇒導入)仮定2を解消 | ||||
| A⇒C | |||||
|
→ 推移律 → 自然演繹の定理：トピック一覧 → 論理記号：トピック一覧 → 総目次 |
・推論規則「⇒導入則」にしたがって、
「仮定1『A⇒B)∧(B⇒C)』のもとで『A⇒C』」を
「( (A⇒B)∧(B⇒C) ) ⇒ (A⇒C)」へ書き換える。
・推論規則「⇒導入則」の規定にしたがうと、
「( (A⇒B)∧(B⇒C) ) ⇒ (A⇒C)」への書き換え後に引き継がれる仮定は、
書き換え前の仮定「(A⇒B)∧(B⇒C)」から、仮定「(A⇒B)∧(B⇒C)」を差し引いた分だけとなるから、
「( (A⇒B)∧(B⇒C) ) ⇒ (A⇒C)」への書き換え後に仮定はすべて差し引かれてなくなって
しまい、
仮定なしの「( (A⇒B)∧(B⇒C) ) ⇒ (A⇒C)」が得られる。
・これで、推論規則「⇒導入則」による書き換えで、
「仮定2『A』、仮定1『(A⇒B)∧(B⇒C)』のもとで『C』」から、
「仮定1『A⇒B)∧(B⇒C)』のもとで『A⇒C』」が導出されたことになる。
| |
|
|
|||
|
[仮定2] |
|
(∧除去) |
[仮定1] |
||
|
[A] |
A⇒B |
||||
|
|
(⇒除去) |
|
(∧除去) |
||
| B |
B⇒C |
||||
|
|
(⇒除去) |
||||
| C | |||||
|
|
(⇒導入)仮定2を解消 |
||||
| A⇒C | |||||
|
|
(⇒導入)仮定1を解消 |
||||