2,633
次編輯
Tankianting(討論 | 貢獻) |
Tankianting(討論 | 貢獻) |
||
行 73: | 行 73: | ||
</pre> | </pre> | ||
=== | ===conditional條件→=== | ||
*假設寫完之後加橫線 | *假設寫完之後加橫線 | ||
<pre> | <pre> | ||
行 89: | 行 89: | ||
4 | | ... | 4 | | ... | ||
</pre> | </pre> | ||
*引入律(→I) | |||
假設子證明假設 C | 假設子證明假設 C 可推演到結論 G,那麼可以做條件引入,如: | ||
<pre> | <pre> | ||
1 | ... | 1 | ... | ||
2 |_ B Premise | 2 |_ B Premise | ||
行 102: | 行 100: | ||
6 | (C → D) 3-5 →I | 6 | (C → D) 3-5 →I | ||
</pre> | </pre> | ||
證明案例: | |||
<pre> | <pre> | ||
行 110: | 行 110: | ||
3 | |_ A Assumption | 3 | |_ A Assumption | ||
4 | | (A ∨ B) 3 ∨I | 4 | | (A ∨ B) 3 ∨I | ||
5 | (A → (A ∨ B)) 3-4 →I | 5 | (A → (A ∨ B)) 3-4 →I #用連字號連結子證明起訖,子證明結束(叫做解除 discharge)。 | ||
</pre> | |||
子證明結束後不能再次開啓,另外一個證明需要解除所有的子證明。 | |||
若是要引入→引入律,那就要在子證明出現前件(p→q的q) | |||
*消去律(→E) | |||
<pre> | |||
1 | A->B | |||
2 | A | |||
3 | B | |||
</pre> | </pre> |