2,633
次編輯
Tankianting(討論 | 貢獻) |
Tankianting(討論 | 貢獻) |
||
行 5: | 行 5: | ||
一堆命題序列,由premises(前件)推論到結論。 | 一堆命題序列,由premises(前件)推論到結論。 | ||
本文使用 Fitcher | 本文使用 Fitcher 的演繹證明格式,證明與排版產生器請參此網站:https://mrieppel.github.io/fitchjs/ | ||
==6.1 命題邏輯基本律== | ==6.1 命題邏輯基本律== | ||
行 55: | 行 55: | ||
2 | ~Q | 2 | ~Q | ||
3 |_ P 1,2 vI | 3 |_ P 1,2 vI | ||
</pre> | |||
:如果用上述的證明器會比較 tricky,他不用這個證明規則,要用⊥引入(可以視爲矛盾的意思?)和⊥消除原則,讓各起源於∨左項和右項2個子證明結果證出左項,再進行消除。 | |||
<pre> | |||
Problem: (P v Q), ~Q |- P | |||
1 | (P v Q) Premise | |||
2 |_ ~Q Premise | |||
3 | |_ P Assumption | |||
4 | | P 3 Reit | |||
5 | |_ Q Assumption | |||
6 | | ~Q 2 Reit | |||
7 | | ⊥ 5,6 ⊥I | |||
8 | | P 7 (EFQ) | |||
9 | P 1,3-4,5-8 vE | |||
</pre> | </pre> |