作者MathTurtle (恩典)
看板logic
標題Re: [請益] 證明a=b,then b=a
時間Tue Dec 24 12:29:20 2013
※ 引述《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)