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> | ||