※ 引述《earh (多腦人)》之銘言：
: ※ 引述《priest0204 (香香)》之銘言：
: : Let x and y be variables, A(x),B(x), and A(x,y) be any formulas,
: : and A be any formula not containing any free occurrences of x.
: : Then
: : 1.╞(exist x)(A(x)orB(x))←→(exist x)A(x)or(exist x)B(x)
: 反證法
: 2.~( (exist x)A(x)or(exist x)B(x) )求矛盾
: 3.~(Ex)Ax and ~(Ex)Bx DeM
: 4.Ax or Bx 1,EI
: 5.~Ax 3,Simp,EI
: 6.Bx 4,5 DS
: 7.~Bx 3,Simp,EI
: 8.Bx and ~Bx 6,7 Conj
: 9. (exist x)A(x)or(exist x)B(x) 2-8 ,IP
反方向
1.(Ex)Ax or (Ex)Bx
2.~(exist x)(A(x)orB(x))求矛盾
3.(x)~(Ax or Bx) 2,QN
4.~Ax and ~Bx 3, DeM
5.(x)~Ax 4,Simp,UG
6.(x)~Bx 4,Simp,UG
7.~(Ex)Ax 5,QN
8.~(Ex)Bx 6,QN
9.(Ex)Bx 1,7 DS
10. ~(Ex)Bx and (Ex)Bx 8,9 Conj
11. ~(exist x)(A(x)orB(x)) 2-10 IP
: : 2.╞(for all x)A(x)or(for all x)B(x)→(for all x)(A(x)orB(x))
: 反證法
: 2.~ (x) A(x) or B(x) 求矛盾
: 3.(Ex)~(Ax or Bx) 2,QN
: 4.~(Ax or Bx) 3,EI
: 5.Ax or Bx 1,UI
: 6.~(5) and (5) 4,5 Conj
: 7.(for all x)(A(x)orB(x)) 2-6,IP
: : 3.╞(exist x)(AorB(x))←→Aor(exist x)B(x)
: 反證法
: 2. ~(A or (Ex)Bx) 求矛盾
: 3. ~A and ~(Ex)Bx 2,DeM
: 4. A or Bx 1,EI
: 5.~A 3,Simp
: 6.Bx 4,5 DS
: 7.(Ex)Bx 6,EG
: 8.~(Ex)Bx 2,Simp
: 9. (7) and~(7) 7,8 Conj
: 10. Aor(exist x)B(x) 2-9 IP
(7)請把第7式抄進去，我是懶得打
反方向
1.Aor(exist x)B(x) / (exist x)(AorB(x))
2.~(Ex)(A or Bx) 求矛盾
3.(x)~(A or Bx)
4.~(A or Bx) 3,UI
5.~A and ~Bx 4,DeM
6.~A 5,Simp
7.(Ex)Bx 1,6,DS
8.(x)~Bx 5,Simp,UG
9.~(Ex)Bx 8,QN
10. (Ex)Bx and ~(Ex)Bx 7,9 Conj
11. (Ex)(A or Bx) 2-10,IP
文法部分如果你不太懂，再問你同學
: : Discuss the validity of formulas 1,2 and 3
: 先回前三題
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.42.79.39