Re: [請益] 證明a=b,then b=a

看板logic作者 (恩典)時間12年前 (2013/12/24 12:29), 編輯推噓0(000)
留言0則, 0人參與, 最新討論串13/13 (看更多)
※ 引述《sindarin (官)》之銘言: : : 我不認為「(x)(y)[x=y ≡ (F)(Fx≡Fy)]」是「『正確的』LL」,所謂「正確的LL」與 : : 大彭孟堯教授的「LL」不一樣,其他的理由與意見,有部份被你拿掉了,這裡看不到, : : 如:LL與「正確的LL」可能等價,等等;有需要請回看。 : 所以這裡的意思會是二階邏輯中也可以有像是一階邏輯中PNF theorem? : 這我不敢說到底有沒有,我只是想重述原發文者的意思,而他的說法看起來也比較合理。 : 去年當彭老師助教的時候沒有注意到這點,也是我太疏忽,有機會會再向他請教。 They are certainly not equivalent. In general, (x)[P → Ax] is equivalent to [P → (x)Ax] (provided that x doesn't occur free in P); but [(x)Ax → P] is equivalent to (Ex)[Ax → P], and NOT to (x)[Ax → P] To prove the non-equivalence, let (LL1) be (x)(y)[x=y ≡ (F)(Fx≡Fy)], and (LL2) be (x)(y)(F)[x=y ≡ (Fx≡Fy)] The following model M=<D, D1> (a full model with monadic predicate variables only and no constant) should suffice: D={a, b}; D1= P(D) (the power set of D); Let σ be an assigment such that (x, y, F are variables) σ[x] = a σ[y] = b σ[F] = {a, b} So we have (M, σ) |≠ [x=y ≡ (Fx≡Fy)], hence (LL2) is FALSE in M. But (LL1) is TRUE in M: proof: let τ be any assignment. If (M, τ) |= (x=y), then τ[x]=τ[y] (is either a or b), then for all τ*, τ[x] ∈ τ*[F] iff τ[y] ∈ τ*[F] then (M, τ) |= (F)(Fx≡Fy). As a result, (M, τ) |= [x=y → (F)(Fx≡Fy)] for any τ. on the other hand, If there is some assignment τ such that (M, τ) |≠ (x=y), then τ[x] ≠τ[y] (assume without loss of generality τ[x]=a & τ[y]=b) then we have the assignment υ such that υ[F]={a}, and thus a ∈{a} (=υ[F]), but it is not the case that b ∈{a} (=υ[F]). Hence, τ[x]∈υ[F] but not τ[y] ∈υ[F], Hence (Fx → Fy) is FALSE under assignment υ, Hence (M, τ) |≠ (F)(Fx → Fy), a forteriori, (M, τ) |≠ (F)(Fx ≡Fy). So for ANY assignment τ such that (M, τ) |= (F)(Fx ≡Fy), we should have (M, τ) |= (x=y). So (M, τ) |= [(F)(Fx≡Fy) → x=y ] for any τ. With these results, we have established that (M, τ) |= [x=y → (F)(Fx≡Fy)] for any τ, and (M, τ) |= [(F)(Fx≡Fy) → x=y ] for any τ, so we have (M, τ) |= [x=y ≡ (F)(Fx≡Fy)] for any τ. This implies that (LL1): (x)(y)[x=y ≡(F)(Fx≡Fy)] is TRUE in M. Q.E.D -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.112.146.29 ※ 編輯: MathTurtle 來自: 140.112.146.29 (12/24 12:39)
文章代碼(AID): #1IkGsZap (logic)
討論串 (同標題文章)
文章代碼(AID): #1IkGsZap (logic)